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

fYear

2000

fDate

2000

Firstpage

156

Lastpage

162

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer-Aided Control System Design, 2000. CACSD 2000. IEEE International Symposium on

Conference_Location

Anchorage, AK

Print_ISBN

0-7803-6566-6

Type

conf

DOI

10.1109/CACSD.2000.900204

Filename

900204