MoDELS 2010 ACES-MB Workshop Proceedings From Interaction Overview Diagrams to Temporal Logic Luciano Baresi, Angelo Morzenti, Alfredo Motta, Matteo Rossi Politecnico di Milano Dipartimento di Elettronica e Informazione, Deep-SE Group Via Golgi 42 – 20133 Milano, Italy (baresi|morzenti|motta|rossi)@elet.polimi.it Abstract. In this paper, we use UML Interaction Overview Diagrams as the basis for a user-friendly, intuitive, modeling notation that is well- suited for the design of complex, heterogeneous, embedded systems de- veloped by domain experts with little background on modeling software- based 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, ver- ification technique is built. The modeling and verification technique is presented and discussed through the aid of an example system. Keywords: Metric temporal logic, bounded model checking, Unified Modeling Language. 1 Introduction 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., telecommuni- cation, control systems, software engineering, etc.). Careful modeling starting from the early stages of system development can greatly help increase the qual- ity 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 afore- mentioned 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 partic- ular, it is the first step towards a complete proposal for modeling and validating embedded systems. The plan is to exploit both “conventional” UML diagrams 1 http://www.mades-project.org Oslo, Norway, October 4, 2010 37 MoDELS 2010 ACES-MB Workshop Proceedings 2 [15] and a subset of the MARTE (Modeling and Analysis of Real-Time and Em- bedded 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 rep- resentation 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 com- plete 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 cru- cial 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 Interaction Overview Diagrams Most UML behavioral diagrams have undergone a significant revision from ver- sion 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. Oslo, Norway, October 4, 2010 38 MoDELS 2010 ACES-MB Workshop Proceedings 3 communication diagrams, sequence diagrams, timing diagrams and interaction overview diagrams. In this work we focus on Sequence Diagrams (SDs) and In- teraction 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 de- signer 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 com- pared to ADs and may have different interpretations. In the following the funda- mental 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 Sec- tion to provide graphical examples of IOD constructs. IODs include also other operators whose study is left to future works. 2.1 Initial Node/Final Node/Flow Final Node 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 Control Flow 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 Fork/Join 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 Oslo, Norway, October 4, 2010 39 MoDELS 2010 ACES-MB Workshop Proceedings 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 Decision/Merge 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 describ- ing 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 as- sume 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 com- position and first-order logic quantification. Table 1 defines some of the most significant ones, including those used in this paper. Oslo, Norway, October 4, 2010 40 MoDELS 2010 ACES-MB Workshop Proceedings 5 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) Table 1. TRIO derived temporal operators 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 satisfia- bility (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 Formal Semantics of Interaction Overview Diagrams 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, Oslo, Norway, October 4, 2010 41 MoDELS 2010 ACES-MB Workshop Proceedings 6 whose behavior modeled through a IOD is described in Section 4.1. Then, Sec- tion 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 Example telephone system The example system used throughout this section is a telephone system com- posed of three units, a TransmissionUnit, a ConnectionUnit and a Server, de- picted in the class diagram of Figure 1. The ConnectionUnit is in charge of Fig. 1. Class diagram for the telephone system. 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 dia- grams of Figure 2 report the interaction between only one ConnectionUnit, one TransmissionUnit and one Server. 4.2 TRIO Formalization 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 Oslo, Norway, October 4, 2010 42 MoDELS 2010 ACES-MB Workshop Proceedings 7 Fig. 2. Interaction Overview diagram for the telephone system. Oslo, Norway, October 4, 2010 43 MoDELS 2010 ACES-MB Workshop Proceedings 8 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 execu- tion 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 Dx ST ART and Dx EN 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 Dx ST ART (resp. Dx EN D) and the starting (resp. ending) message ms (resp. me ) is formalized by formulae (1-2)3 . In addition, we introduce a predicate Dx that holds in all instants in which diagram Dx is executing; hence, predicate Dx holds between Dx ST ART and Dx EN D, as stated by formula (3). Dx ST ART ⇔ ms (1) Dx EN D ⇔ me (2) Dx ⇔ Dx ST ART ∨ Since(¬Dx EN D, Dx ST ART ) (3) For example, the instances of formulae (1-3) for diagram delegateSMS corre- spond to formulae (4-6). delegateSM SST ART ⇔ downloadSM S (4) delegateSM SEN D ⇔ reply3 (5) delegateSM S ⇔ delegateSM SST ART ∨ (6) Since(¬delegateSM SEN D, delegateSM SST ART ) 3 Note that TRIO formulae are implicitly temporally closed with the Alw operator; hence, Dx ST ART ⇔ ms is actually an abbreviation for Alw(Dx ST ART ⇔ ms ) . Oslo, Norway, October 4, 2010 44 MoDELS 2010 ACES-MB Workshop Proceedings 9 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 (5) reply3 appears instead of reply. A diagram Dx is followed by a diagram Dy for either of two reasons: (1) Dx is directly connected to Dy , in this case the end of Dx is the necessary condition to start Dy ; (2) Dx is connected to Dy through some decision operator, in this case the necessary condition to start Dy is given by the end of Dx , provided the condition on the decision operator is met. If a diagram Dx is preceded by p sequence diagrams, we introduce p predicates Dx ACT Ci (i ∈ {1...p}), where Dx ACT Ci holds if the i-th necessary condition to start diagram Dx holds. We also introduce predicate Dx ACT , which holds the instant after any of the p necessary conditions holds, as defined by formula (7). This is done to avoid that Dx ST ART and Dy EN D are true at the same time instant, with Dy ∈ {1...p}. In fact a condition Dx ACT Ci holds when the ending predicate of the i-th diagram that precedes Dx hold. After the necessary condition to start a diagram is met, the diagram will start at some point in the future (not necessarily immediately), as stated by formula (8). Finally, after a diagram starts, it cannot start again until the necessary condition to start it is met anew, as defined by formula (9). Dx ACT ⇔ Past(Dx ACT C0 ∨ ... ∨ Dx ACT Cm , 1) (7) Dx ACT ⇒ SomF(Dx ST ART ) ∨ Dx ST ART (8) Dx ST ART ⇒ ¬SomF(Dx ST ART ) ∨ Until(¬Dx ST ART , Dx ACT ) (9) In the case of SD downloadSMS of Figure 2, the instances of formulae (7-9) are given by (12-14). In addition, formulae (10-11) define the necessary conditions to start diagram downloadSMS : either diagram delegateSMS ends, or diagram downloadSMS ends and condition moredata holds. Currently, we can only deal with atomic boolean conditions. The representation of more complex data, and conditions upon them, is already in our research agenda. downloadSM SACT C1 ⇔ delegateSM SEN D (10) downloadSM SACT C2 ⇔ downloadSM SEN D ∧ moredata (11)   downloadSM SACT C1 downloadSM SACT ⇔ Past (12) ∨ downloadSM SACT C2 downloadSM SACT ⇒ SomFe (downloadSM SST ART ) ∨ downloadSM SST ART (13) downloadSM SST ART ⇒ ¬SomFe (downloadSM SST ART ) ∨ Until(¬downloadSM SST ART , downloadSM SACT ) (14) Oslo, Norway, October 4, 2010 45 MoDELS 2010 ACES-MB Workshop Proceedings 10 Message-related Formulae Suppose that, in a SD, a message mi is followed by another message mj . Then the occurrence of mi entails that mj will also occur in the future; conversely, the occurrence of mj entails that mi must have occurred in the past. This is formally defined by formulae (15-16). In addition, after an instance of mj , there can be a new instance of the same message only after a new occurrence of mi ; this is stated by formula (17), which defines that, after mj , there will not be a new occurrence of mj until there is an occurrence of mi . mi ⇒ SomF(mj ) ∧ ¬mj (15) mj ⇒ SomP(mi ) ∧ ¬mi (16) mj ⇒ ¬SomF(mj ) ∨ Until(¬mj , mi ) (17) If, for example, formulae (15-17) are instantiated for SD checkingSMS of Figure 2, one obtains formulae (18-20). checkSM S ⇒ SomF(reply1) ∧ ¬reply1 (18) reply1 ⇒ SomP(checkSM S) ∧ ¬checkSM S (19) checkSM S ⇒ ¬SomF(checkSM S) ∨ Until(¬checkSM S, reply1) (20) 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 Connec- tionUnit 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 (21) mi ∨ Since(¬mj , mi ) ⇔ BBLOCKEDk (22) m ⇔ ABLOCKEDh (23) m ⇔ BBLOCKEDk (24) 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. Oslo, Norway, October 4, 2010 46 MoDELS 2010 ACES-MB Workshop Proceedings 11 ∀1 ≤ i, j ≤ n(i = j ∧ ABLOCKEDi ⇒ ¬ABLOCKEDj ) (25) The following formulae are instances of (21-25) for object ConnectionUnit, which appears in four separate SDs in the IOD of Figure 2: ConnectionU nitBLOCKED1 ⇔ checkSM S∨ Since(¬reply1, checkSM S) ConnectionU nitBLOCKED2 ⇔ incomingCall ConnectionU nitBLOCKED3 ⇔ downloadSM S∨ Since(¬reply2, donwloadSM S) ConnectionU nitBLOCKED4 ⇔ beginCall∨ Since(¬reply3, beginCall) ∀1 ≤ i, j ≤ 4(i = j ∧ ConnectionU nitBLOCKEDi ⇒ ¬ConnectionU nitBLOCKEDj ) 4.3 Properties 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/en- us/um/redmond/projects/z3/) as the SMT solver. Oslo, Norway, October 4, 2010 47 MoDELS 2010 ACES-MB Workshop Proceedings 12 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 Trans- missionUnit 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 wit- nessed 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 Related Work 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 conse- quence, 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örrle analyzes the semantics of these diagrams and pro- poses 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 founda- tion [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 ad- dress the lack of UML interactions to explicitly describe variability and propose extensions equipped with a denotational semantics. Knapp and Wuttke trans- late 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 MSC- based 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. Oslo, Norway, October 4, 2010 48 MoDELS 2010 ACES-MB Workshop Proceedings 13 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 Kü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 se- mantics 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 Conclusions and Future Works In this paper we presented the first steps towards a technique to precisely model and analyze complex, heterogeneous, embedded systems using an intuitive UML- based 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 seman- tics 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 seman- tics 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 feed- back 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 cus- tomarily 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. Oslo, Norway, October 4, 2010 49 MoDELS 2010 ACES-MB Workshop Proceedings 14 Acknowledgments 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. References 1. A. Bagnato, A. Sadovykh, R. F. Paige, D. S. Kolovos, L. Baresi, A. Morzenti, and M. Rossi. MADES: Embedded systems engineering approach in the avionics domain. In Proccedings of the First Workshop on Hands-on Platforms and tools for model-based engineering of Embedded Systems (HoPES), 2010. 2. M. M. Bersani, A. Frigeri, M. Pradella, M. Rossi, A. Morzenti, and P. San Pietro. Bounded reachability for temporal logic over constraint systems. In Proceedings of TIME 2010, 2010. 3. G. Blohm and A. Bagnato. D1.1 requirements specification. Technical report, MADES Consortium, 2010. Draft. 4. T. Bouabana-Tebibel. Semantics of the interaction overview diagram. In Proc. of the IEEE International Conference on Information Reuse Integration (IRI), pages 278–283, 2009. 5. M. V. Cengarle, P. Graubmann, and S. Wagner. Semantics of UML 2.0 interactions with variabilities. Electronic Notes in Theoretical Computer Science, 160:141–155, 2006. 6. M. V. Cengarle and A. Knapp. Operational semantics of UML 2.0 interactions. Technical Report TUM-I0505, Technische Universität Mnchen, 2005. 7. E. Ciapessoni, A. Coen-Porisini, E. Crivelli, D. Mandrioli, P. Mirandola, and A. Morzenti. From formal models to formally-based methods: an industrial ex- perience. ACM TOSEM, 8(1):79–113, 1999. 8. R. Eshuis. Symbolic model checking of UML activity diagrams. ACM Trans. Softw. Eng. Methodol., 15(1):1–38, 2006. 9. R. Eshuis and R. Wieringa. Tool support for verifying UML activity diagrams. IEEE Trans. Software Eng., 30(7):437–447, 2004. 10. D. Harel and H. Kugler. Synthesizing state-based object systems from LSC spec- ifications. In Proceedings of the International Conference on the Implementation and Application of Automata, volume 2088 of Lecture Notes in Computer Science, pages 1–33, 2000. 11. L. Kloul and J. Küster-Filipe. From intraction overview diagrams to PEPA nets. In In proc. of the Workshop on Process Algebra and Stochastically Timed Activities, 2005. 12. A. Knapp and J. Wuttke. Model checking of UML 2.0 interactions. In Models in Software Engineering, volume 4634 of Lecture Notes in Computer Science, pages 42–51, 2007. 13. V. S. W. Lam. On -calculus semantics as a formal basis for uml activity diagrams. International Journal of Software Engineering and Knowledge Engineering, 2008. 14. Object Management Group. UML Profile for Modeling and Analysis of Real-Time Embedded Systems. Technical report, OMG, 2009. formal/2009-11-02. 15. Object Management Group. OMG Unified Modeling Language (OMG UML), Superstructure. Technical report, OMG, 2010. formal/2010-05-05. Oslo, Norway, October 4, 2010 50 MoDELS 2010 ACES-MB Workshop Proceedings 15 16. M. Pradella, A. Morzenti, and P. San Pietro. The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties. In Proceedings of ESEC/SIGSOFT FSE, pages 312–320, 2007. 17. T. S. Staines. Intuitive mapping of UML 2 activity diagrams into fundamental modeling concept petri net diagrams and colored petri nets. Proceedings of the IEEE International Conference on the Engineering of Computer-Based Systems, pages 191–200, 2008. 18. H. Störrle and J. H. Hausmann. Towards a formal semantics of UML 2.0 activities. In Software Engineering, volume 64 of Lecture Notes in Informatics, pages 117–128, 2005. 19. S. Uchitel and J. Kramer. A workbench for synthesising behaviour models from scenarios. In Proceedings of the 23rd International Conference on Software Engi- neering, pages 188–197, 2001. Oslo, Norway, October 4, 2010 51