Formalization and Verification of Hierarchical Use of Interaction Overview Diagrams Using Timing Diagrams
---
paper_title: Mapping UML Interaction Overview Diagram to Time Petri Net for Analysis and Verification of Embedded Real-Time Systems with Energy Constraints

paper_content:

With the heterogeneity and complexity growth of embedded real-time systems (ERTS) is required an interdisciplinary approaches in the development processes embracing software engineering, mechanics, electric and electronics areas. Accordingly, a modeling language, called Unified Modeling Language (UML), has been specified by OMG (Object Management Group). However, when dealing with ERTS is indispensable the description of quantitative system aspects such as time and energy consumption. For that, a new UML Profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) has been also specified by OMG. Nevertheless, these UML models themselves are not directly analyzable. This paper presents the mapping process of interaction overview diagram (IO) into a time Petri net with energy constraints (ETPN) so as to analyze and verify the functional, timing and energy requirements in early phases of the life-cycle development.
---
paper_title: Semantics of the interaction overview diagram

paper_content:

UML 2 interaction overview diagram, IOD for short, is a variant of UML activity diagrams where the nodes may be sequence diagrams. This combination provides it with benefits related to both specific and generic behaviors. Indeed, the use of sequence diagrams for describing the objects dynamics, allows a valuated control flow specification. We propose in this paper an approach based on a value oriented validation of the IOD. The validation is made by model checking using the hierarchical Petri nets derived from the IOD diagrams. A case study is given to
---
paper_title: Formal validation with OCL

paper_content:

System validation allows to check whether the modeled system complies with the customer requirements. For UML modeling, these requirements can be specified by the designer as invariants using the Object Constraint Language (OCL). To validate the OCL invariants, we first propose to derive the UML dynamic models to Petri nets. The OCL invariants are after, translated to temporal logic properties in order to be checked on the derived Petri nets. To efficiently exploit all OCL capabilities in expressing invariants, we also propose an object flow specification on the dynamic models and introduce an adequate technique to translate them to Petri nets. A case study is given throughout the paper to illustrate the approach.
---
paper_title: Reasoning on UML class diagrams

paper_content:

UML is the de-facto standard formalism for software design and analysis. To support the design of large-scale industrial applications, sophisticated CASE tools are available on the market, that provide a user-friendly environment for editing, storing, and accessing multiple UML diagrams. It would be highly desirable to equip such CASE tools with automated reasoning capabilities, such as those studied in Artificial Intelligence and, in particular, in Knowledge Representation and Reasoning. Such capabilities would allow to automatically detect relevant formal properties of UML diagrams, such as inconsistencies or redundancies. With regard to this issue, we consider UML class diagrams, which are one of the most important components of UML, and we address the problem of reasoning on such diagrams. We resort to several results developed in the field of Knowledge Representation and Reasoning, regarding Description Logics (DLs), a family of logics that admit decidable reasoning procedures. Our first contribution is to show that reasoning on UML class diagrams is EXPTIME-hard, even under restrictive assumptions; we prove this result by showing a polynomial reduction from reasoning in DLs. The second contribution consists in establishing EXPTIME-membership of reasoning on UML class diagrams, provided that the use of arbitrary OCL (first-order) constraints is disallowed. We get this result by using DLR"i"f"d, a very expressive EXPTIME-decidable DL that has been developed to capture typical features of conceptual and object-oriented data models. The last contribution has a more practical flavor, and consists in a polynomial encoding of UML class diagrams in the DL ALCQI, which essentially is the most expressive DL supported by current state-of-the-art DL-based reasoning systems. Though less expressive than DLR"i"f"d, the DL ALCQI preserves enough semantics to keep reasoning about UML class diagrams sound and complete. Exploiting such an encoding, one can use current DL-based reasoning systems as core reasoning engines for a next generation of CASE tools, that are equipped with reasoning capabilities on UML class diagrams.
---
paper_title: A Methodology for Mapping SysML Activity Diagram to Time Petri Net for Requirement Validation of Embedded Real-Time Systems with Energy Constraints

paper_content:

In this paper we use the Activity diagram of the System Modeling Language (SysML) in combination with the new UML profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) in order to validate functional, timing and low power requirements in early phases of the embedded system development life-cycle. However, SysML lacks a formal semantics and hence it is not possible to apply, directly, mathematical techniques on SysML models for system validation. Thus, a novel approach for automatic translation of SysML Activity diagram into Time Petri Net with Energy constraints (ETPN) is proposed. In order to depict the practical usability of the proposed method, a case study is presented, namely, pulse-oximeter. Besides, the estimates obtained (execution time and energy consumption) from the model are 95% close to the respective measures obtained from the real hardware platform.
---
paper_title: UML behavioral consistency checking using instantiable Petri nets

paper_content:

Model-driven engineering (MDE) development methods are gaining increasing attention from industry. In MDE, the model is the primary artifact and serves several goals, including code generation, requirements traceability, and model-based testing. MDE thus enables cost-effective building of models versus direct coding of an application. Thus model-based formal verification of behavioral consistency is desirable as it helps improve model quality. Our approach is based on translation of a UML model to instantiable Petri nets (IPN). This formalism is based on the semantics of Petri nets, but introduces the concepts of type and instance. This allows one to accurately capture these concepts in UML models. IPN support hierarchical descriptions natively, and use the notion of transition synchronization for composition of behaviors. This is a general and powerful mechanism borrowed from process algebra. We show that IPN allow one to adequately address the challenges of translation from UML for analysis purposes. The approach has been implemented and experimental results are presented.
---
paper_title: Mapping UML Interaction Overview Diagram to Time Petri Net for Analysis and Verification of Embedded Real-Time Systems with Energy Constraints

paper_content:

With the heterogeneity and complexity growth of embedded real-time systems (ERTS) is required an interdisciplinary approaches in the development processes embracing software engineering, mechanics, electric and electronics areas. Accordingly, a modeling language, called Unified Modeling Language (UML), has been specified by OMG (Object Management Group). However, when dealing with ERTS is indispensable the description of quantitative system aspects such as time and energy consumption. For that, a new UML Profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) has been also specified by OMG. Nevertheless, these UML models themselves are not directly analyzable. This paper presents the mapping process of interaction overview diagram (IO) into a time Petri net with energy constraints (ETPN) so as to analyze and verify the functional, timing and energy requirements in early phases of the life-cycle development.
---
paper_title: Towards model checking executable UML specifications in mCRL2

paper_content:

We describe a translation of a subset of executable UML (xUML) into the process algebraic specification language mCRL2. This subset includes class diagrams with class generalisations, and state machines with signal and change events. The choice of these xUML constructs is dictated by their use in the modelling of railway interlocking systems. The long-term goal is to verify safety properties of interlockings modelled in xUML using the mCRL2 and LTSmin toolsets. Initial verification of an interlocking toy example demonstrates that the safety properties of model instances depend crucially on the run-to-completion assumptions.
---
paper_title: Semantics of the interaction overview diagram

paper_content:

UML 2 interaction overview diagram, IOD for short, is a variant of UML activity diagrams where the nodes may be sequence diagrams. This combination provides it with benefits related to both specific and generic behaviors. Indeed, the use of sequence diagrams for describing the objects dynamics, allows a valuated control flow specification. We propose in this paper an approach based on a value oriented validation of the IOD. The validation is made by model checking using the hierarchical Petri nets derived from the IOD diagrams. A case study is given to
---
paper_title: Semantics of the interaction overview diagram

paper_content:

UML 2 interaction overview diagram, IOD for short, is a variant of UML activity diagrams where the nodes may be sequence diagrams. This combination provides it with benefits related to both specific and generic behaviors. Indeed, the use of sequence diagrams for describing the objects dynamics, allows a valuated control flow specification. We propose in this paper an approach based on a value oriented validation of the IOD. The validation is made by model checking using the hierarchical Petri nets derived from the IOD diagrams. A case study is given to
---
paper_title: Unifying Modeling and Simulation Based on UML Timing Diagram and UPPAAL

paper_content:

The modeling, simulation and verification of real-time systems can be unified and the efficiency of system development can be improved if the UML timing diagram model can be translated into the timed automata model. The conversion rules and the algorithm are given in this paper. A coffee machine control system is given as an example in which we give the UML timing diagram model and translate it to timed automata model in UPPAAL, then we verify the accessibility, the security and the activity of the system by UPPAAL.
---
paper_title: Semantics of the interaction overview diagram

paper_content:

UML 2 interaction overview diagram, IOD for short, is a variant of UML activity diagrams where the nodes may be sequence diagrams. This combination provides it with benefits related to both specific and generic behaviors. Indeed, the use of sequence diagrams for describing the objects dynamics, allows a valuated control flow specification. We propose in this paper an approach based on a value oriented validation of the IOD. The validation is made by model checking using the hierarchical Petri nets derived from the IOD diagrams. A case study is given to
---
paper_title: Semantics of the interaction overview diagram

paper_content:

UML 2 interaction overview diagram, IOD for short, is a variant of UML activity diagrams where the nodes may be sequence diagrams. This combination provides it with benefits related to both specific and generic behaviors. Indeed, the use of sequence diagrams for describing the objects dynamics, allows a valuated control flow specification. We propose in this paper an approach based on a value oriented validation of the IOD. The validation is made by model checking using the hierarchical Petri nets derived from the IOD diagrams. A case study is given to
---
paper_title: Semantics of the interaction overview diagram

paper_content:

UML 2 interaction overview diagram, IOD for short, is a variant of UML activity diagrams where the nodes may be sequence diagrams. This combination provides it with benefits related to both specific and generic behaviors. Indeed, the use of sequence diagrams for describing the objects dynamics, allows a valuated control flow specification. We propose in this paper an approach based on a value oriented validation of the IOD. The validation is made by model checking using the hierarchical Petri nets derived from the IOD diagrams. A case study is given to
---
paper_title: Formal validation with OCL

paper_content:

System validation allows to check whether the modeled system complies with the customer requirements. For UML modeling, these requirements can be specified by the designer as invariants using the Object Constraint Language (OCL). To validate the OCL invariants, we first propose to derive the UML dynamic models to Petri nets. The OCL invariants are after, translated to temporal logic properties in order to be checked on the derived Petri nets. To efficiently exploit all OCL capabilities in expressing invariants, we also propose an object flow specification on the dynamic models and introduce an adequate technique to translate them to Petri nets. A case study is given throughout the paper to illustrate the approach.
---

Title: Formalization and Verification of Hierarchical Use of Interaction Overview Diagrams Using Timing Diagrams

Section 1: INTRODUCTION
Description 1: This section should provide an introduction to UML and its importance, the problems with its informal nature, and the need for formalization of the hierarchical use of Interaction Overview Diagrams (IOD) using Hierarchical Colored Petri Nets (HCPNs) and Timing Diagrams (TDs).

Section 2: RELATED WORK
Description 2: This section should discuss the related work in the field of formal verification of UML2 specifications, and previous attempts to formalize and verify IODs.

Section 3: UML2 Interaction Overview Diagrams
Description 3: This section should define IODs, their components, and their hierarchical nature. It should include a formal definition of IODs and explain their elements.

Section 4: Timing diagram (TD)
Description 4: This section should define Timing Diagrams, their components, and their importance in the context of UML2. It should provide a formal definition and explain how TDs are integrated and used.

Section 5: FROM THE HIERARCHICAL USE OF IOD TO HCPNs USING THE TIMED CP-net
Description 5: This section should provide the formalization process of converting hierarchical IODs into HCPNs using timed CP-nets. It should include the mapping rules and the transformation functions used.

Section 6: Case study modeling
Description 6: This section should present a case study to illustrate the practical application of the proposed formalization method. It should include the UML model of the system and detailed explanation of interactions and behaviors.

Section 7: Verification of HCPN based model using timed CP-net
Description 7: This section should describe the verification process of the HCPN model using timed CP-net. It should explain how safety and liveness properties are checked using CPN Tools.

Section 8: CONCLUSION AND FUTURE WORK
Description 8: This section should summarize the findings of the paper, the contributions made, and the results obtained from the verification process. It should also outline potential future work and improvements.