Provably Reaching Verifiably Safest States of Autonomous Machines in Rare Scenarios
Automation, Mechatronics, Control Systems, Intelligent Technical Systems, Robotics
Engineering Design, Machine Elements, Product Development
Software Engineering and Programming Languages
Final Report Abstract
Controllers of autonomous machines are required to detect hazardous situations and perform appropriate actions to react to such situations in a way such that undesirable consequences are avoided. The validity, completeness, and dependability of both, hazard detection capabilities and risk mitigation capabilities, have to be assured. This engineering task requires novel methods equipping safety engineers with corresponding abstraction and modelling techniques. The objective of this project was to develop a formal framework for situational hazard modelling and for the design and verification of mitigation actions based on such models. The research on this project resulted in: a new theory of risk structures; a formal framework for generic situational risk modelling and analysis, particularly useful for highly automated machines with dependable risk mitigation mechanisms; an investigation and demonstration of basic algebraic properties of this framework; an enhancement and validation of the software tool YAP implementing the concepts used in the framework; an analysis of design and argumentation patterns to validate both theory and tool development; a relational approach to the behavioural specification of mitigation actions that can be verified against a given risk model; an analysis of issues in and obstacles to formal methods integration, transfer, and use to prepare for the transformation of the framework into an industry-strength formal method. The developed framework aims at a generalisation and extension of existing methods (e.g. dynamic fault tree analysis), usable as an integrated formal method allowing engineers to deal with several abstractions (e.g. from software, electronic and mechanical hardware) in a coherent way. Safety also depends on the context of an autonomous machine and safety invariants rely on good context models. Risk structures provide a flexible and powerful way for identifying and structuring such invariants in a layered manner. That way, risk structures address an ongoing research challenge in safety-critical systems engineering. Overall, the research on this project lead to many new insights and interesting further research questions that create opportunities for further research and development. Further Work. YAP involves manual modelling and expert interaction during the analysis of the models. This has to be improved by integrating YAP with tools such as the CSP Failures/Divergences refinement checker4 (FDR): Particularly, I want to automatically translate YAP scripts into CSP M , the machine-readable CSP dialect used as the input language of FDR. My formal investigations suggest the existence of a hierarchy of increasingly complete and expressive mitigation orders. I am currently investigating one of these. To aid the safety engineer in keeping the risk model R minimal and simple, the simplification rules for R have to go beyond the present discussion. I aim to implement these rules in YAP. Because R is provided with an operational semantics, it allows the derivation of minimal cut sequences (MCSeqs) and has the potential to automate DFTA and repair synthesis based on such analysis. YAP can be useful for this and thus requires corresponding extensions. Exploitation of the Results. Together with a German software company in Bremen developing industrial model-based testing tools, I aim to investigate an approach to the derivation of test models for safety monitors from risk structures.
Publications
- (2018). “Strukturen für die Gefahrenerkennung und -behandlung in autonomen Maschinen”. In: acatech DISKUSSION: Beiträge zu einer Systemtheorie Sicherheit. Ed. by Jürgen Beyerer et al., pp. 154–167. ISSN: 2192-6182
Mario Gleirscher
- (2019). “Evolution of Formal Modelbased Assurance Cases for Autonomous Robots”. In: 17th Int. Conf. Software Engineering and Formal Methods. Vol. 11724. LNCS. Springer
Mario Gleirscher, Simon Foster, and Yakoub Nemouchi
(See online at https://doi.org/10.1007/978-3-030-30446-1_5) - (2019). “New Opportunities for Integrated Formal Methods”. In: ACM Computing Surveys. ISSN: 0360-0300
Mario Gleirscher, Simon Foster, and Jim Woodcock
(See online at https://doi.org/10.1145/3357231) - (2019). “Risk Mitigation Strategies in High Automation”. In: Software Engineering und Software Management. Ed. by S. Becker et al. Vol. P-292. LNI. Presentation abstract. Bonn: Gesellschaft für Informatik. ISBN: 978-3-88579-686-2
Mario Gleirscher
(See online at https://doi.org/10.18420/se2019-12)
