Dependability checking with StoCharts: Is train radio reliable enough for trains?

D.N. Jansen, H. Hermanns

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    9 Citations (Scopus)
    68 Downloads (Pure)

    Abstract

    Performance, dependability and quality of service (QoS) are prime aspects of the UML modelling domain. To capture these aspects effectively in the design phase, we have recently proposed STOCHARTS, a conservative extension of UML statechart diagrams. In this paper, we apply the STOCHART formalism to a safety critical design problem. We model a part of the European Train Control System specification, focusing on the risks of wireless communication failures in future high-speed cross-European trains. Stochastic model checking with the model checker PROVER enables us to derive constraints under which the central quality requirements are satisfied by the STOCHART model. The paper illustrates the flexibility and maturity of STOCHARTS to model real problems in safety critical system design.
    Original languageUndefined
    Title of host publicationQEST 2004: first international conference on the quantitative evaluation of systems
    Place of PublicationLos Alamitos, Calif., USA
    PublisherIEEE Computer Science Press
    Pages250-259
    Number of pages10
    ISBN (Print)0-7695-2185-1
    DOIs
    Publication statusPublished - Sep 2004
    Event1st International Conference on Quantitative Evaluation of Systems, QEST 2004 - University of Twente, Enschede, Netherlands
    Duration: 27 Sep 200430 Sep 2004
    Conference number: 1
    http://www.qest.org/qest2004/

    Publication series

    Name
    PublisherIEEE Computer Science Press

    Conference

    Conference1st International Conference on Quantitative Evaluation of Systems, QEST 2004
    Abbreviated titleQEST
    CountryNetherlands
    CityEnschede
    Period27/09/0430/09/04
    Internet address

    Keywords

    • IR-49759
    • EWI-1297
    • METIS-222571

    Cite this