@inproceedings{Boh2003,
Author = {Bohn, J. and Damm, W. and Klose, J. and  Moik, A. and  Wittke, H.},
Title = {Modeling and Validating Train System Applications Using Statemate  and Live Sequence Charts},

Year = {2003},
Month = {05},
Editor = {Society for Design and Process Science},
Publisher = {Society for Design and Process Science},
Booktitle = {Proceedings of the Conference on Integrated Design and Process Technology (IDPT2002)},
type = {inproceedings},
note = {The European CENELEC norm now requires train system applications with critical safety integrity levels to be developed using formal methods, in particular supporting various forms of analysis to check for different correctness properties. In doing so, the},
Abstract = {The European CENELEC norm now requires train system applications with critical safety integrity levels to be developed using formal methods, in particular supporting various forms of analysis to check for different correctness properties. In doing so, the CENELEC standard reflects the increasing need for advanced validation techniques in developing in particular also on board train system applications, which increasingly involve both complex and safety critical control units. This paper describes a methodology for developing train system applications based on powerful extensions of the Statemate modeling tool from I-Logix Inc. The extension come in three dimensions:- Live Sequence Charts - a variant of the well-known Message Sequence Charts of MSC2000 and the Sequence Diagrams in UML - are integrated with Statemate in order to allow capturing all interworkings between players such as on-board train control and train crossing control or between different trains, thus supporting the system development steps with a concise and semantically well-founded representation of the critical communication protocols - Model Checking is integrated into Statemate to formally establish the correctness between such system requirements and a system specification developed in the industry standard CASE tool Statemate. This paper reports on an extension of the product version now marketed by I-Logix, which supports formal verification of communication protocols captured as Live Sequence Charts. Model Checking can hence be used to verify all safety requirements on the system model, as well as to formally verify all system integration aspects using a virtual system integration as captured in Statemate. - Automatic Generation of Test Vectors from the Statemate specification model as well as from Scenarios can be used to validate the actual control units - in fact the test vectors can be downloaded to test-rigs allowing hardware-in-the-loop tests of system components. The paper focuses on the overall methodology, which is explained using a train-system application, incorporating experiences from an ongoing cooperation with Bombardier transport systems.}
}
@COMMENT{Bibtex file generated on }