The GTO Toolset and Method

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.
Type de document :
Communication dans un congrès
Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.77-90, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00089492
Contributeur : Stephan Merz <>
Soumis le : vendredi 18 août 2006 - 19:21:09
Dernière modification le : vendredi 18 août 2006 - 19:57:26
Document(s) archivé(s) le : mardi 6 avril 2010 - 00:38:01

Fichier

Identifiants

  • HAL Id : inria-00089492, version 1

Collections

Citation

Lars-Henrik Eriksson. The GTO Toolset and Method. Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.77-90, 2006, Automatic Verification of Critical Systems (AVoCS 2006). 〈inria-00089492〉

Partager

Métriques

Consultations de la notice

99

Téléchargements de fichiers

92