An SMT-Based Approach to the Formal Analysis of MARTE/CCSL

Min Zhang 1 Frédéric Mallet 2, 3 Huibiao Zhu 1
1 ECNU - East China Normal University [Shangaï]
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
3 UCA - Université Côte d'Azur
Abstract : MARTE (abbreviated for Modeling and Analysis of Real-Time and Embedded systems) is a UML profile which provides a general modeling framework to design and analyze real-time embedded systems. CCSL (abbreviated for Clock Constraint Specification Language) is a formal language companion to MARTE, used to specify the constraints between the occurrences of events in real-time embedded systems. Many approaches have been proposed to the formal analysis of CCSL such as simulation and model checking. We propose in this paper an SMT-based approach to the formal analysis of CCSL. It is well-known that the SMT-based approach can effectively overcome the state-explosion problem for model checking, and can also be used for theorem proving. The latter feature allows us to prove the invalidity of CCSL constraints, which most of the existing approaches lack. We implement the proposed approach in a prototype tool clyzer on top of K framework and use Z3 as the underlying SMT solver.
Keywords : SMT Solver MARTE/CCSL Z3 K-Framework
Type de document :
Communication dans un congrès
Formal Methods and Software Engineering, Nov 2016, Tokyo, Japan. Springer, 10009, pp.433-449, 2016, Lecture Notes in Computer Science. 〈10.1007/978-3-319-47846-3_27〉
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01394677
Contributeur : Frédéric Mallet <>
Soumis le : mercredi 21 décembre 2016 - 17:37:58
Dernière modification le : jeudi 26 avril 2018 - 10:28:12
Document(s) archivé(s) le : mardi 21 mars 2017 - 12:08:47

Fichier

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

Identifiants

Collections

UNICE | INRIA | I3S | UNIV-COTEDAZUR

Citation

Min Zhang, Frédéric Mallet, Huibiao Zhu. An SMT-Based Approach to the Formal Analysis of MARTE/CCSL. Formal Methods and Software Engineering, Nov 2016, Tokyo, Japan. Springer, 10009, pp.433-449, 2016, Lecture Notes in Computer Science. 〈10.1007/978-3-319-47846-3_27〉. 〈hal-01394677〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

318

Téléchargements de fichiers

74

Contact


archive-ouverte@inria.fr