Proving safety properties for embedded control systems

It is well-known that a fundamental problem in embedded control systems is the verification of the safety requirements. Formal methods and related support tools can successfully be applied in the formal proof that a system is safe. However, the complexity of real systems is such that automated tools often fail to formally validate such systems. A typical case is when "state explosion" problems arise. In this paper, we show some "abstraction techniques" to make the problem of safety requirements validation tractable by current tools. These abstraction techniques have been defined inside a verification methodology that has been tested on the specification of a railway computer based interlocking signalling control system. The conditions under which this methodology can be applied to systems in different application areas are finally discussed.