Title :
SF2STeP: a CAD tool for formal verification of timed stateflow diagrams
Author :
Kalita, Dhrubajyoti ; Khargonekar, Pramod P.
Author_Institution :
Dept. of Electr. Eng. & Comput. Sci., Michigan Univ., Ann Arbor, MI, USA
Abstract :
Stateflow is a graphical design and development tool from Mathworks for modeling complex reactive systems based on Harel´s (1987) statecharts. TTMcharts introduced by Ostroff (1997) are similar to statecharts with a simpler execution semantics and support for modeling timing properties. A Stateflow diagram can be augmented to a timed Stateflow diagram based on the semantics of TTMcharts. STeP (Stanford´s Temporal Prover) is a tool to formally verify temporal specifications of reactive systems. The basic inputs to STeP are a model of reactive system expressed as a fair transition system, and a specification to be proved expressed in temporal logic. The paper describes a CAD tool SF2STeP that translates a timed Stateflow diagram to a fair transition system which can be used as an input to STeP. The correctness of a reactive system modeled in Stateflow can thus be formally verified using STeP with the help of this CAD tool
Keywords :
control system CAD; formal verification; software packages; temporal logic; theorem proving; CAD tool; Mathworks; SF2STeP; Stanford´s Temporal Prover; TTMcharts; execution semantics; graphical design and development tool; reactive system; temporal specifications; timed Stateflow diagram; timed stateflow diagrams; Analytical models; Computer languages; Design automation; Design engineering; Explosions; Formal verification; Logic; Machining; Mathematical model; Timing;
Conference_Titel :
Computer-Aided Control System Design, 2000. CACSD 2000. IEEE International Symposium on
Conference_Location :
Anchorage, AK
Print_ISBN :
0-7803-6566-6
DOI :
10.1109/CACSD.2000.900204
