Paper Info
Title
A Structured Approach to the Formal Certification of Safety of Computer Aided Development Tools
Abstract
Safety-critical systems are often designed using development support tools which perform translations of high-level specifications into lower-level counterparts. The correctness of the translation is critical to the safety of the resulting systems. However, using non failure-safe components to implement translators is desirable because of the extremely high cost of certified components. In order to ensure the correct behavior of development tools, we adopt a solution based on the idea of verifying each of their executions. In order to perform the verification in an automatic and efficient way, we follow an innovative approach, by distinguishing an off-line and an on-line verification phases. Each proof in the two phases is guaranteed correct by designing the certifying tools according to a logging-and-checking architecture. We describe the off-line and on-line logging-and-checking methodology, its application in the frame of an industrial project, and the ongoing logging-and-checking redesign of a state-of-the-art prover which we intend to use in future applications.
Year
DOI
Venue
1998
10.1007/3-540-49646-7_17
SAFECOMP
Keywords
Field
DocType
ongoing logging-and-checking redesign,certified component,on-line logging-and-checking methodology,formal certification,development tool,development support tool,logging-and-checking architecture,correct behavior,safety-critical system,structured approach,development tools,on-line verification phase,certifying tool
Systems engineering,Computer science,Computer-aided,Computer Aided Design,Correctness,Real-time operating system,Systems architecture,Certification,Gas meter prover,Software development
Conference
Volume
ISSN
ISBN
1516
0302-9743
3-540-65110-1
Citations 
PageRank 
References 
1
0.37
7
Authors
4
Name
Order
Citations
PageRank
Piergiorgio Bertoli177546.89
Alessandro Cimatti25064323.15
Fausto Giunchiglia35431469.35
Paolo Traverso43483223.80