In this paper, we consider incremental development of state transition diagrams by adding features, which add new states and transitions. The goal is to capture when properties of a state transition diagram are preserved when adding a feature. We classify several typical cases of such state transition diagram extensions and show when commonly used properties are preserved. In some cases, we add restrictions to the input events. In others, we need to transform properties to account for new failure cases. Properties are specified on the externally visible input and output events. To formalize the properties and to reason about internal state transition diagram extensions we use a computation tree logic with states and events.
/)Issue)1cket) )/)done) /)conf) /)Issue)1cket)
Refining)Transi1ons) Feature-based Development of State Transition Diagrams with Property Preservation credit)
Adding)failures) /)credit)check) issued eventually)•i s not preserved, as the loop m)ay be traversed infinitely many □(!"#$" →+ ◊%&" %"'()&" ) times. Next, consi•d er Figure 4, which adds two new failure path) s. In this case, the above property tOhaRt)□a(t!i"c#ke$t"i→si◊s(su(#ed3 (is&4no%5t6pr%%es&e"r%v"e'(d).&W")e %h)ave two options here. As the first option, we may assume that such a failure does not occur. Alternatively, we may also transform the property to account for this new case.
More precisely, we consider the case where an SD is extended by a new feature, which adds new states and transitions. We classify several typical cases of such SD extensions and show when commonly used properties are preserved. In some cases, we also transform properties to account for new failure cases.
Our approach is, on a conceptual level, similar to adding aspects on a
programming language level. For this, [
We formalize properties in a specific computation tree logic (CTL) which
considers both states and events, following the logic in [
There exists ample work on refinement for SDs, e.g. [
Other work on modularity for model checking [
We model software systems by SDs, which we formalize as labeled transition systems.
Definition 1 (Labelled Transition System). A labelled transition system (or LTS) is a structure L = (S, s0, A, →) where – S is a set of states. – s0 ∈ S is the initial state. – Two disjoint sets I and O of input and output events and the silent event τ is not in I nor O. – Pairs of input and output events A = (I ∪ {τ }) × (O ∪ {τ }), called labels. – →⊆ S × A × S is the transition relation; an element (r, α, s) ∈→ is called a transition, and is usually written as r −→α s.
To model practical examples we use explicit labels with a pair of input and output events. We write (s, (i, o), s0) or (s, α, s0), where α = (i, o), for transitions. We let Aτ = A ∪ {τ }. We let α, β, . . . range over Aτ . As I and O are disjoint, we also write i instead of (i, τ ) and o instead of (τ, o).
Let L = (S, s0, A, →) be an LTS. A sequence (s0, α0, s1)(s1, α1, s2) . . . ∈→∞ is called a path from s0; if a path cannot be extended anymore because it is either infinite or ends in a state without outgoing transitions, it is called a maximal path. We write statei(π) for the i’th state of the path, i ≥ 0. We write eventi(π) for the i’th event of the path, i ≥ 0.
In the following, we briefly introduce a computation tree logic (CTL) based on both states and events. This is needed as we aim to separate the external view on an SD, in terms of events, and the internal view in terms of states, as discussed below.
Our logic, called ESCTL, is a special case of the UMC logic presented in [
Definition 2 (ESCTL). The syntax of the logic ESCTL(Event/State-based CTL) is defined by the following grammar where we let φ, φ0, . . . range over ESCTL-state formulas: φ ::= T | s | ¬φ | φ ∧ φ0 | Eϕ | Aϕ where s ∈ S and ϕ is a path formula. ESCTL-path formulae are formed according to the following grammar: ϕ ::= Xφ | Xχφ | φχUχ0 φ0 | φχWχ0 φ0 where φ and φ0 are ESCTL-state formula and χ and χ0 are event formulae. An event formula is defined by the following grammar where we let χ, χ0 range over event formulas: χ ::= true | α | ¬χ | χ ∧ χ0
In the following we will say state and path formula instead of ESCTL-state and ESCTL-path formula.
Let L = (S, s0, A, →) be an LTS. The satisfaction relation |= between states
s ∈ S and state formulae is defined as usual. For a detailed treatment, we refer
to [
We define the usual operators F and G, as well as Fχ, for a event χ, as follows: F = ¬T, EF φ = E(TtrueU φ), AF φ = A(TtrueU φ), EFχφ = E(TtrueUχφ), EFχ = E(TtrueUχT ), AGφ = ¬EF ¬φ, AGχ = ¬EF¬χ, EGφ = AG¬φ, E(ϕφU ϕ0) = ϕ0 ∨ E(ϕφUφϕ0). Without ambiguity, we omit T in formulae. Similarly, we write eUχ instead of TeUχ.
Note that our combined event/state logic treats events and state separately, and many properties on states are easier to formalize than similar ones on events. For instance consider a property state s implies state s0; we denote this as AG(s → AF s0), which is defined as AG(¬s ∨ AF s0). On the other hand, an event e implies P is denoted as AG(e → P ), defined as AG((Xe(AF P )) ∨ X¬eT ). 3
In the following, we first motivate our specifications in state/event logic and then classify properties on SDs. This is followed by a detailed analysis of SD composition for different cases.
We use our event/state logic in order to specify externally visible behavior and internal behavior, respectively. Assume an SD S and a set of input traces I consisting only of input events.
– We express properties on externally visible behavior by properties on input and output events. No formulae with states are permitted, as these are considered internal. – (Full) behavior specifications use properties over states, input and output events created by S, using all of the above.
One reason why we use externally visible events for behavior is that two composed SDs may share input or output events. This is not possible if only names of states are considered. On the other hand, we need states to reason about internals of a composition, as discussed below. 3.1
Specification Patterns
Our goal is to study what properties are preserved when adding a new feature
to an SD. For the properties to consider, we use the specification patterns as in
[
In this paper, we hence focus on leads to or response properties. Together
with the invariants, this covers a significant amount of specifications. The other
pattens in [
SD Composition
In the following, we define formally how to extend an SD by a new feature.
We also use SDs to denote such extensions, which are then glued together at
specified join states. Based on join states, similar to join points in aspect-oriented
languages, we use graphical notation to denote the composition of SDs. For a
more formal definition, we refer to [
For adding a new path, consider the schematic view in Figure 5. By convention, the SD E in red color represents the path to be added to the blue, base SD S. We assume that E and S have disjoint states, and further that E has initial state s0 and a state j0. In S, we assume a start state s and a join state j for adding a path. The two SDs will be composed by merging these two states, s0 and j0, with the states s and j, respectively. This is denoted by the light dashed lines. In the merged state, we use the states s and j for these. Formally, the states s0 and j0 are renamed to s and j in E, and the two SDs are then merged to obtain S ∪ E. Note that we do not use the same names for the states i and j in S and E to be merged in order to avoid confusion when expressing preconditions on E or S.
We also consider refinement of transitions as follows. We write S − E, where E denotes a set of transitions in S which are removed. Based on this, we can express transition refinement by S − E ∪ E0 as shown in Figure 3. If E removes a single transition for which a corresponding path with same start and end states and the same trigger event in the first transition in this path, then we denote this as a transition refinement by S ∪r E0 and leave E implicit (without ambiguity).
Adding)alterna1ve)paths) ...)
/)b) j) The main goal of this section is to define rules for the extension of an SD. As defined above, assume an SD S which is extended to S ∪ E by an extension E. The goal is now to define criteria when a property for S, e.g. S |= P , also holds for S ∪ E, i.e., S ∪ E |= P .
This achieves modularity on properties w.r.t. extension, and also simplifies formal proofs as S ∪ E is larger than S and E. Furthermore, we will see that many properties can be obtained easily by local analysis of the state diagram. We should observe also that some properties are not preserved by extensions. For this, we will transform the properties into extended properties with extra conditions.
Adding Alternative Paths We consider the schematic view of adding an alternative path in Figure 5. We use the states s, s0 and j, j0 as shown in this figure. However, the schematic case as in Figure 5 is simplified for illustration and does not show all cases covered by this rule. More precisely, this case is specified by the following assumptions: First, there is a path from s to j in S, i.e., S |= AG(s → EFj ). This means that j is reachable from s on at least one path; thus we add an alternative path to this. Second, E |= AG(s0 → AFj0 ). This means that j0 is reached eventually when entering E. Furthermore, we assume s 6= j to avoid trivial loops which are covered in a separate case below. Third, we assume that j0 is a final state in E. Hence we have no newly added infinite loops and termination only in state j for E.
We consider first a property of the form AG(a → AFb). The main idea here is to identify cases when an alternative path does not obstruct this property. In other words, the event b is observed in any path after a, even with the new alternative path.
Assuming S, E with states s, s0 and j, j0 as specified above for Figure 5. In case S |= AG(a → AFb) holds for S, we obtain S ∪ E |= AG(a → AFb) if one of the following holds: – S |= AG(a → (¬sUb)) – or S |= AG(s → (¬jWb)) – or E |= AG(s0 → AFb). Adding)failures)
Adding)fallback)paths) ...) a) ...).)
j) j‘) □(# →◊8 )) □A(d#di→ng◊a8F)a)ilure Path We consider the schematic view of adding a failure path in Figure 6. The assumptions for) this case are as follows: there is a failure )event c which occurs in E, E is entered by event e and furthermore that there is no paths back to the SD S. Formally, we have no j0 in this case and E |= AG(e → AFc).
In case of leadsto properties, we have several cases. The base case happens when the property is not affected by the failure, i.e., if the added path is not taken before b, formally a → (¬sUb). Then, we have the case that b always occurs in E, similar to above.
If these simple cases do not hold, we have the option to weaken the property. Assuming S |= AG(a → AFb) and AG(E |= e → AFc), we obtain S ∪ E |= AG(a → AFc∨b).
Adding Fallback Paths The idea of a fallback path is that a new path is added, similar to the alternative path case. Here, the new path leads to a state already traversed earlier. Thus we fall back to an earlier state and create a possible loop, which is different from the above cases.
We consider the schematic view of adding an alternative path in Figure 7. As above, the SD E in red color represents the path to be added to the blue, base SD S, with join states s and j. We assume that E has initial state s0 and a final state j0.
The fallback case, as illustrated schematically in Figure 7, is specified by the following assumptions: First, there is a path from j to s in S, i.e., S |= AG(j → EFs). Secondly, E |= AG(s0 → AFj0 ). Third, j0 is a final state in E. The main problem in this case is that the fallback path adds a loop which may be traversed infinitely often.
Consider a response property of the form a leads to b. The main idea here is to identify cases when an alternative path does not obstruct this property. In other words, the event b is observed in any path after a, even with the new alternative path.
Assuming S, E with states s, s0 and j, j0 as specified above for Figure 7. Assuming S |= AG(a → AFb), we obtain S ∪ E |= AG(a → AFb) if – S |= AG(a → (¬sWb)) – or E |= AG(s0 → AFb).
For adding a fallback path, we have another important case. If we can avoid non-termination by the added loop of the fallback path, we can also establish
Adding)looRpse)fine)Transi1on)=)Add)+)Delet ) □th(e#de→sir◊ed8 p)roperty. It is sufficient to □ex(p#re→sst◊h8at)i)n state s, the input e does )not occur infinitely often.
The problem is that we cannot exp)ress such fairness properties in a
CTLlogic. We can formalize this as S ∪ E |= ¬AG(s ∧ Xe), but this is a CTL*
formula and not a CTL formla. Fortunately, for our state/event logic, there
also exists an extension, including model checking, for the μ-calculus, which can
embed CTL* [
Refining Transitions In this case, a transition is refined into several new states and new transitions. This is typical when moving from a higher level model to a more detailed model, which shows more details by refining a transition into several transitions. Note that removing transitions is a special case of this refinement. An example is shown in Figure 9.
The schematic case is illustrated in Figure 9. Formally, it is specified by the following assumptions: First, there is a transition from s to j in S. Second, E |= AG(s0 → Aj0 ). This means that j is reached eventually when entering E. Hence we have no infinite loops and termination only in state j. Refining a transition could be modeled by removing a transition and adding a new path; for refinement it is however more effective to consider this in conjunction.
We consider first a property of the form a → AFb. The main idea here is to identify cases when the added path does not obstruct this property. In other words, the event b is observed in any path after a, even with the new alternative path.
Assuming S |= AG(a → AFb), we obtain S ∪r E |= AG(a → AFb) if – S |= AG(a → (¬sWb)) – or S |= AG(s → (¬jWb)) – or E |= AG(s0 → AFb).
The cases above are as in the case of adding a transition: In the first case, (¬sU b) means s never happens before b. Hence b occurs always before the alternative path is taken. In the second case, s → (¬jWb) means this: if s happens, then b happens after j. This is to avoid the case that b only occurs between s and j. Finally, E |= AG(s0 → AFb) means that b happens in E when the path is taken. Hence the property also holds for the combined SD.
Putting things together In the following, we apply the above results to the example in the introduction. We consider the base SD as in Figure 1 and the property AG(start → AFIssue ticket). Combining the examples from Section 1, we obtain the SD in Figure 10 1. Adding the voucher option in Figure 1 preserves this property. 2. Adding the discount option in Figure 2 does not preserve this property. Assuming a fairness precondition, this turns into AG(start → AFIssue ticket). More formally, we need to assume in the following that enter discount does not occur infinitely often in sequence. 3. Refining the credit transition in Figure 3 preserves this last property. 4. Adding the failure cases as in Figure 4 does not preserve this property. We need to weaken the property as follows: AG(start → AFdeclined∨cancel∨Issue ticket), assuming the above fairness precondition regarding enter discount. 4
In this paper, we have presented a new approach for incremental development of state transition diagrams. We have developed a classification of individual features to be added to an SD, and then discussed when properties can be established. In some failure cases, we had to modify the properties to account for failure cases. In case of loops, we may need a notion of fairness for some properties. The conditions for the rules only assume properties of the SDs to be composed, which means that the rules are modular. Hence, one benefit is that we can validate the rules more efficiently. In many cases the conditions can be checked by simple analysis on the SD level.
We have formalized our rule by using a recently developed Event/State CTL
logic. This permits us to express properties on externally visible behavior in
terms of input and output events, while expressing composition conditions by
internal states. We have validated our rules by several examples in a workflow
example. We assume that our rules and examples are easy to express in a model
checker for our state/event logic, e.g. in the UMC tool [
The main novelty is to focus on different kinds of properties individually, which permits new ways for incremental development. Regarding other works on refinement, we note that usual notions of refinement preserve all properties, which is too strong for our case. Further work will address other patterns of property specifications, also including different scopes.
Acknowledgements The author would like to thank Sebastian Bauer, Martin Wirsing, Franco Mazzanti and Rolf Hennicker for stimulating discussions.