Clocks vs. Instants Relations: Verifying CCSL Time Constraints in UML/MARTE Models
Sprache des Vortragstitels:
Englisch
Original Kurzfassung:
The specification of non-functional requirements,
e. g., on timing forms an essential part of modern system design.
Modeling languages such as MARTE/CCSL provide dedicated description means enabling engineers to formally define the ticking of the clocks to be implemented in terms of clock constraints and the actually intended timing behavior in terms
of instant relations. But thus far, instant relations have only been utilized in order to monitor the correct execution of the clock
constraints. In this work, we propose a methodology which, for the first time, verifies clock constraints against the given instant
relations. To this end, the timing behavior is represented in terms of an automaton followed by its verification through satisfiability
solvers. A case study illustrates the application of the proposed methodology.
Forschungs-