@inproceedings{3a8fc65fce054943912ee53a82cf737d,
title = "An SMT-based approach to the formal analysis of MARTE/CCSL",
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 SMTbased 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 𝕂 framework and use Z3 as the underlying SMT solver.",
keywords = "MARTE/CCSL, Model checking, SMT, Z3, 𝕂 framework",
author = "Min Zhang and Fr{\'e}d{\'e}ric Mallet and Huibiao Zhu",
note = "Publisher Copyright: {\textcopyright} Springer International Publishing AG 2016.; 18th International Conference on Formal Engineering Methods, ICFEM 2016 ; Conference date: 14-11-2016 Through 18-11-2016",
year = "2016",
doi = "10.1007/978-3-319-47846-3\_27",
language = "英语",
isbn = "9783319478456",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "433--449",
editor = "Kazuhiro Ogata and Mark Lawford and Shaoying Liu",
booktitle = "Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016, Proceedings",
address = "德国",
}