CHECKING BEHAVIOURAL CONSISTENCY OF UML-RT MODELS THROUGH TRACE-BASED SEMANTICS

摘要

Starting from a methodological approach intended to obtain a correct system specification in CSP+T from a UML-RT model of an RTS, we develop now a systematic procedure to check whether the obtained design is consistent with other views of the same system, such as the ones given by class, composite structure and state machines diagrams. To achieve this objective, a formal semantics of the notational elements of UML-RT according to CSP+T process terms is presented, which guarantees that system requirements are preserved from their initial UML-RT modelling to the final system implementation. As a consequence, the formal support given by the compositional refinement of CSP+T process terms will allow performing the system's software compositional verification. In addition, the derived formal semantic definitions are applied to the Production Cell case study.