Write a Blog >>
LCTES 2017
Wed 21 - Thu 22 June 2017 Barcelona, Spain
co-located with PLDI 2017

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 Jun

15:30 - 17:10: LCTES 2017 - Session 2: Abstraction, Modelling and Scheduling for IoT and Embedded Systems at Vertex WS208
Chair(s): Bernhard ScholzUniversity of Sydney, Australia
LCTES-2017-papers15:30 - 15:55
Weiwen JiangChongqing University, Edwin ShaChongqing University, Qingfeng ZhugeChongqing University, China, Hailiang DongChongqing University, Xianzhang ChenChongqing University
LCTES-2017-papers15:55 - 16:20
Gyeongmin LeePOSTECH, Seonyeong HeoPOSTECH, Bongjun KimPOSTECH, Jong KimPOSTECH, Hanjun KimPOSTECH
LCTES-2017-papers16:20 - 16:45
Min ZhangEast China Normal University, Yunhui Ying
LCTES-2017-papers16:45 - 17:10
Wenguang Zheng, Hui WuUniversity of New South Wales, Australia, Chuanyao NieThe University of New South Wales