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 the enabling technology ProB 2.0, a Java API to the ProB animator and model checker. We describe several case studies that use ProB 2.0 to interact with a formal specification at runtime.
CITATION STYLE
Körner, P., Bendisposto, J., Dunkelau, J., Krings, S., & Leuschel, M. (2019). Embedding high-level formal specifications into applications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11800 LNCS, pp. 519–535). Springer. https://doi.org/10.1007/978-3-030-30942-8_31
Mendeley helps you to discover research relevant for your work.