Loading
June 2006
Abstract:A suitable method supported by a toolset with a high degree of automation is a necessity for the successful employment of formal methods in industrial projects. The GTO toolset and method have been developed, and successfully applied, to formal methods in safety- critical control applications related to railway signalling since the mid 1990s.
The toolset and method support the entire formal methods process from writing and validating formal specifications, through modelling of the implementation to formal verification and analysis of verification results. One goal the toolset and method was to make formal methods more competitive by streamlining the process so that - at least within an established application area - individual verification tasks could be done in an "assembly line"-like fashion with minimum overhead.
In line with this goal, the toolset is intended for use with configurable systems, where a generic specification is applicable to a family of systems and adapted to a specific system using configuration data.
The functions carried out by the toolset include static checking and simulation of specifications, checking of configuration data, generation of implementation models from PLC program code or relay schematics, simulation of the implementation model, formal verification by refinement proof, and analysis of failed refinement proofs. Refinement proofs are automatically carried out by a satisfiability (SAT) solver of the user's choice, which is interfaced to the main tool.
We will outline the method and functions of the toolset as well as the formal notation - a simple temporal predicate logic - used by the toolset.
Available as PDF (153 kB, no cover)
Download BibTeX entry.