Efficient SMT-based LTL Model Checking of Clock Constraint Specification Language for Real-Time and Embedded Systems
MARTE (abbreviated for Modeling and Analysis of Real-Time and Embedded systems) is a UML profile, used to facilitate the design and analysis of real-time and embedded systems. The Clock Constraint Specification Language (CCSL) is a formal language companion to MARTE, which is proposed to specify the constraint of the occurrences of events in systems. However, the language lacks efficient verification support to the formal analysis of temporal properties which are important 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. We implement a prototype tool for the proposed approach and use the state-of-the-art tool Z3 as the underlying SMT solver. We model two practical cases including a traffic light controller and a power window system in CCSL, and verify LTL properties of the two systems using the proposed approach. Experimental results demonstrate the effectiveness of our approach.
Wed 21 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:30 - 17:10
|Optimal Functional Unit Assignment and Voltage Selection for Pipelined MPSoC with Guaranteed Probability on Time Performance|
|Integrated IoT Programming with Selective Abstraction|
|Efficient SMT-based LTL Model Checking of Clock Constraint Specification Language for Real-Time and Embedded Systems|
|Integrating Task Scheduling and Cache Locking for Multicore Real-time Embedded Systems|