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 by Industrilogik 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 of 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.

• L.-H. Eriksson, The GTO Toolset and Method, In S. Merz, T. Nipkow (eds.), Proceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006), Electronic Notes in Theoretical Computer Science, Vol. 185, 2007.
• L.-H. Eriksson, Using Formal Methods in a Retrospective Safety Case, In M. Heisel, P. Liggesmeyer, S. Wittman (eds.), Computer Safety, Reliability, and Security -- 23rd International Conference, SAFECOMP 2004, Lecture Notes in Computer Science 3219, Springer-Verlag, 2004.
• L.-H. Eriksson, GTO Reference Manual, Uppsala university, Department of Information Technology 2006.