基于SMT的时钟约束语言CCSL的形式化分析方法与工具

摘要

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.%时钟约束语言CCSL是一种用于描述实时嵌入式系统中事件之间约束的形式化语言,它是UML针对实时嵌入式系统建模的扩展包MARTE(modeling and analysis of real-time and embedded systems)中用于对时间建模的一个子语言.给定一组由CCSL定义的时钟约束条件,需要判断是否存在某种调度策略满足约束、是否所有满足这些约束的行为都不会导致系统死锁等分析.目前已经有一定的针对CCSL的形式化分析研究工作,如基于状态迁移系统与时间自动机的方法等.但这些方法要么只针对某种特定的分析,要么只适用于部分CCSL约束,要么分析效率较低.提出了基于SMT的统一且高效的CCSL形式化分析方法.统一性体现在其可用于有效性证明、迹分析、死锁检测、LTL模型检测等方面的验证与分析.基于该方法开发了原型工具,同时支持上述4种验证功能.工具集成了当前最高效的SMT求解器Z3和CVC4.得益于SMT求解器的高效性,实验中大部分的验证可以在短时间内完成.