A formal methodology for semantics and time consistency checking of UML dynamic diagrams

UML 2.0 is a multi-paradigm language which copes well with modeling of reactive and real-time systems by offering many visual and flexible notations for description of their various aspects including their time constraints. However, their development remains a complex task and error-prone even if object-oriented concepts are used. Consequently, one is interested in validation techniques Which allow analyzing the behaviors of a design already in early phases. Nevertheless, the consistency and compatibility checking of designed artifacts for a reactive system is a difficult task; because of both the imprecise dynamic semantics of UML diagrams and the expressiveness gap between them. In this setting, this article proposes a methodology for semantics and time consistency checking between behavioral models and scenario-based specifications depicted, respectively, by state and sequence diagrams.