Towards the UML-Based Formal Verification of Timed Systems

This paper presents the approach to the formal verification of UML-based models of timed systems developed in the MADES project. The approach differs from many current ones in that it aims at (i) being inclusive in the range of diagrams considered when producing the formal model, and (ii) adhering to the UML notation as much as possible. The metric temporal logic-based semantics developed in the project is presented through an example system