Clock Constraints Specification Langage : A mechanized denotational semantics in Agda
| Autor: | Montin, Mathieu, Pantel, Marc |
|---|---|
| Přispěvatelé: | Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Institut National Polytechnique (Toulouse) (Toulouse INP), ANR-12-INSE-0011,GeMoC,Un framework de modèles de calcul génériques pour l'exécution et l'analyse dynamique de modèles(2012) |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
Denotational semantics
CCSL ACM: D.: Software/D.1: PROGRAMMING TECHNIQUES/D.1.3: Concurrent Programming/D.1.3.0: Distributed programming ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.3: Formal methods ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs/F.3.1.2: Logics of programs [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] Proof assistant Agda ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.2: Semantics of Programming Languages/F.3.2.1: Denotational semantics |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|