Periodic scheduling for MARTE/CCSL: Theory and practice

Abstract : The UML profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE) is used to design and analyze real-time and embedded systems. The Clock Constraint Specification Language (ccsl) is a companion language for MARTE. It introduces logical clocks as first class citizens as a way to formally specify the expected behavior of models , thus allowing formal verification. ccsl describes the expected infinite behaviors of reactive embedded systems. In this paper we introduce and focus on the notion of periodic schedule to allow for a nice finite abstraction of these infinite behaviors. After studying the theoretical properties of those schedules we give a practical way to deal with them based on the executable operational semantics of ccsl in rewriting logic with Maude. We also propose an algorithm to find automatically periodic schedulers with the proposed sufficient condition, and to perform formal analysis of ccsl constraints by means of customized simulation and bounded LTL model checking.
Type de document :
Article dans une revue
Science of Computer Programming, Elsevier, 2018, 154, pp.42-60. 〈10.1016/j.scico.2017.08.015〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01670450
Contributeur : Frédéric Mallet <>
Soumis le : lundi 7 janvier 2019 - 16:03:17
Dernière modification le : jeudi 7 février 2019 - 15:38:56

Fichier

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

Identifiants

Collections

Citation

Min Zhang, Feng Dai, Frédéric Mallet. Periodic scheduling for MARTE/CCSL: Theory and practice. Science of Computer Programming, Elsevier, 2018, 154, pp.42-60. 〈10.1016/j.scico.2017.08.015〉. 〈hal-01670450〉

Partager

Métriques

Consultations de la notice

320

Téléchargements de fichiers

75