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

摘要：

时钟约束语言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模型检测、工具

所属期刊栏目：29

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金61502171National Natural Science Foundation of China 61502171

在线出版日期：2018-07-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共12页

页码：1595-1606