No Cover Image

Conference Paper/Proceeding/Abstract 31 views

Decomposing scheme plans to manage verification complexity

Phillip James Orcid Logo, Faron Moller Orcid Logo, Hoang Nguyen Orcid Logo, Markus Roggenbach Orcid Logo, 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 Orcid Logo, Faron Moller Orcid Logo, Hoang Nguyen Orcid Logo, Markus Roggenbach Orcid Logo

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...

Full description

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