A Logic-Based Approach for the Verification of UML Timed Models

作者：Baresi Luciano^*; Morzenti Angelo; Motta Alfredo; Pourhashem Mohammad Mehdi K; Rossi Andmatteo

来源：ACM Transactions on Software Engineering and Methodology, 2017, 26(2): 7.

DOI：10.1145/3106411

• Formal verification
• metric temporal logic
• formal semantics
• timed systems

This article presents a novel technique to formally verify models of real-time systems captured through a set of heterogeneous UML diagrams. The technique is based on the following key elements: (i) a subset of Unified Modeling Language (UML) diagrams, called Coretto UML (C-UML), which allows designers to describe the components of the system and their behavior through several kinds of diagrams (e.g., state machine diagrams, sequence diagrams, activity diagrams, interaction overview diagrams), and stereotypes taken from the UML Profile for Modeling and Analysis of Real-Time and Embedded Systems; (ii) a formal semantics of C-UML diagrams, defined through formulae of the metric temporal logic Tempo Reale ImplicitO (TRIO); and (iii) a tool, called Corretto, which implements the aforementioned semantics and allows users to carry out formal verification tasks on modeled systems. We validate the feasibility of our approach through a set of different case studies, taken from both the academic and the industrial domain.

• 出版日期2017-10