基于SMT的时钟约束语言CCSL的形式化分析方法与工具
基于SMT的时钟约束语言CCSL的形式化分析方法与工具
复制标题
DOI：
10.13328/j.cnki.jos.005469
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
张民
中科院分区：
文献类型：
--
作者：
应云辉;张民
时钟约束语言CCSL是一种用于描述实时嵌入式系统中事件之间约束的形式化语言.它是UML针对实时嵌入式系统建模的扩展包MARTE （Modeling and Analysis of Real-Time and Embedded systems）中用于对时间建模的一个子语言.给定一组由CCSL定义的时钟约束条件，需要判断是否存在某种调度策略满足约束，是否所有满足这些约束的行为都不会导致系统死锁等分析.针对CCSL的形式化分析目前已经有一定的研究工作，如基于状态迁移系统与时间自动机的方法等.但这些方法要么只针对某种特定的分析，要么只适用于部分CCSL约束，要么分析效率较低.本文提出一种基于SMT的统一且高效的CCSL形式化分析方法.统一性体现在其可用于有效性证明、迹分析、死锁检测、LTL模型检测等方面的验证与分析.基于该方法开发了原型工具同时支持上述四种验证功能.工具集成了当前最高效的SMT求解器Z3和CVC4.得益于SMT求解器的高效性，实验中大部分的验证可以在短时间内完成.