Paper Info
Title
Specification and Verification of a Safety Shell with Statecharts and Extended Timed Graphs
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.
Year
DOI
Venue
2000
10.1007/3-540-40891-6_4
SAFECOMP
Keywords
Field
DocType
formal method,safety shell,formal specification,formal notation,extended timed graphs,preliminary document,tool support,safety principle,safety critical region,following step,formal verification
Functional verification,Programming language,Intelligent verification,Computer science,Formal specification,Verification,Language Of Temporal Ordering Specification,Refinement,Formal methods,Formal verification
Conference
Volume
ISSN
ISBN
1943
0302-9743
3-540-41186-0
Citations 
PageRank 
References 
8
0.67
10
Authors
5
Name
Order
Citations
PageRank
Jan van Katwijk114731.70
Hans Toetenel27610.54
Abd-El-Kader Sahraoui3314.19
Eric Anderson482.36
Janusz Zalewski513634.56