An Executable Semantics of Clock Constraint Specification Language and its Applications

Min Zhang 1 Frédéric Mallet 2
2 AOSTE - Models and methods of analysis and optimization for systems with real-time and embedding constraints
CRISAM - Inria Sophia Antipolis - Méditerranée , COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués, Inria de Paris
Abstract : 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.
Type de document :
Communication dans un congrès
Cyrille Artho, Peter Csaba Ölveczky. Formal Techniques for Safety-Critical Systems, Nov 2015, Luxembourg, Luxembourg. Springer, 596, pp.37-51, 2016, Communications in Computer and Information Science. 〈10.1007/978-3-319-29510-7_2〉
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01353824
Contributeur : Frédéric Mallet <>
Soumis le : dimanche 14 août 2016 - 16:03:42
Dernière modification le : lundi 29 août 2016 - 10:36:31
Document(s) archivé(s) le : mardi 15 novembre 2016 - 10:25:08

Fichier

main (1).pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Min Zhang, Frédéric Mallet. An Executable Semantics of Clock Constraint Specification Language and its Applications. Cyrille Artho, Peter Csaba Ölveczky. Formal Techniques for Safety-Critical Systems, Nov 2015, Luxembourg, Luxembourg. Springer, 596, pp.37-51, 2016, Communications in Computer and Information Science. 〈10.1007/978-3-319-29510-7_2〉. 〈hal-01353824〉

Partager

Métriques

Consultations de
la notice

122

Téléchargements du document

36