Model checking of MARTE/CCSL time behaviors using timed I/O automata

摘要

Modelling and Analysis of Real-time and Embedded systems (MARTE) as a domain-specific language is widely used for designing, analysing, and the building of cyber physical systems (CPS). It also provides CCSL as a purely declarative language for expressing logical and chronometric constraints on clocks. Although MARTE/CCSL is powerful expressively, it lacks formal semantics-based language support for describing and analysing. Semantic support, such as timed Input/Output automata not only provides modelling and analysis of timing behaviors, it also provides modelling of the Input/Output behaviors in a direct sense compared to timed automata. The Input/Output behavior can verify the casual relationship between components, one of the most important behaviors is the fairness between components. Thus, to improve the capacity of modeling and verification of the MARTE/CCSL behavior model, we present a method to use MARTE/CCSL as a high level specification language for modelling, then mapping MARTE/CCSL behavior model to timed Input/Output automata, then using an integrated tool (UPPAAL-TIGA) to verify the safety, liveness, and fairness thereof. Finally, we demonstrate the proposed transformation method using a Telerobot control system of real-time systems.