主页期刊介绍编委会编辑部服务介绍道德声明在线审稿编委办公编辑办公English
2018-2019年专刊出版计划 微信服务介绍 最新一期:2018年第12期
     
在线出版
各期目录
纸质出版
分辑系列
论文检索
论文排行
综述文章
专刊文章
美文分享
各期封面
E-mail Alerts
RSS
旧版入口
中国科学院软件研究所
  
投稿指南 问题解答 下载区 收费标准 在线投稿
应云辉,张民.基于SMT的时钟约束语言CCSL的形式化分析方法与工具.软件学报,2018,29(6):1595-1606
基于SMT的时钟约束语言CCSL的形式化分析方法与工具
SMT-Based Approach to Formal Analysis of CCSL with Tool Support
投稿时间:2017-07-01  修订日期:2017-09-01
DOI:10.13328/j.cnki.jos.005469
中文关键词:  CCSL  SMT  有效性证明  迹分析  死锁检测  LTL模型检测  工具
英文关键词:CCSL  SMT  validity proving  trace analysis  deadlock detection  LTL model checking  tool
基金项目:国家自然科学基金(61502171)
作者单位E-mail
应云辉 华东师范大学 计算机科学与软件工程学院, 上海 200062
高可信软件国家重点实验室(华东师范大学), 上海 200062 
 
张民 华东师范大学 计算机科学与软件工程学院, 上海 200062
高可信软件国家重点实验室(华东师范大学), 上海 200062 
zhangmin@sei.ecnu.edu.cn 
摘要点击次数: 826
全文下载次数: 566
中文摘要:
      时钟约束语言CCSL是一种用于描述实时嵌入式系统中事件之间约束的形式化语言,它是UML针对实时嵌入式系统建模的扩展包MARTE (modeling and analysis of real-time and embedded systems)中用于对时间建模的一个子语言.给定一组由CCSL定义的时钟约束条件,需要判断是否存在某种调度策略满足约束、是否所有满足这些约束的行为都不会导致系统死锁等分析.目前已经有一定的针对CCSL的形式化分析研究工作,如基于状态迁移系统与时间自动机的方法等.但这些方法要么只针对某种特定的分析,要么只适用于部分CCSL约束,要么分析效率较低.提出了基于SMT的统一且高效的CCSL形式化分析方法.统一性体现在其可用于有效性证明、迹分析、死锁检测、LTL模型检测等方面的验证与分析.基于该方法开发了原型工具,同时支持上述4种验证功能.工具集成了当前最高效的SMT求解器Z3和CVC4.得益于SMT求解器的高效性,实验中大部分的验证可以在短时间内完成.
英文摘要:
      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.
HTML  下载PDF全文  查看/发表评论  下载PDF阅读器
 

京公网安备 11040202500064号

主办单位:中国科学院软件研究所 中国计算机学会
编辑部电话:+86-10-62562563 E-mail: jos@iscas.ac.cn
Copyright 中国科学院软件研究所《软件学报》版权所有 All Rights Reserved
本刊全文数据库版权所有,未经许可,不得转载,本刊保留追究法律责任的权利