Industrial-Strength Formal Specification Techniques, Workshop on (1995)
Boca Raton, Florida
Apr. 5, 1995 to Apr. 8, 1995
V. Hartonas-Garmhausen , Dept. of Eng. & Public Policy, Carnegie Mellon Univ., Pittsburgh, PA, USA
T. Kurfess , Dept. of Eng. & Public Policy, Carnegie Mellon Univ., Pittsburgh, PA, USA
E.M. Clarke , Dept. of Eng. & Public Policy, Carnegie Mellon Univ., Pittsburgh, PA, USA
D. Long , Dept. of Eng. & Public Policy, Carnegie Mellon Univ., Pittsburgh, PA, USA
This study presents new risk analysis tools and demonstrates the feasibility and applicability of these tools in the design verification of railway interlocking control systems and deadlock prevention in automated manufacturing systems. Our verification methodology consists of the following stages. First, we analyze the rules executed by the controller and extract a state machine model of the controller. Second, we compose safety, reliability, and operability system specifications using a propositional temporal logic. Finally, we use the model checker to check the state machine model of the system against its requirements. The verification approach allows an exhaustive search of all possible behaviors and scenarios. We verified two real railway interlocking control applications with 125 and 452 constraints respectively. Checking two opposing signal protection specifications involving 3 signals ranged between 74 and 1223 seconds depending on the size and the complexity of the interlocking. Traditional verification methods typically require several person weeks.
risk management; computer integrated manufacturing; concurrency control; formal verification; formal specification; temporal logic; CAD/CAM; industrial control; industrial design verification; design verification; railway interlocking control systems; deadlock prevention; automated manufacturing systems; verification methodology; state machine model; safety; reliability; operability; propositional temporal logic; model checker; railway interlocking control; signal protection specifications
E. Clarke, T. Kurfess, V. Hartonas-Garmhausen and D. Long, "Automatic verification of industrial designs," Industrial-Strength Formal Specification Techniques, Workshop on(WIFT), Boca Raton, Florida, 1995, pp. 88.