Paper Info
Title
A Logic-Based Approach for the Verification of UML Timed Models.
Abstract
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.
Year
DOI
Venue
2017
10.1145/3106411
ACM Trans. Softw. Eng. Methodol.
Keywords
Field
DocType
Formal verification, formal semantics, metric temporal logic, timed systems
Sequence diagram,Programming language,Unified Modeling Language,UML tool,Computer science,Activity diagram,Theoretical computer science,Applications of UML,Story-driven modeling,Systems Modeling Language,Formal verification
Journal
Volume
Issue
ISSN
26
2
1049-331X
Citations 
PageRank 
References 
0
0.34
56
Authors
5
Name
Order
Citations
PageRank
L. Baresi116013.28
Angelo Morzenti221.05
Alfredo Motta3565.20
Mohammad Mehdi Pourhashem Kallehbasti4172.42
Matteo Rossi582.77