A Formal Specification and Validation of a Control System in Presence of Byzantine Errors

S. Gnesi, D. Latella, G. Lenzini, C. Abbaneo, A. Amendola, P. Marmo

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

    5 Citations (Scopus)

    Abstract

    This paper describes an experience in formal specification and fault tolerant behavior validation of a railway critical system. The work, performed in the context of a real industrial project, had the following main targets: (a) to validate specific safety properties in the presence of Byzantine system components or of some hardware temporary faults; (b) to design a formal model of a critical railway system at a right level of abstraction so that could be possible to verify certain safety properties and at the same time to use the model to simulate the system. For the model specification we used the Promela language, while the verification was performed using the SPIN model checker. Safety properties were specified by means of both assertions and temporal logic formulae. To make the problem of validation tractable in the SPIN environment, we used ad hoc abstraction techniques.
    Original languageEnglish
    Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
    Subtitle of host publication6th International Conference, TACAS 2000, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 – April 2, 2000, Proceedings
    EditorsSusanne Graf, Michael Schwartzbach
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages535-549
    Number of pages15
    ISBN (Electronic)978-3-540-46419-8
    ISBN (Print)978-3-540-67282-1
    DOIs
    Publication statusPublished - Mar 2000
    Event6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000 - Berlin, Germany
    Duration: 27 Mar 200031 Mar 2000
    Conference number: 6

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume1785
    ISSN (Print)0302-9743

    Conference

    Conference6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000
    Abbreviated titleTACAS
    CountryGermany
    CityBerlin
    Period27/03/0031/03/00

    Keywords

    • Formal verification
    • Safety critical systems
    • Fault tolerant behavior
    • Linear temporal logic
    • Model checking

    Fingerprint Dive into the research topics of 'A Formal Specification and Validation of a Control System in Presence of Byzantine Errors'. Together they form a unique fingerprint.

    Cite this