text: Vehicle safety depends on (a) the range of identified hazards and (b) the operational situations for which mitigations of these hazards are acceptably decreasing risk. Moreover, with an increasing degree of autonomy, risk ownership is likely to increase for vendors towards regulatory certification. Hence, highly automated vehicles have to be equipped with verified controllers capable of reliably identifying and mitigating hazards in all possible operational situations. To this end, available methods for the design and verification of automated vehicle controllers have to be supported by models for hazard analysis and mitigation.
  @cite_1: Assuring safety of autonomous vehicles requires that the vehicle control system can perceive the situation in the environment and react to actions of other entities. One approach to vehicle safety assurance is based on the assumption that hazardous sequences of events should be identified during hazard analysis and then some means of hazard avoidance and mitigation, like barriers, should be designed and implemented. Another approach is to design a system which is able to dynamically examine the risk associated with possible actions and then select the safest action to carry it out. Dynamic risk assessment requires maintaining the situation awareness and prediction of possible future situations. We analyse how these two approaches can be applied for autonomous vehicles and what strategies can be used for safety argumentation.
  @cite_13: System substitution can be defined as the capability to replace a system by another one that preserves the specification of the original one. It may occur in different reconfiguration situations like failure management or maintenance. When substituting a system at runtime, a key requirement is to correctly restore the state of the substituted one. This paper proposes a correct by construction generic model for system reconfiguration defined using formal methods, based on a system substitution operator. Systems are seen as state transition systems. This proposal relies on refinement and proofs. The formal development is conducted with the Event-B method. It consists in defining system substitution as a system composition operator associated to proof obligations. A generic formal model is developed using Event-B. Specific systems instantiate this generic model using a particular use of refinement-based on the definition of witnesses. This proposal is illustrated with an electronic commerce service.
summary: Babin et al. @cite_13 propose a system reconfiguration approach developed with the Event-B method in a correct-by-construction fashion using a behavior pattern similar to our approach (particularly, fig:statemodel ). Reconfiguration as one way to faults is discussed in this work. Wardzi ' n ski @cite_1 discusses hazard identification and mitigation for autonomous vehicles by predetermined risk assessment ( with safety barriers) and dynamic risk assessment. For both, he provides argumentation patterns for creating AV safety cases. In addition to his work, the abstraction and the method we propose covers both paradigms in one framework. We provide formal notions of all core concepts.