Specification and verification of a safety shell with statecharts and extended timed graphs

    Authors

    J. van Katwijk; H. Toetenel; A. E. Sahraoui; E. Anderson;J. Zalewski

    Comments

    Authors: contact us about adding a copy of your work at STARS@ucf.edu

    Keywords

    SYSTEMS; Computer Science, Hardware & Architecture; Computer Science, Software; Engineering; Computer Science, Theory & Methods

    Abstract

    A new technique for applying safety principles, termed safety shell, eases the formal verification by segregation of the safety critical regions of the application into independent, well structured modules. This paper presents a practical use of formal methods for verification of the safety shell. A framework is proposed for the integration of semiformal and formal notations, in order to produce a formal specification on which verification tools can be applied. The approach relies on the following steps. The first step consists in using adequately statecharts and support tools to guide the analyst's understanding of the system and produce a preliminary document. In the second step an XTG-based specification is generated from the preliminary document on the basis of predefined rules. The third step then is to verify the specification w.r.t. relevant specified properties. Tool support is being developed to assist in the second step, while tool support for verification is available through the TVS toolset.

    Journal Title

    Computer Safety, Reliability and Security, Proceedings

    Volume

    1943

    Publication Date

    1-1-2000

    Document Type

    Article

    Language

    English

    First Page

    37

    Last Page

    52

    WOS Identifier

    WOS:000175008000004

    ISSN

    0302-9743; 3-540-41186-0

    Share

    COinS