@inproceedings{73d4ae5eca164ca5ac80275aa4ed0dae,
title = "Verification of MARTE/CCSL time requirements in Promela/SPIN",
abstract = "The Clock Constraint Specification Language (CCSL) provides expressions and relations to specify the time requirements and causal dependencies of systems. It was initially proposed, in the context of MARTE: the UML profile for Modeling and Analysis of Real-Time and Embedded Systems. In this paper, we propose a method to verify CCSL specifications. We give a formal state-based interpretation of a fundamental subset of CCSL clock constraints. Based on it, we translate a CCSL specification into a Promela model and feed the result into the model checker SPIN. Then we show some patterns for expressing the properties of the model and do the verification. A digital filter application is used as an example to illustrate the approach.",
keywords = "CCSL, MARTE, Promela, Verification",
author = "Ling Yin and Fr{\'e}d{\'e}ric Mallet and Jing Liu",
year = "2011",
doi = "10.1109/ICECCS.2011.14",
language = "英语",
isbn = "9780769543819",
series = "Proceedings - 2011 16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011",
publisher = "IEEE Computer Society",
pages = "65--74",
booktitle = "Proceedings - 2011 16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011",
address = "美国",
}