Clock Constraints Specification Langage : A mechanized denotational semantics in Agda

CCSL is a concurrency modeling language defined inside the MARTE UML profile. It was designed to provide system designers with requirement modeling facilities that are easier to master than temporal logics. It allows the expression of event occurrences and constraints between them. TimeSquare is a tool that implements CCSL providing on the one hand textual and graphical modeling facilities, and on the other hand a solver that checks the satisfaction of these constraints, hence giving CCSL an operational semantics. This toolset allows to assess system specific properties at the model level. But, some properties need to best verified at language level, especially when extending the language itself. In order to prove these ones, the designers of CCSL provided a denotational semantics that associate mathematical definitions to CCSL constructs. But, since this semantics is handmade and lacks a formal version to build and verify the properties of the extensions, we propose to mechanize it in a proof assistant. We have selected the Agda theorem prover, developed by Ulf Norell at Chalmer's university for this work