SMT-Based Approach to Formal Analysis of CCSL with Tool Support

作者：Ying, Yun Hui; Zhang, Min^*

来源：Journal of Software, 2018, 29(6): 1595-1606.

DOI：10.13328/j.cnki.jos.005469

• CCSL
• Clock constraints
• Deadlock detection
• LTL model-checking
• Model and analysis
• Model driven development
• Real-time and embedded systems
• Validity proving

CCSL (abbreviated for clock constraint specification language) is a formal language for specifying the constraints on the occurrences of events in real-time and embedded systems. CCSL is a companion language of MARTE (abbreviated for modeling and analysis of real-time and embedded systems), a UML profile which provides support for specification, design, and verification/validation stages for model-driven development of real time and embedded Systems. Given a set of CCSL constraints, it is necessary to check if there exist schedules that satisfy all the constraints and if all the behaviors that conforming to the constraints will never incur deadlock of systems. Many approaches have been proposed based on state transition system, timed automata, etc. However, most of the existing approaches have some drawbacks, such as being ad hoc to specific formal analysis, and being suited to only subsets of CCSL constraints or inefficient. In this paper, a unified and efficient SMT-based approach to formal analysis of CCSL is proposed. This approach is unified in that it can be applied to various analysis such as validity proving, trace analysis, deadlock detection and LTL model checking. A prototype tool for the new approach is implemented to support the four types of formal analysis, utilizing the state-of-the-art SMT solvers such as Z3 and CVC4. With efficient SMT solvers, verification can be completed in a reasonable time, as demonstrated by the experimental results in the case studies.

• 出版日期2018
• 单位华东师范大学