In: Real-Time Systems, Vol. 8, No. 2-3, pages 117-172. 1995.
Abstract: Tools for formally specifying software for real-time systems have strongly improved their capabilities in recent years. At present, tools have the potential for improving software quality as well as engineers' productivity Many tools have grown out of languages and methodologies proposed in the early 1970s. In this paper, the evolution and the state of the art of tools for real-time software specification is reported, by analyzing their development over the last 20 years. Specification techniques are classified as operational, descriptive or dual if they have both operational and descriptive capabilities. For each technique reviewed three different aspects are analyzed, that is, power of formalism, tool completeness, and low-level characteristics. The analysis is carried out in a comparative manner; a synthetic comparison is presented in the final discussion where the trend of technology improvement is also analyzed.
Keywords: Petri nets, communicating processes, formal methods, language specifications, safety analysis, software development, specification-oriented tools, structured analysis, temporal logics.