5 citations · 19 across the 7 of their papers we have counts for
9 papers
Sound Development of Safety Supervisors
Mario Gleirscher, Lukas Plecher, Jan Peleska
Safety supervisors are controllers enforcing safety properties by keeping a system in (or returning it to) a safe state. The development of such high-integrity components can benef…
Complete Test of Synthesised Safety Supervisors for Robots and Autonomous Systems
Mario Gleirscher, Jan Peleska
Verified controller synthesis uses world models that comprise all potential behaviours of humans, robots, further equipment, and the controller to be synthesised. A world model ena…
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs
Simon Foster, Jonathan Julián Huerta y Munive, Mario Gleirscher +1
We extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof assistant by an algebraic model for hybrid program stores, a shallow expression model for…
YAP: Tool Support for Deriving Safety Controllers from Hazard Analysis and Risk Assessments
Mario Gleirscher
Safety controllers are system or software components responsible for handling risk in many machine applications. This tool paper describes a use case and a workflow for YAP, a rese…
Mechanised Assurance Cases with Integrated Formal Methods in Isabelle
Yakoub Nemouchi, Simon Foster, Mario Gleirscher +1
Assurance cases are often required as a means to certify a critical system. Use of formal methods in assurance can improve automation, and overcome problems with ambiguity, faulty…
Assurance of System Safety: A Survey of Design and Argument Patterns
Mario Gleirscher, Stefan Kugele
The specification, design, and assurance of safety encompasses various concepts and best practices, subject of reuse in form of patterns. This work summarizes applied research on s…