We present a novel propositional encoding for the reachability problem of communicating state machines. The problem deals with the question whether there is a path to some combination of states in a state machine view starting from a given configuration. Reachability analysis finds its application in many verification scenarios. By using an encoding inspired by approaches to encode planning problems in artificial intelligence, we obtain a compact representation of the reachability problem in propositional logic. We present the formal framework for our encoding and a prototype implementation. A first case study underpins its effectiveness.
In model-based engineering (MBE), software models take over the role as core development
artifact, which textual code has in traditional software engineering. The goal of MBE is to
leverage the abstraction power of models in order to deal with the complexity of modern
software systems [
In the context of MBE, model checking is used for the verification of behavioral models like UML state machines. For this purpose, many encodings of state machines have been proposed which translate the state machines to the input format of the model checkers. Usually, ? This work was partially funded by the Vienna Science and Technology Fund (WWTF) under grant
ICT10-018 and by the Austrian Science Fund (FWF): P25518-N23.
Student
working
/the model checkers provide languages to describe finite state automata, which are also the
conceptual basis of state machines. However, it still can be challenging to find a
semanticspreserving translation as even similar concepts may strongly diverge in their semantics. In this
paper, we propose to directly encode the reachability problem for composite state machines
into the problem of satisfiability of propositional logic (SAT). The motivation behind this
approach is an integration into our formal MBE framework [
This paper is structured as follows. First, we review related work in Sec. 2. Then we provide a concise problem definition in Sec. 3 which serves as basis for our encoding presented in Sec. 4. In Sec. 5 we introduce our Eclipse-based implementation and report on a first case study. Finally, we conclude with an outlook to future work. 2
Several works have been presented which deal with the transformation of UML state machines
to input languages of model checkers (see for example in [
However, one of the major challenges of such approaches is to overcome semantical
heterogenities, which raises the question if this translation step is really required. This has already
been recognized by Niewiadomski et al., who propose an encoding to propositional logic
for bounded reachability analysis of state machines, which they show to be more efficient
than translations to standard model checkers [
To motivate our approach consider the following example. Fig. 1 shows the state machines of a student and a coffee machine implementing a simplified workflow of a student’s interaction StudentExt working ////desperate /orderCoffee coffeeDone//waiting error/with a coffee machine. The initial state of each state machine is indicated by an arrow from a black filled circle. States are visualized as rounded rectangles and are connected to each other by transitions. Each transition carries a label consisting of a symbol called trigger to the left, and a set of symbols called effects to the right of a “/.” The empty trigger indicates that the transition can be executed without receiving any trigger symbol. This symbol can be used to model an on-completion event. The symbol “–” represents an empty set of effects. The receipt of the trigger symbol causes the state machine to change its current state from the source state to the target state of the transition. The symbols in the set of effects are sent during the execution of the transition. The communication among state machines is synchronous and therefore the execution of a transition is only possible if each of its effects is understood by a different state machine in its current state.
For a given set of state machines, the Global State Checking (GSC) problem asks whether a certain combination of states of the state machines can be reached from an initial configuration. In this paper we consider the k-Global State Checking (k-GSC) problem. Given a set M of state machines which communicate over an alphabet A, the k-GSC problem asks whether a certain combination of states of the state machines can be reached from an initial configuration by a path with a length of at most k. For example, it can be checked whether the combination of the states working in state machine student and preparing in state machine coffee machine is reachable starting from the initial states through a path of length 10, or whether the combination of waiting and error is not reachable by a path of length 1000. In the following, we present a precise definition of the semantics of a state machine view and of the k-GSC problem. We start by defining a state machine as follows: Definition 1 (State Machine). Given an alphabet A, a state machine M is a quintuple (S,ι,Atr ,Aeff ,T ), where S is a set of states, ι ∈ S is a designated initial state, Atr ⊆ A, Aeff ⊆ A, and T ⊆ S ×Atr ∪{ }×P(Aeff )×S.
A state machine consists of a set of states, two alphabets, and a transition relation between the states. For a transition t ∈ T with t = (s,tr ,eff ,s0), s is the source state of the transition, s0 is the target state, tr is a symbol (trigger) which upon receipt triggers the execution of the transition, and eff is a set of symbols (effects) that are sent when the transition is executed. The trigger symbol can be the special symbol ∈6 A standing for an empty trigger. A transition containing can be triggered no matter whether any symbol is received. In order for the execution of the transition to finish, each symbol in eff must be received by a different state machine. In Fig. 1, state machine Student contains states S = {working,desperate,waiting}, triggers Atr = {coffeeDone, error} and effect Aeff = {orderCoffee}. An example for a transition is (working, ,{orderCoffee},waiting).
In order to give a precise semantics of the interaction between state machines, we introduce the notion of an extended state machine.
Definition 2 (Extended State Machine). Given a state machine M = (S,ι,Atr ,Aeff ,T ), the extended state machine M ∗ is a quintuple (S ∪S∗,ι,Atr ,Aeff ,T ∗) where S∗ = {st∗ | t ∈ T } and T ∗ = {(s,tr ,∅,st∗),(st∗, ,eff ,s0) | t = (s,tr ,eff ,s0) ∈ T }.
An extended state machine introduces an intermediate state st∗ for each transition t. This intermediate state has one incoming transition, which is triggered by the trigger of t and has no effects. It also has one outgoing transition, which leads to the target state of t with as trigger and the effects of t. The states contained in S∗ we call extended states. Fig. 2 depicts the extended state machine constructed from state machine Student in Fig. 1. The reason for the construction of an extended state machine is to distinguish between the event of having received the trigger and the event of being able to send the effects.
The communication between state machines takes place through a structure called message set. A message set contains a sender state machine and a set of pairs, each containing a symbol sent by the sender state machine and a receiving state machine. Each of the symbols is sent by the same state machine but received by a different state machine. This is captured in the following definition.
Definition 3 (Message Set). Given a set M = {M1∗,...,Ml∗} of extended state machines with Mi∗ = (Si,ιi,Atir ,Aieff ,Ti) for 1 ≤ i ≤ l, a message set is a pair (σ,{(a1,R1∗),...,(ak,Rk∗)}) where – σ = Md∗ with 1 ≤ d ≤ l and – {(a1,R1∗),...,(ak,Rk∗)} ∈ P(Aedff ×M\{σ}) such that for 1 ≤ i ≤ k all Ri∗ are pairwise distinct.
For a message set (σ,{(a1,R1∗),...,(ak,Rk∗)}), σ is an extended state machine which executes a transition leaving an extended state with the set {a1,...,ak} of effects, and for each 1 ≤ i ≤ k, Ri∗ is an extended state machine which executes a transition leaving an original (non-extended) state through trigger ai. Note that {(a1,R1∗),...,(ak,Rk∗)} can be the empty set, which represents an empty set of effects on a transition.
A message set can be admissible in some global configuration. Such a configuration is given by a global state, a tuple of states containing exactly one state per state machine. By applying a message, a global successor state is reached.
Definition 4 (Application of a Message Set). Given a set of extended state machines M = l } with Mi∗ = (Si,ιi,Atir ,Aeiff ,Ti) for 1 ≤ i ≤ l, and a global state ˆs= (s1,...,sl) ∈ {M1∗,...,M ∗ S1 ×···×Sl, a message set m = (Md∗,{(a1,R1∗),...,(ak,Rk∗)}), with 1 ≤ d ≤ l and 1 ≤ k < l, is admissible in ˆs if (i) (sd, ,{a1,...,ak},s0d) ∈ Td, and (ii) there exists a set R ⊆ {1,...,l}\{d} and a bijective function rec : {1,...,k} → R such that Rj∗ = Mr∗ec(j) and (srec(j),aj,∅,s0rec(j)) ∈ Trec(j) for each 1 ≤ j ≤ k. Given a global state ˆs and a message set m that is admissible in ˆs, a global successor state ˆs0 of ˆs after applying m is given by ˆs0 = (next(s1),...,next(sl)) where next(si) = s0 d s0 i si if i=d if i ∈ R otherwise
There are two requirements for a message set to be admissible in a global state: (1) the sender’s state in the global state is an extended state with an outgoing transition containing the set {a1,...,ak} of effects, and (2) each receiver’s state in the global state has an outgoing transition triggered by the respective symbol from the message set. Note that we are dealing with extended state machines, which means that a transition cannot carry a trigger symbol other than together with a non-empty set of effects. Therefore it can never happen that a receiver state machine Ri∗ sends any effects while executing the transition triggered by some symbol ai. The global successor state ˆs0 is reached by applying a message set. It differs from ˆs in states of the sender and the receiver state machines contained in the applied message set: The sender’s state changes from an extended state to its only successor state, and the receivers’ states change according to the received symbol into an extended state.
We combine message sets of disjoint sets of state machines in a transaction as follows. Definition 5 (Transaction). A transaction is a nonempty set of message sets {m1,...,ml} with mi = (σi,{(ai,1,Ri∗,1),...,(ai,ki ,Ri∗,ki )}) such that all state machines occurring in the message sets, i. e., all σi and Ri∗,j (with 1 ≤ i ≤ l,1 ≤ j ≤ ki), are pairwise distinct. A transaction is admissible if all its message sets are admissible. The global state reached by applying a transaction is the global state reached by applying each of its message sets.
We further define a path as a sequence of transactions as follows.
Definition 6 (Path). A path μ from a global state ˆs0 to a global state ˆsk is a sequence μ = [n1,...,nk] of transactions such that there exists a sequence [ˆs0,...,ˆsk] of global states where for all 1 ≤ i ≤ k, ni is admissible in state ˆsi−1 and ˆsi is the global successor state of ˆsi−1 after applying ni.
A global state ˆsj is reachable from ˆsi if there is a path from ˆsi to ˆsj. The length of a path is the number of its transactions.
The k-GSC problem deals with reaching a combination of states of state machines in a state machine view. This combination contains at most one state of each state machine. Hence such a combination not necessarily specifies a complete global state. We therefore define a partial global state as follows.
Definition 7 (Partial Global State). Given a set M = {M1∗, ... , Ml∗} of extended state machines with Mi∗ = (Si,ιi,Atir ,Aieff ,Ti) for 1 ≤ i ≤ l, a partial global state is an l-tuple ˆsp ∈ S1 ∪{?}×···×Sl ∪{?}, where ? is a new symbol not contained in any Si. ˆsp = (s1,...,sl) matches a global state ˆs= (q1,...,ql) if for all 1 ≤ i ≤ l, si = qi whenever si =6 ?.
Finally, we define the k-GSC problem as follows. k-GSC Instance: A set M of state machines, a global state ˆs, and a partial global state ˆsp. Question: Is there a path of length at most k from ˆs to a global state ˆs0 that matches ˆsp? The global state ˆs is also referred to as initial state and the partial global state ˆsp is also referred to as goal. The initial state usually contains each state machine’s initial state. 4
In order to find solutions to the k-GSC problem, we propose to encode it to the satisfiability problem of propositional logic (SAT) and hand it to a SAT solver. In the following we present a detailed description of the SAT formula representing the k-GSC problem. In the next section we describe our tool, the Global State Checker, which builds upon this encoding.
Let k be a positive integer, ˆs a global state representing an initial state, and ˆsp a partial global state representing a goal. Then the formula ϕ is satisfiable if and only if there is a global state ˆs0 that is reachable from ˆs by a path of length at most k and that matches ˆsp.
Recall that in a k-GSC instance we are given a set M = {M1, ... , Ml} of state machines, a global state ˆs = (x1, ... , xl), and a partial state ˆsp = (g1, ... , gl). For each 1 ≤ i ≤ l let Mi = (Si, ιi, Atir , Aeff , Ti) and the corresponding extended state machine i be Mi∗ = (Si ∪Si∗,ιi,Atir ,Aeiff ,Ti∗).
In order to define the set of variables of ϕ, we introduce a set T := S1≤i≤l Ti of transitions, a set A := S1≤i≤l Atir ∪Aieff of symbols, a set S := S1≤i≤l Si of states, and a set S∗ := S1≤i≤l Si∗ of extended states. Then the set of variables is given by {vi | v ∈ (T ∪ A ∪ S ∪ S∗), 0 ≤ i ≤ k} were i is an index capturing the relative position of the variable in the path. That is, each transition, symbol, state, and extended state together with one index up to k represents a variable.
Let t = (s,tr ,eff ,s0) be a transition of a state machine and (s,tr ,∅,st∗) and (st∗, ,eff ,s0) be the corresponding transitions in the respective extended state machine. To simplify the presentation, we use the functions src(t) := s, int(t) := st∗, trg(t) := tr , eff(t) := eff , and tgt(t) := s0.
Further let T ∗ := S1≤i≤l Ti∗. Given a state s ∈ S, let environ(s) := {s∗ | (s∗, ,∅,s) ∈ T ∗}∪{s∗ | (s, ,eff ,s∗) ∈ T ∗} be a set of extended states containing a predecessor of s if the transition does not contain any effects and a successor of s if the transition contains as trigger.
The formula ϕ is then given by a conjunction of the following subformulas: ti → src(t)i ∧int(t)i+1 ∧trg(t)i ∧trg(t)i+1 ∧
^ eff i ∧eff i+1 → si ∧si+1 →
_ t∈T ,s=src(t) int(t)i ∧int(t)i+1
→ int(t)i ∧int(t)i+1 → t∈T ,eff ∈eff(t) _ ti
ti . The intuition behind these subformulas is as follows: ϕinit initialises the path by setting the initial states with index 0 to true, and all other states and all symbols to false. ϕgoal encodes the goal states and the extended states in their environment for index k. For all other path indices, a symbol variable in its positive polarity means that the respective symbol has been made available as effect through the transaction at the respective index and is waiting to be consumed by some transition as a trigger in a later transaction. When the symbol has been consumed, the respective symbol variable occurs in its negative polarity. ϕ1 ensures that whenever a transition is executed, the state machine changes to the respective extended state. Then the trigger symbol is set its negative polarity and the effect symbols are set to their positive polarity. ϕ2 and ϕ3 express that whenever the polarity of a symbol is changed, there must be a transition causing this change. ϕ4 encodes that leaving a state is always caused by some transition. ϕ5 and ϕ6 ensure that after executing a transaction either all effect symbols of a transition are consumed or none of them. The formulas ϕj with j ∈ {2,...,5} are also called framing axioms. These formulas ensure that every change in a global state has a cause. Note that it is not necessary to state all changes explicitly, because they are already covered implicitly by other formulas. ϕ7 forces a machine to move to the target state if all effect symbols have been consumed. ϕ8 expresses that each machine is in exactly one state after each transaction.
Note that the encoding allows that nothing happens, i. e., no transaction takes place at an index. It is ensured by the framing axioms that in this case, the global state remains the same. This relaxation implicitly encodes the “at most k” formulation of the problem: If at n indices nothing happens and the goal is reached at index k, it means that the length of the transaction sequence is k −n. The framing axioms also ensure that state machines not participating in a transaction do not change.
A solution returned by the SAT solver consists of a set of variables set to true. By extracting those variables that represent states and transitions (sets S, S∗, and T ) we obtain a path to the goal. If the length of the path is less than k, then for some consecutive indices the state variables represent the same states. The shorter path can therefore be easily extracted.
In order to simplify the encoding we assume that after applying a transaction each symbol
can be consumable only once. Allowing a symbol to be consumable multiple times after one
transaction requires the integration of counters, which can be realized, e.g., by building upon
ideas presented in [
We have implemented the encoding described above as Eclipse plugin5 and designed a set of
instances for an initial case study. Our prototype implementation is available on our Eclipse
update site6. Further resources and instructions can be found on our project website7. In the
following, we shortly describe our implementation and discuss a first case study.
Implementation. The Global State Checker prototype is embedded into the Eclipse modeling
framework (EMF). The metamodel for the statemachine view described in Sec. 3 is provided
by an Ecore metamodel. Instances of the k-GSC problem are created as models of the defined
language. Our encoder module takes a state machine view as input and encodes it into a
formula of propositional logic according to the encoding described in Sec. 4. Additional
measures are taken to convert the formula into conjunctive normal form (CNF), which is a
common format used by SAT solvers. The data structure representing the encoding is handed
to the SAT4J [
Fig. 3 shows the graphical user interface of our prototype. The user can select a set of states directly in the modeling editor, enter a bound, and start the k-GSC tool. For convenience, it may be specified whether the given global state is expected to be reachable or not. Red or green highlighting indicate how the expected result compares to the effective result. All test cases are listed in the global state checker console. The expanded subitems of the third test case in Fig. 3 show the path found by the SAT solver.
Case Study. We have designed three different benchmark instances with varying number of
state machines, states, and transitions in order to test our prototype. The instances have been
adapted from our previous work [
For all test cases, ˆs (the starting state of the path) has been set to the global initial state, i.e., the global state where each state machine is in its initial state. For instances “coffee” and “mail,” each possible combination of states for each state machine, and for the instance “philosophers” a meaningful selection of combination of states have been tested with the bound k set to {3,15,100}. Details on the outcomes of the test cases are presented on our project website. The results of all test cases are as expected. The bugs in the erroneous versions have been found. The approach performs well up to a bound of k =1000. In Fig. 4 we exemplarily show the runtime measures for the coffee machine instance, which were evaluated on an Intel Core i5 CPU with 2.5 GHz running Linux. The red lines show a test case in which the goal was a partial global state containing a state of one out of three state machines, and the blue lines show a case where the goal was a complete global state, i.e., containing a state of each state machine. The dashed lines express the time needed to encode the problem and the solid lines give the total time, i.e., encoding time plus time spent by the SAT solver. As can be expected, the bottleneck for higher bounds is the task of solving the SAT instance. 6
We presented a SAT-based approach to verify whether a combination of states in the state machine view of a software model can be reached through a path of bounded length from an initial configuration. Using SAT allowed for a more direct translation than, e.g., using a model checker, and for a good integration within our existing framework which is implemented as plugin for the popular development environment Eclipse and therefore easily accessible to developers. We precisely defined the semantics of the state machine view of a software model. On this formal semantics we could build a formal problem definition. Based on this problem definition, the encoding to SAT turned out to be very intuitive, easy to understand and therefore easy to extend.
Immediately planned extensions of our encoding include the integration of a counter to
handle the availability of multiple occurrences of a symbol representing an effect. Another
important task is the optimization of the encoding in order to avoid unnecessary blowups and
yield a more compact representation. On a longer time frame, the integration of transition
guards and hierarchical state machines are planned. Before extending our approach, however,
more extensive testing as well as a runtime comparison to alternative encodings will be
necessary. To thoroughly test the tool, we will implement a solution verifier to automatically
verify the solution returned by the SAT solver and apply our previously used approach of
grammar-based fuzzing for MBE tools [