Abstract 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.

Abstract Initially, the Rodin platform for Event‐B did away with a textual representation for models. In this paper, we explain why a textual representation was required after all and we present the semantic‐aware text editor Camille for Rodin. We explain the design choices of Camille, such as splitting the syntax into two‐levels for machine and formula syntax. We also describe the challenges, such as synchronizing the textual representation with the Rodin database, and how they were overcome using an EMF abstraction layer. Copyright © 2011 John Wiley & Sons, Ltd.