Refinement of Safety-Related Hazards into Verifiable Code Assertions

: This paper presents a process for the stepwise refinement of safety code assertions from identified system hazards. The code assertions are intended for use in system safety verification. The development of the safety code assertions increases the feasibility of using code verification tools such as SPARK Examiner in the safety verification of large software-intensive systems. The process is demonstrated for a hypothetical chemical factory information system.

• Type: Conference
• Year: 1998
• Where: SAFECOMP
• Authors: Ken Wong, Jeff Joyce
• Keywords: Code Verification Tools, SAFECOMP 1998, Safety Code Assertions, Safety Verification, Security Privacy