Specification and verification of reactive system behaviour: The Railroad Crossing example

In this paper we present an approach to the specication and verication of reactive systems. The approach uses Timed Statecharts and Real Time Logic for the specication of temporal behaviour, and theorem proving techniques for the verication of safety and utility properties. Formal verication is achieved through the automation of semi-formal (rigorous) proofs using a theorem prover (Proofpower HOL). To illustrate the approach, we use the Railroad Crossing Problem, which has been proposed, along with a set of criteria for assessment, as a benchmark for the comparison of real-time formalisms. We conclude with our assessment of the approach against the proposed criteria.