In this paper, we use UML Interaction Overview Diagrams as the basis for a user-friendly, intuitive, modeling notation that is wellsuited for the design of complex, heterogeneous, embedded systems developed by domain experts with little background on modeling softwarebased systems. To allow designers to precisely analyze models written with this notation, we provide (part of) it with a formal semantics based on temporal logic, upon which a fully automated, tool supported, verification technique is built. The modeling and verification technique is presented and discussed through the aid of an example system.
Complex embedded systems such as those found in the Aerospace and Defense domains are typically built of several, heterogeneous, components that are often designed by teams of engineers with different backgrounds (e.g., telecommunication, control systems, software engineering, etc.). Careful modeling starting from the early stages of system development can greatly help increase the quality of the designed system when it is accompanied and followed by verification and code generation activities. Modeling-verification-code generation are three pillars in the model driven development of complex embedded systems; they are most effective when (i) modeling is based on user-friendly, intuitive, yet precise notations that can be used with ease by experts of domains other than computer science; (ii) rigorous, possibly formal, verification can be carried out on the aforementioned models, though in a way that is hidden from the system developer as much as possible; (iii) executable code can be seamlessly produced from verified models, to generate implementations that are correct by construction.
This work, which is part of a larger research effort carried out in the MADES European project1 [1], focuses on aspects (i) and (ii) mentioned above. In particular, it is the first step towards a complete proposal for modeling and validating embedded systems. The plan is to exploit both “conventional” UML diagrams 2 [15] and a subset of the MARTE (Modeling and Analysis of Real-Time and Embedded systems) UML profile [14]. We want to use Class Diagrams to define the key components of the system. State Diagrams to model their internal behaviors, and Sequence and Interaction Overview Diagrams to model the interactions and cooperations among the different elements. These diagrams will be augmented with clocks and resources taken from MARTE. The result is a multi-faceted model of the system, automatically translated into temporal logic to verify it. Temporal Logic helps glue the different views, create a single, consistent representation of the system, discover inconsistencies among the different aspects, and formally verify some global properties.
This paper starts from Interaction Overview Diagrams (IODs) since they are often neglected, but they provide an interesting means to integrate Sequence Diagrams (SDs) and define coherent and complex evolutions of the system of interest. IODs are ascribed a formal semantics, based on temporal logic, upon which a fully automated, tool supported, verification technique is built.
The choice of IODs as the starting point for a modeling notation that is accessible to experts of different domains, especially those other than software engineering, is borne from the observation that, in the industrial practice, SDs are often the preferred notation of system engineers to describe components’ behaviors [3]. However, SDs taken in isolation are not enough to provide a complete picture of the interactions among the various components of a complex system; hence, system designers must be given mechanisms to combine different SDs into richer descriptions, which is precisely what IODs offer.
IODs cannot be used to perform the kind of rigorous analysis that is crucial throughout the development of critical systems such as those typical of the Aerospace and Defense domains unless they are given a precise semantics. To this end, in this article we provide a preliminary formal semantics of IODs based on metric temporal logic. While this semantics is not yet complete, as it does not cover all possible mechanisms through which SDs can be combined into IODs, it is nonetheless a significant first step in this direction. The provided semantics has been implemented into the Zot bounded satisfiability/model checker [16]2, and has been used to prove some properties of an example system.
This paper is structured as follows. Section 2 briefly presents IODs; Section 3 gives an overview of the metric temporal logic used to define the formal semantics of IODs, and of the Zot tool supporting it; Section 4 introduces the formal semantics of IODs through an example system, and discusses how it has been used to prove properties of the latter; Section 5 discusses some relevant related works; finally, Section 6 draws some conclusions and outlines future works. 2
Most UML behavioral diagrams have undergone a significant revision from version 1.x to version 2.x To model interactions, UML2 offers four kinds of diagrams: 2 Zot is available at http://home.dei.polimi.it/pradella. 3 communication diagrams, sequence diagrams, timing diagrams and interaction overview diagrams. In this work we focus on Sequence Diagrams (SDs) and Interaction Overview Diagrams (IODs).
SDs have been considerably revised and extended in UML2 to improve their expressiveness and their structure. IODs are new in UML2. They allow a designer to provide a high-level view of the possible interactions in a system. IODs constitute a high-level structuring mechanism that is used to compose scenarios through mechanisms such as sequence, iteration, concurrency or choice. IODs are a special and restricted kind of UML Activity Diagrams (ADs) where nodes are interactions or interaction uses, and edges indicate the flow or order in which these interactions occur. Semantically, however, IODs are more complex compared to ADs and may have different interpretations. In the following the fundamental operators of IODs are presented. Figure 2 shows an example of IOD for the application analyzed in Section 4, which will be used throughout this Section to provide graphical examples of IOD constructs. IODs include also other operators whose study is left to future works.
In IODs these operators have exactly the same meaning of the corresponding operators found in ADs.
An initial node is a type of control node which initiates flow in a IOD. It has no incoming flows and one or more outgoing flows. The outgoing flows may be guarded with conditions that determine if they will accept tokens. When a IOD starts, tokens are offered to all outgoing flows of the initial node.
A final node is a node that stops a IOD. When a token arrives at a final node all flows in the enclosing activity are stopped and the IOD is terminated. The token arriving at the final node is destroyed.
Finally, a flow final node is a type of final node that consumes the incoming token. When a token arrives at a flow final node the token is consumed and nothing else in the IOD is affected.
The IOD of Figure 2 has an initial node at the top, but no final or flow final nodes. 2.2
A control flow is a directed connection (flow) between two SDs (e.g., between diagrams delegateSMS and downloadSMS in Figure 2). As soon as the SD at the source of the flow is finished, it presents a token to the SD at the end of the flow. 2.3
A fork node is a control node that has a single incoming flow and two or more outgoing flows. Incoming tokens are offered to all outgoing flows (edges). The 4 outgoing flows can be guarded, which gives them a mechanism to accept or reject a token. If one of the outgoing flows accepts the token, the token is duplicated for that flow. In this work we do not deal with guards, but this is a rather straightforward extension that we will consider in the future. In the IOD of Figure 2, there is one fork node at the top of the diagram (between the initial node and SDs waitingCall and checkingSMS ) modeling two concurrent execution of the system.
The dual operator is the join node, which synchronizes a number of incoming flows into a single outgoing flow. Each (and every) incoming control flow must present a control token to the join node before the node can offer a single token to the outgoing flow. 2.4
A decision node is a control node that has one incoming flow and two or more outgoing flows. When a token arrives at a decision node it is offered to all the outgoing flows, one (and only one) of which accepts the token. In the IOD of Figure 2 there are four decision operators (e.g., the one between SDs waitingCall and delegateCall ) with their corresponding boolean conditions.
Conversely, the merge node is a type of control node that has two or more incoming flows and a single outgoing flow. It is used to reunite alternative flows that originate from one or more decision nodes. The merge node accepts a token on any one (and only one) of the incoming flows and passes it to the single outgoing flow. 3
TRIO and Zot TRIO [7] is a general-purpose formal specification language suitable for describing complex real-time systems, including distributed ones. TRIO is a first-order linear temporal logic that supports a metric on time. TRIO formulae are built out of the usual first-order connectives, operators, and quantifiers, as well as a single basic modal operator, called Dist, that relates the current time, which is left implicit in the formula, to another time instant: given a time-dependent formula F (i.e., a term representing a mapping from the time domain to truth values) and a (arithmetic) term t indicating a time distance (either positive or negative), the formula Dist(F, t) specifies that F holds at a time instant whose distance is exactly t time units from the current instant. Dist(F, t) is in turn also a time-dependent formula, as its truth value can be evaluated for any current time instant, so that temporal formulae can be nested as usual. While TRIO can exploit both discrete and dense sets as time domains, in this paper we assume the standard model of the nonnegative integers N as discrete time domain. For convenience in the writing of specification formulae, TRIO defines a number of derived temporal operators from the basic Dist, through propositional composition and first-order logic quantification. Table 1 defines some of the most significant ones, including those used in this paper.
Operator
Definition Past(F, t) t ≥ 0 ∧ Dist(F, −t) Futr(F, t) t ≥ 0 ∧ Dist(F, t) Alw(F ) ∀d : Dist(F, d) AlwP(F ) ∀d > 0 : Past(F, d) AlwF(F ) ∀d > 0 : Futr(F, d) SomF(F ) ∃d > 0 : Futr(F, d) SomP(F ) ∃d > 0 : Past(F, d) Lasted(F, t) ∀d ∈ (0, t] : Past(F, d)
Lasts(F, t) ∀d ∈ (0, t] : Futr(F, d) WithinP(F, t) ∃d ∈ (0, t] : Past(F, d) WithinF(F, t) ∃d ∈ (0, t] : Futr(F, d) Since(F, G) ∃d > 0 : Lasted(F, d) ∧ Past(G, d) Until(F, G) ∃d > 0 : Lasts(F, d) ∧ Futr(G, d)
The TRIO specification of a system consists of a set of basic items, which are primitive elements, such as predicates, time-dependent values, and functions, representing the elementary phenomena of the system. The behavior of a system over time is formally described by a set of TRIO formulae, which state how the items are constrained and how they vary, in a purely descriptive (or declarative) fashion.
The goal of the verification phase is to ensure that the system S satisfies some desired property R, that is, that S |= R. In the TRIO approach S and R are both expressed as logic formulae Σ and ρ, respectively; then, showing that S |= R amounts to proving that Σ ⇒ ρ is valid.
TRIO is supported by a variety of verification techniques implemented in prototype tools. In this paper we use Zot [16], a bounded satisfiability checker which supports verification of discrete-time TRIO models. Zot encodes satisfiability (and validity) problems for discrete-time TRIO formulae as propositional satisfiability (SAT) problems, which are then checked with off-the-shelf SAT solvers. More recently, we developed a more efficient encoding that exploits the features of Satisfiability Modulo Theories (SMT) solvers [2]. Through Zot one can verify whether stated properties hold for the system being analyzed (or parts thereof) or not; if a property does not hold, Zot produces a counterexample that violates it. 4
This section introduces the formal semantics of IODs defined in terms of the TRIO temporal logic. The semantics is presented by way of an example system, whose behavior modeled through a IOD is described in Section 4.1. Then, Section 4.2 discusses the TRIO formalization of different constructs of IODs, and illustrates how this is used to create a formal model for the example system. Finally, Section 4.3 briefly discusses some properties that were checked for the modeled system by feeding its TRIO representation to the Zot verification tool. 4.1
The example system used throughout this section is a telephone system composed of three units, a TransmissionUnit, a ConnectionUnit and a Server, depicted in the class diagram of Figure 1. The ConnectionUnit is in charge of checking for the arrival of new SMSs on the Server (operation checkSMS of class Server ) and to handle new calls coming from the Server (operation IncomingCall of class ConnectionUnit ). The TransmissionUnit is used by the ConnectionUnit to download the SMSs (operation downloadSMS ) and to handle the call’s data (operation beginCall ). The TransmissionUnit receives the data concerning SMSs and calls from the Server (operations receiveSMSToken and receiveCallData).
The behavior of the telephone system is modeled by the IOD of Figure 2. The fork operator specifies that the two main paths executed by the system are in parallel; for example the checkingSMS and receiveCall sequence diagrams run in parallel. Branch conditions are used in order to distinguish between different possible executions; for example after checking for a new SMS on the Server the system will continue with downloading the SMSs if one is present, otherwise it will loop back to the same diagram. It can be assumed that the Server allocates a dedicated thread to each connected telephone, this is why the sequence diagrams of Figure 2 report the interaction between only one ConnectionUnit, one TransmissionUnit and one Server. 4.2
The formalization presented here was derived from the diagram of Figure 2 by hand. The availability of a tool, which we are building, will allow us to analyze more complex models and assess the actual scalability of the proposed technique. The formalization is organized into sets of formulae, each of them corresponding to one of the SDs appearing in the IOD. Every set can be further decomposed into three subsets modeling different aspects of the SDs: – diagram-related formulae, which concern the beginning and the end of the execution of each SD, and the transition between a SD and the next one(s); – message-related formulae, which concern the ordering of the events within a single SD; – component-related formulae, which describe constraints on the execution of operations within single components.
These subsets are presented in the rest of this section.
Diagram-related Formulae In this first version of the semantics of IODs we
impose that, within each SD of an IOD, messages are totally ordered. This is to
clearly identify a begin message and an ending message. This assumption can
be removed using the fork/join operators to split diagrams into totally ordered
ones. Then, for each SD Dx, it is possible to identify two messages, ms and me,
which correspond to the beginning and to the end of the diagram. For each SD
Dx we introduce predicates DxST ART and DxEN D that are true, respectively,
at the beginning and the end of the diagram. We also introduce, for each message
m appearing in diagram Dx, a predicate m that holds in all instants in which
the message occurs in the system (this entails that components synchronize on
messages: send and receive of a message occur at the same time). Then, the
correspondence between DxST ART (resp. DxEN D) and the starting (resp.
ending) message ms (resp. me) is formalized by formulae (
For example, the instances of formulae (
delegateSM SST ART ⇔ downloadSM S delegateSM SEN D ⇔ reply3 delegateSM S ⇔ delegateSM SST ART ∨
Since(¬delegateSM SEN D, delegateSM SST ART ) 3 Note that TRIO formulae are implicitly temporally closed with the Alw operator; hence, DxST ART ⇔ ms is actually an abbreviation for Alw(DxST ART ⇔ ms) .
Notice that if the IOD contains k different occurrences of the same message
m, k different predicates m0...mk are introduced. For this reason in formula (
A diagram Dx is followed by a diagram Dy for either of two reasons: (
In the case of SD downloadSMS of Figure 2, the instances of formulae (
downloadSM SACT C1 ⇔ delegateSM SEN D downloadSM SACT C2 ⇔ downloadSM SEN D ∧ moredata downloadSM SACT ⇔ Past downloadSM SACT C1 ∨ downloadSM SACT C2 downloadSM SACT ⇒
(
mi ⇒ SomF(mj) ∧ ¬mj mj ⇒ SomP(mi) ∧ ¬mi mj ⇒ ¬SomF(mj) ∨ Until(¬mj, mi)
If, for example, formulae (
checkSM S ⇒ SomF(reply1) ∧ ¬reply1
reply1 ⇒ SomP(checkSM S) ∧ ¬checkSM S checkSM S ⇒ ¬SomF(checkSM S) ∨ Until(¬checkSM S, reply1) Component-related Formulae This set of formulae describes the conditions under which the entities of the system are busy, hence cannot perform further operations until they become free again. For example, in the telephone system of Figure 2, when the execution is inside the checkingSMS diagram, the ConnectionUnit cannot perform any other operations during the time interval between the invocation of operation ckechSMS and its corresponding reply message, since the invocation is synchronous (as highlighted by the full arrow).
In general, a synchronous invocation between objects A and B that starts with message mi and ends with message mj blocks both components from the moment of the invocation until its end; this is formalized by formulae (21-22), in which h and k are indexes identifying the occurrences of objects A and B in the IOD. In case of an asynchronous message m between A and B (such as, for example, incomingCall in SD waitingCall, as denoted by the wire-like arrow), the semantics is the one defined by formulae (23-24), which state that the objects are blocked only in the instant in which the message occurs.
mi ∨ Since(¬mj, mi) ⇔ ABLOCKEDh mi ∨ Since(¬mj, mi) ⇔ BBLOCKEDk m ⇔ ABLOCKEDh m ⇔ BBLOCKEDk
Finally, if n is the number of occurrences of object A in the IOD, formula
(25) states that all executions involving A are mutually exclusive.
(
The following formulae are instances of (21-25) for object ConnectionUnit, which appears in four separate SDs in the IOD of Figure 2: 11 (25)
4.3
Using the formalization presented above, we can check whether the modeled system satisfies some user-defined properties or not, by feeding it as input to the Zot verification tool.4
We start by asking whether it is true that, if no SMS is received in the future, then nothing will ever be downloaded. This property is formalized by the following formula: ¬SomF(SM S) ⇒ ¬SomF(downloadSM S) (26)
After feeding it the system and the property to be verified, the Zot tool determines that the latter does not hold for the telephone system of Figure 2. In fact, between the check for a new SMS and its download there can be an arbitrary delay; hence, the situation in which the last SMS has been received, but it has not yet been downloaded, violates the property. Zot returns this counterexample in around 8.5 seconds.5
The following variation of the property above, instead, holds for the system: ¬(SomP(SM S) ∨ SM S) ⇒ ¬WithinF(downloadSM S, 3) (27) 4 The complete Zot model can be downloaded from http://home.dei.polimi.it/rossi/telephone.lisp. 5 All tests have been performed with a time bound of 50 time units (see [16] for the role of time bounds in Bounded Model/Satisfiabliity Checking), using the Common Lisp compiler SBCL 1.0.29.11 on a 2.80GHz Core2 Duo laptop with Linux and 4 GB RAM. The verification engine used was the SMT-based Zot plugin introduced in [2], with Microsoft Z3 2.8 (http://research.microsoft.com/enus/um/redmond/projects/z3/) as the SMT solver.
Formula (27) states that, if no SMS has yet been received, for the next 3 instants there will not be an SMS download. Zot determines that formula (27) holds in around 7 seconds.
The following formula states that after a nextSMSToken request from TransmissionUnit to Server, no data concerning an incoming call can be received by the TransmissionUnit until a new SMS is received.
nextSM ST oken ⇒ Until(¬receiveCallData, receiveSM ST oken) (28)
Zot verifies that property (28) does not hold in around 8 seconds. As witnessed by the counterexample produced by Zot, the reason why (28) does not hold is that the downloadSMS diagram and the receiveCall diagram can run in parallel, and after sending a nextSMSToken message the TransmissionUnit and the Server are free to exchange a receiveCallData message. 5
Scenario-based specifications such as UML sequence diagrams, UML interaction diagrams, and Message Sequence Charts (MSCs) are classified as semi-formal, meaning that their syntax is formal but not their interpretation. As a consequence, the research community has devoted a significant effort to studying ways to give these diagrams a formal semantics.
Many works focus on the separate formalization of sequence diagrams and activity diagrams. St¨orrle analyzes the semantics of these diagrams and proposes an approach to their formalization [18]. More recently, Staines formalizes UML2 activity diagrams using Petri nets and proposes a technique to achieve this transformation [17]. Also, Lam formalizes the execution of activity diagrams using the π − Calculus, thus providing them with a sound theoretical foundation [13]. Finally, Eshuis focuses on activity diagrams, and defines a technique to translate them into finite state machines that can be automatically verified [9][8].
Other works investigate UML2 interaction diagrams. Cengarle and Knapp in [6] provide an operational semantics to UML 2 interactions, and in [5] they address the lack of UML interactions to explicitly describe variability and propose extensions equipped with a denotational semantics. Knapp and Wuttke translate UML2 interactions into automata and then verify that the proposed design meets the requirements stated in the scenarios by using model checking [12].
When multiple scenarios come into play, like in IODs, there is the problem of finding a common semantics. Uchitel and Kramer in [19] propose an MSCbased language with a semantics defined in terms of labeled transition systems and parallel composition, which is translated into Finite Sequential Processes that can be model-checked and animated. Harel and Kugler in [10] use Live Sequence Charts (LCSs) to model multiple scenarios, and to analyze the problem of knowing if there exists a satisfying object system and, if so, to synthesize one automatically.
In spite of the extensive research on the diagrams mentioned above, to the best of our knowledge very little attention has been paid to IODs. Kloul and Ku¨ster-Filipe [11] show how to model mobility using IODs and propose a formal semantics to the latter by translating them into the stochastic process algebra PEPA nets. Tebibel uses hierarchical colored Petri nets to define a formal semantics for IODs [4]. Our work is quite different, because it uses metric temporal logic to define the semantics of IODs; as briefly discussed in Sections 1 and 6, this opens many possibilities as far as the range of properties that can be expressed and analyzed for the system is concerned. 6
In this paper we presented the first steps towards a technique to precisely model and analyze complex, heterogeneous, embedded systems using an intuitive UMLbased notation. To this end, we started by focusing our attention on Interaction Overview Diagrams, which allow users to describe rich behaviors by combining together simple Sequence Diagrams. To allow designers to rigorously analyze modeled systems, the basic constructs of IODs have been given a formal semantics based on metric temporal logic. This semantics has been implemented in a fully automated verification tool, which has been used to prove some properties of an example system.
The work presented in this paper is part of a longer term research, and it will be extended in several ways.
As mentioned in Section 3, the TRIO temporal logic on which the semantics of IODs presented here is based has a metric notion of time. As such, it allows users to express real-time properties (e.g., ”a message will be sent within 3 seconds”). Nonetheless, in the present paper we only formalize qualitative temporal properties, like (partial) ordering among events and eventualities. The metric features of TRIO will be used to extend the formalization of SDs and IODs to real-time features that will be introduced in the modeling language by providing support for the MARTE UML profile.
Furthermore, we will provide semantics to constructs of IODs that are not yet covered. This semantics will be used to create tools to automatically translate IODs into the input language of the Zot tool, and to show designers the feedback from the verification tool (e.g., counterexamples) in a user-friendly way. In particular, we will define mechanisms to show counterexamples provided by Zot as SDs. These tools will allow domain experts who have little or no background in formal verification techniques to take advantage of these techniques in the analysis of complex systems.
A longer term goal of the present research is to include in the formalization not only Sequence Diagrams, but also other, related, notations that are customarily used to specify the behavior of the modeled systems, most typically State Diagrams. TRIO, and its related verification engine Zot, will become the common underlying semantic ground on which to build an integrated, coherent verification environment for real-time critical systems.
This research was supported by the European Community’s Seventh Framework Program (FP7/2007-2013) under grant agreement n. 248864 (MADES), and by the Programme IDEAS-ERC, Project 227977-SMScom.