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

作者简介:

应云辉(1992-),男,浙江宁海人,硕士,主要研究领域为形式化方法;张民(1982-),男,博士,副教授,CCF专业会员,主要研究领域为形式化方法,软件工程.

通讯作者:

张民,E-mail:zhangmin@sei.ecnu.edu.cn

基金项目:

国家自然科学基金(61502171)


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

Fund Project:

National Natural Science Foundation of China (61502171)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
    摘要:

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

    Abstract:

    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.

    参考文献
    相似文献
    引证文献
引用本文

应云辉,张民.基于SMT的时钟约束语言CCSL的形式化分析方法与工具.软件学报,2018,29(6):1595-1606

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
历史
  • 收稿日期:2017-07-01
  • 最后修改日期:2017-09-01
  • 录用日期:2017-11-06
  • 在线发布日期: 2017-12-28
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号