uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
The GTO Toolset and Method
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
2007 (English)In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, Vol. 185, 77-91 p.Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
2007. Vol. 185, 77-91 p.
Keyword [en]
Formal methods process, Formal methods tools, Formal verification, Generic specification, Refinement proof
National Category
Computer Science
URN: urn:nbn:se:uu:diva-20834DOI: 10.1016/j.entcs.2007.05.030OAI: oai:DiVA.org:uu-20834DiVA: diva2:48607
Available from: 2008-01-18 Created: 2008-01-18 Last updated: 2011-02-28Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Eriksson, Lars-Henrik
By organisation
Computing Science
In the same journal
Electronical Notes in Theoretical Computer Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 207 hits
ReferencesLink to record
Permanent link

Direct link