Often different behavior definitions for a given system component are given different description formalisms. For instance, the behavior of a method (declared in the interface of a given object class) can be desribed by the algorithm of its body - or by input and output assertions concerning its parameters and the values of the state variables of the object instance. Or the behavior of an accepting state machine, may also be defined by a regular expression. Often one of these behavior definitions appear to be more abstract than the other.
In the case of model checking, one considers two behavior descriptions, one usually in an "executable" description language, such as programming language, state machine, or similar, and the other given in Tempora Logic. Temporal logic is an extension of prediate logic which includes, in addition to the basic logic operations of and, or, not, imply, etc. also operators that relate to the behavior over time. These operators are usually always, eventually, next and until.
These operators can be used to express some other interesting time-related properties, such as
There are two types of temporal logic (TL): Linear time and branching time TL
Here is a good introduction to Model Checking by Girish Keshav Palshikar. This article describes the motivation and gives some examples using the branching time temporal logic CTL, as introduced by Ed Clarke. A PhD student of his team used models in the form of BDD (binary decision diagrams) << see tutorial T1 >>. CTL is also used in the UPPAAL tool - the verification of some properties of an example system is described in Section 3.3. if this article.
Now model checking using SAT (this is the problem of satisfying a boolean function by selecting appropriate values for the variables occuring as parameters in the function) has been proposed by different authors << see tutoriel T2 by Clarke>>. In this case the function to be satisfied is the negation of the desired system property, and if the function can be satisfied, a counter-example will be found which shows that the property is not satisfied. If SAT is unsuccessful for a large space of explored possibilities, one may assume that the property holds. Note that the Alloy tool also uses the SAT technique; Aloy uses a notation related to UML class diagrams for defining models, and searches amoung all possible instantiations (object instant models - within a certain range that can be specified) whether an instant exists that contradicts the desired system property.
The Spin tool provides model checking for linear time temporal logic (see paper by Holzmann). This paper also gives an introduction to linear temporal logic and to the Promela language used for defining models. It also presents some examples.
Some additional course notes on temporal logic can be found on pages 7 through 12 and 38 through 40 here. << A more complex example involving linear-time temporal logic and specification with assumptions and guarantees is given by the arbiter specification in [Bochmann 1982] >
Here are some advanced tutorials on formalized modeling of distributed systems, including a tutorial on model checking of BDD systems.
If a system is composed of several components, one is often interested in viewing the system as a black box, showing only the external interactions, but not the interactions between the components within the system. One says that the internal interactions should be hidden. In other cases, one may be interested only in the interactions at one particular interface of the specified system, ignoring the interactions at another interface (called projection onto the visible interface). Such a black-box view of a composed system or a projection on a subset of the interfaces is an abstraction of the original (more detailed) specification. Such a more abstract view of the behavior can be obtained by replacing the labels of interactions to be hidden, in the original behavior specification, with sponteneous transitions labelled "i" or "tau". The resulting transition system is in general state-nondeterministic, that is, for a given sequence of observed (visible) interactions, the system may be in more than one state.
Instead of the non-deterministic behavior resulting from hiding, one is sometimes interested in having an equivalent deterministic transition systems that generates the same execution sequences as the behavior obtained from hiding.
Definition: Two behavior specifications are trace-equivalent if they define the same set of possible execution sequences of interactions.
There is a well-known algorithm (see section on Deterministic and non-deterministic automata in the course notes for SEG-2106 A - at the end) which constructs an equivalent deterministic automaton from a nondeterministic one, based on trace equivalence. Unfortunately, the number of states of the deterministic automaton may be exponentially larger than the number of states of the given nondeterministic automaton; this means the algorithm has exponential complexity, but in most practical cases, it gives reasonable results.
There are other approaches to comparing the dynamic behavior of different specifications. This is important when one asks such questions as: "Does this more detailed design specification conform to the requirements defined by this more abstract model ?" - If we assume that a system specification defines the set of all allowed execution sequences (this approach is called "trace semantics"), then we can define safeness as follows: An implementation modeled by I conforms to a specification model S iff the set of execution sequences defined by I is included in those defined by S. This conformance relation is called "trace inclusion". It is an ordering relationship between specifications.
Sometimes other comparison criteria, besides trace equivalence, are more appropriate for comparing specifications (see slides 27 through 36 in course notes):
Note that bi-simulation equivalence impies testing equivalence, and the latter implies trace equivalence (but not the other way round). See slide 35 in course notes.
From programming languages, one is used to "compositonal specifications": A class defined in some file can be used as a component in another system. That system would normally be composed of several separately defined classes, plus possibly some specific code written for this system.
In the chapter on "Behavior modeling using states and transitions", we have seen that separately defined state machines can be composed into a system where the different state machines communicate by rendezvous or by message passing, thus giving rise to a distributed system. We have seen that reachability analysis can be used to understand the behavior of the global system based on the behaviors of each of the components.
One is therefore interested in a specification language that allows the description of a system composed out of several components. The following list gives some examples of such notations.
An intuitive graphical notation for block structures with channels for exchanging messages has standardized by SDL. It has now also been included in UML-2 under the name of "composite structures".
Different process algebras have been proposed for introducing a notation with abstraction and concurrency for systems communicating through rendezvous. The sequencing operators normally include sequence, alternative, concurrency, (possibly recursive) definitions (with alphabet), interaction hiding. For example, in the LOTOS specification language, the following constructs are available:
Here is an example specification
Two kinds of choices: internal and external
The activity defined by the left diagram may be used to define the behavior of a simple activity in another activity diagram. The diagram on the right is such an example (where the Assemble Order activity may be defined by a detailed diagram, as on the left).
"Parameter set" = alternative sets of inputs or outputs
Created in 2007; last update: March 5, 2013
