2026-07-20T05:27:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:640 2024-03-06T11:06:53Z ddc:004 open_access

Animating and Model Checking B Specifications with Higher-Order Recursive Functions Leuschel, Michael Bendisposto, Jens B-Method Model Checking Animation Logic Programming Visualization Real-life specifications often contain complicated functions. Animation and validation of such functions and specifications is very important. However, such functions pose a major challenge to animation and model checking. Earlier versions of ProB required that functions be explicitly expanded which is prohibitively expensive or impossible. The central idea of this new research is to compile such functions into symbolic closures which are only examined when the function is applied to some particular argument. This enables ProB to successfully animate and model check a new class of specifications, where animation is especially important due to the involved nature of the specification. We will illustrate this new approach on an industrial case study. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Michael Leuschel and Jens Bendisposto 2006 Is Part Of Dagstuhl Seminar Proceedings, Volume 6191, Rigorous Methods for Software Construction and Analysis (2006) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.06191.3 urn:nbn:de:0030-drops-6407 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06191.3 eng https://creativecommons.org/licenses/by/4.0/legalcode