An Executable Semantics of Clock Constraint Specification Language and its Applications - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

An Executable Semantics of Clock Constraint Specification Language and its Applications

Résumé

The Clock Constraint Specification Language (ccsl) is a language to specify logical and timed constraints between logical clocks. Given a set of clock constraints specified in ccsl, formal analysis is preferred to check if there exists a schedule that satisfies all the constraints, if the constraints are valid or not, and if the constraints satisfy expected properties. In this paper, we present a formal executable semantics of ccsl in rewriting logic and demonstrate some applications of the formal semantics to its formal analysis: 1) to automatically find bounded or periodic schedules that satisfy all the given constraints; 2) to simulate the execution of schedules with customized simulation policies; and 3) to verify LTL properties of ccsl constraints by bounded model checking. Compared with other existing modeling approaches, advantages with the rewriting-based semantics of ccsl are that we do not need to assume a bounded number of steps for the formalization, and we can exhaustively explore all the solutions within a given bound for the analysis.
Fichier principal
Vignette du fichier
main (1).pdf (374.86 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01353824 , version 1 (14-08-2016)

Identifiants

Citer

Min Zhang, Frédéric Mallet. An Executable Semantics of Clock Constraint Specification Language and its Applications. Formal Techniques for Safety-Critical Systems, Nov 2015, Luxembourg, Luxembourg. pp.37-51, ⟨10.1007/978-3-319-29510-7_2⟩. ⟨hal-01353824⟩
375 Consultations
169 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More