University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Decomposing scheme plans to manage verification complexity

James, P, Moller, F, Nguyen, HN, Roggenbach, M and Treharne, H (2014) Decomposing scheme plans to manage verification complexity

Full text not available from this repository.


Several formal methods have been proposed for the specification and safety verification of railway applications. In order to be successful they need industrial strength tools to support the animation, proof, model checking and simulation of such systems. The complexity of railway systems means that capabilities of the analysis tools have consistently been improving. In our approach we propose that the complexity of analysis of railway interlocking systems can also be managed through incremental addition of system detail and decomposition of system specifications themselves. We propose a domain specific language (DSL) which describes the core aspects of a railway interlocking system and demonstrate how one can identify suitable decompositions in terms of the DSL. The DSL informs our system engineering approach which uses a graphical editor to input railway scheme plans, supports the automatic generation of CSP jj B specifications of the plans and uses the ProB tool for their animation and model checking.

Item Type: Conference or Workshop Item (UNSPECIFIED)
Divisions : Surrey research (other units)
Authors :
James, P
Moller, F
Nguyen, HN
Roggenbach, M
Date : 1 January 2014
Depositing User : Symplectic Elements
Date Deposited : 17 May 2017 13:33
Last Modified : 23 Jan 2020 18:41

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800