Formal Verification of Statemate-Statecharts
During the software development process it is important to use powerful techniques for proving the expected behavior of the system and hence avoiding failures in real applications later on. Therefore, an effective means to increase confidence in the development process is to use analysis techniques based on the formal descriptions used in early phases (requirements specification).
KeywordsMutual Exclusion Linear Temporal Logic Finite State Automaton Verification Tool Copy Process
Unable to display preview. Download preview PDF.
- [CL96]M. Conrad and E. Lehmann. Anforderungsspezifikation des Fahrgeschwindigkeitskonstanters mit Z und Statemate. Technischer Bericht Nr. F3S/K96–03,Daimler Benz AG, Berlin, 1996.Google Scholar
- [Emm90]E. A. Emmerson. Temporal and modal logic. Handbook of Theoretical Computer Science MIT Press, 1990.Google Scholar
- [For97]Formal Systems (Europe) Ltd. Failures Divergence Refinement, FDR2 User Manual, 1997.Google Scholar
- [HLN+90]David Harel, Hagi Lachover, Amnon Naamad, Amir Pnueli, Michal Politi, Rivi Sherman, Aharon Shtull-Trauring, and Mark Trakhtenbrot. Statemate: A working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering, 16 No. 4, April 1990.Google Scholar
- [HN95]David Harel and Amnon Naamad. The stalemate semantics of statecharts. Technical Report, i-Logis, October 1995.Google Scholar
- [Hoa78]C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, Number 8, 21: 666–667, 1978.Google Scholar
- [Hoa85]C.A.R. Hoare. CSP - Communicating Sequential Processes. Prentice Hall International, 1985.Google Scholar
- [Sca95]J.B. Scattergood. Tools for CSP and Timed CSP, D.Phil. Oxford University Computing Laboratory, 1995.Google Scholar