Paper Info
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.
Year
DOI
Venue
2017
10.1145/3078633.3081035
LCTES
Keywords
Field
DocType
Model checking,SMT,Z3,CCSL,LTL
Programming language,Model checking,Clock constraint specification language,Computer science,Theoretical computer science,Real-time computing,Linear temporal logic,Uml profile,Satisfiability modulo theories,Control theory,Formal language,Traffic signal,Embedded system
Conference
Volume
Issue
ISSN
52
5
0362-1340
Citations 
PageRank 
References 
4
0.45
15
Authors
2
Name
Order
Citations
PageRank
Min Zhang174.23
Yunhui Ying240.45