4 papers
Animation, Verification and Visualisation of Prolog Transition Systems with ProB
Jan Gruteser, Michael Leuschel, Katharina Engels +1
ProB is a Prolog-based model checker, animator and constraint solver for high-level formal specifications. One can also use ProB to animate transition systems defined by Prolog pre…
Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB
Katharina Engels, Jan Gruteser, Michael Leuschel
Event-B is a formal method rooted in predicate logic and set theory. We encoded over 600 proof rules in Prolog, enabling a systematic, comprehensible proof analysis and constructio…
Failure divergence refinement for Event-B
Sebastian Stock, Michael Leuschel, Atif Mashkoor
When validating formal models, sizable effort goes into ensuring two types of properties: safety properties (nothing bad happens) and liveness properties (something good occurs eve…
Using Formal Models, Safety Shields and Certified Control to Validate AI-Based Train Systems
Jan Gruteser, Jan RoÃbach, Fabian Vu +1
The certification of autonomous systems is an important concern in science and industry. The KI-LOK project explores new methods for certifying and safely integrating AI components…