No Cover Image

Book Chapter 335 views

Verification of Solid State Interlocking Programs / Phillip James; Andy Lawrence; Faron Moller; Markus Roggenbach; Monika Seisenberger; Anton Setzer; Karim Kanso; Simon Chadwick

Software Engineering and Formal Methods, Volume: 8368

Swansea University Author: Moller, Faron

Full text not available from this repository: check for access using links below.

DOI (Published version): 10.1007/978-3-319-05032-4_19

Abstract

This paper reports on the inclusion of a formal method into an industrial design process: concretely, a verification step in railway interlocking design between programming the interlocking and testing this program. Safety still relies on testing; but the burden of completeness and correctness of th...

Full description

Published in: Software Engineering and Formal Methods
Published: 2014
URI: https://cronfa.swan.ac.uk/Record/cronfa19513
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: This paper reports on the inclusion of a formal method into an industrial design process: concretely, a verification step in railway interlocking design between programming the interlocking and testing this program. Safety still relies on testing; but the burden of completeness and correctness of the validation is greatly reduced. A complete methodology is presented for carrying out this verification step in the case of ladder logic programs, and results are presented for real world railway interlockings.
Item Description: Originality:The paper makes the bold step of bringing mathematical theory down to the level of engineering practice; something rare, explaining why the type of formal methods presented are not readily adapted in practice.Significance:The methodology outlined in this paper forms the basis of the technology being adapted by Siemens, which is the foundation of the REF Impact Case Study.Rigour:The methodology is, of course, founded on the most rigorous of mathematical theory development.
College: College of Science
End Page: 268