A Transformation Approach for Multiform Time Requirements

摘要

Many of the timing constraints expressed in physical prescriptions of distributed systems and multi-clock electronic systems can be expressed in logical concepts. A logical time model has been developed as a part of the official OMG UML profile MARTE, in order to enrich the formalism of this profile and also to facilitate the description and analysis of temporal constraints. This time model is associated with CCSL (Clock Constraint Specification Language). Once the software is modeled, the difficulty lies in both expressing the relevant properties and in verifying them formally. We present an automatic transformation technique related to a method for verifying properties by model checking, thus exploiting both the CDL language (Context Description Language) and the OBP tool (Observer-based Prover). The technique is based on a translation of MARTE models and the CCSL constraints into Fiacre code. CDL can express predicates and observers. These are verified during the exhaustive exploration of the complete model by OBP. We illustrate our contribution by an illustrative case.