Objective/MC: A high-level model checking language Formalization of the imperative core and translation into PRISM

摘要

Among model checking tools, the behaviour of a system is often formalized as a transition system with atomic propositions associated with states (Kripke structure). In current modeling languages, transitions are usually specified as updates of the system's variables to be performed when certain conditions are satisfied. However, such a low-level representation makes the description of complex transformations difficult, in particular in the presence of structured data. We present Objective/MC, a high-level language with imperative semantics for modeling finite-state systems. The language features are selected with the aim of enabling the translation of models into compact transition systems, amenable to efficient verification via model checking. To this end, we have developed a compiler of our high-level language into the modeling language of the PRISM probabilistic model checker. One of the main characteristics of the language is that it makes a very different treatment of global and local variables. It is assumed that global variables are actually the variables that describe the state of the modeled system, whereas local variables are only used to ease the specification of the system's internal mechanisms. In this paper, we give a complete formal definition of the language, its type system and static analyses, of the transformations to be performed at the level of the Control Flow Graph for the pruning of local variables, and of the PRISM code generation.