Conference Paper/Proceeding/Abstract 657 views
Decomposing scheme plans to manage verification complexity
Phillip James 
,
Faron Moller ,
Hoang Nguyen ,
Markus Roggenbach ,
Steve Schneider,
Helen Treharne
,
Faron Moller ,
Hoang Nguyen ,
Markus Roggenbach ,
Steve Schneider,
Helen Treharne
FORMS/FORMAT- 10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems
Swansea University Authors:
Phillip James , Faron Moller , Hoang Nguyen , Markus Roggenbach
Abstract
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...
| Published in: | FORMS/FORMAT- 10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems |
|---|---|
| Published: |
2014
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa37077 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
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. |
|---|---|
| College: |
Faculty of Science and Engineering |