The traffic light controller of a simple two-way intersection is specified by data flow components. The focus of this work is on the use of readable description techniques, such as state transition diagrams and tables, to hide the mathematical background of the specifications. A second main point is the use of automatic formal verification tools for the proof of some simple behavioral properties of the specification to validate the specifications.
Stichworte:
Tabular Specification; Model Checking; Traffic Control