Model Checking

In model checking, as it will be investigated in this course, the models will be abstract structures representing the behavior of some kind of automata $M_{ExGraph}$. The formal languages $S_{TL}$ used will be languages of so called temporal logics. Whereas CTL$^{*}$ has been shown to be too powerful for computation there are weaker versions like LTL and CTL (or ACTL* and ACTL) which can be used instead. There will some mapping $\cal{I}$ be constructed which makes the behavior of the automata a model for the expressions of the temporal logic languages. To check whether an expression $f \in S_{TL}$ is satisfied by such a model will be done by constructing an checking algorithm which takes as input $\{f, M_{ExGraph}\}$ and as output Yes, No^2.2. (cf. figure 2.7).

Figure 2.7: Engineering Requirements Models, Specifications, and Verification

The interesting question is then, whether the algorithm will ever stop or not. To answer this question one has to verify it. This can be done by hand or automatically. If the number of possible states is sufficiently large a manual procedure will not be feasible. Since the 1980s automatic procedures for model checking have been invented. But these are -as one can easily imagine- can become again impractical when the computing time is becoming too large, which is e.g. caused by a 'state space explosion'. But steadily new improvements are researched and provided, which are making this strategy of model checking more and more usable for industry sized projects.

Thus applying formal specifications with temporal logic languages based on usable model structures combined with verification procedures are allowing a remarkable improvement of the quality of systems modeling.