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

来源：软件学报杂志2018年第6期北京时间：

作者：应云辉,张民

单位：应云辉，华东师范大学 计算机科学与软件工程学院, 上海 200062;高可信软件国家重点实验室(华东师范大学), 上海 20006211,张民，华东师范大学 计算机科学与软件工程学院, 上海 200062;高可信软件国家重点实验室(华东师范大学), 上海 20006202

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

关键词：CCSL;SMT;有效性证明;迹分析;死锁检测;LTL模型检测;工具

基金资助：国家自然科学基金（61502171）