Sie befinden Sich nicht im Netzwerk der Universität Paderborn. Der Zugriff auf elektronische Ressourcen ist gegebenenfalls nur via VPN oder Shibboleth (DFN-AAI) möglich. mehr Informationen...
Integrating formal specifications into applications: the ProB Java API
Ist Teil von
Formal methods in system design, 2021-10, Vol.58 (1-2), p.160-187
Ort / Verlag
New York: Springer US
Erscheinungsjahr
2021
Quelle
SpringerLink (Online service)
Beschreibungen/Notizen
The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques. Once an appropriate level of certainty is reached, code generators are used in order to gain executable code. In this paper, we propose a different approach: instead of generating code from formal models, it is also possible to embed a model checker or animator into applications in order to use the formal models themselves at runtime. We present a Java API to the
ProB
animator and model checker. We describe several case studies that use this API as enabling technology to interact with a formal specification at runtime.