ePrints Soton (University of Southampton) · 2013 · 10 citations · 5 references
Open access
EngineeringComputer ScienceSystems EngineeringFormal MethodsHazard IdentificationSafety EngineeringSafety Requirements EngineeringSafety SystemsSafety-critical SystemsSoftware DesignSpecification LanguagesSystem SafetyFormal Methods For SafetyFormal ReasoningProof LanguageSafety ConstraintsSafety-critical System ModelingSafety-critical System RequirementsSafety-critical Systems AnalysisSystem-theoretic Process Analysis
System-Theoretic Process Analysis (STPA) from Leveson is a technique for hazard analysis developed to identify more thoroughly the causal factors in complex safety-critical systems, including software design errors.Event-B is a proof-based modelling language and method that enables the development of specifications using a formal notion of refinement.We propose an approach to hazard analysis where system requirements are captured as monitored, controlled, mode and commanded phenomena and STPA is applied to the controlled phenomena to identify systematically the safety constraints.These are then represented formally in an Event-B specification which is amenable to formal refinement and proof.
5