@inproceedings{57853469dcbd44b9b85254deef29a47a,
title = "Towards SMT-Based LTL model checking of clock constraint specification language for real-time and embedded systems",
abstract = "The Clock Constraint Specification Language (CCSL) is a formal language companion to MARTE (shorthand for Modeling and Analysis of Real-Time and Embedded systems), a UML profile used to facilitate the design and analysis of real-time and embedded systems. CCSL is proposed to specify constraints on the occurrences of events in systems. However, the language lacks efficient verification support to formally analyze temporal properties, which are important properties to real-time and embedded systems. In this paper, we propose an SMT-based approach to model checking of the temporal properties specified in Linear Temporal Logic (LTL) for CCSL by transforming CCSL constraints and LTL formulas into SMT formulas. We implement a prototype tool for the proposed approach and use the state-of-the-art tool Z3 as its underlying SMT solver. We model two practical real-time and embedded systems, i.e., a traffic light controller and a power window system in CCSL, and model check LTL properties of them using the proposed approach. Experimental results demonstrate the effectiveness and efficiency of our approach.",
keywords = "CCSL, LTL, Model checking, SMT, Z3",
author = "Min Zhang and Yunhui Ying",
note = "Publisher Copyright: {\textcopyright} 2017 ACM.; 18th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, LCTES 2017 ; Conference date: 21-06-2017 Through 22-06-2017",
year = "2017",
month = jun,
day = "21",
doi = "10.1145/3078633.3081035",
language = "英语",
series = "Proceedings of the ACM SIGPLAN Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES)",
publisher = "Association for Computing Machinery",
pages = "61--70",
editor = "Zili Shao and Vijay Nagarajan",
booktitle = "LCTES 2017 - Proceedings of the 18th ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, co-located with PLDI 2017",
address = "美国",
}