一种基于活性顺序图的运行时验证研究  

Research of Runtime Verification Based on Live Sequence Chart

作　　者：叶俊民[1] 张坤[1] 叶竹君 陈盼[1] 陈曙[1] YE Jun-min ZHANG Kun YE Zhu-jun CHEN Pan CHEN Shu(School of Computer Science, Central China Normal University, Wuhan 430079, China Personnel Training Station of National Physics,Central China Normal University,Wuhan 430079,China)

机构地区：[1]华中师范大学计算机学院,武汉430079 [2]华中师范大学国家物理学人才培养基地,武汉430079

出　　处：《计算机科学》2016年第8期137-141,164,共6页Computer Science

基　　金：国家科技支撑计划项目(2015BAK33B00);中央高校基本科研业务费专项资金科研项目(CCNU15GF003);教育部人文社会科学研究规划基金(15YJA880095)资助

摘　　要：运行时验证是一种轻量级的形式化验证方法,使用可视化的需求规约描述语言建模需求规约场景是运行时验证领域的研究热点。针对目前基于活性顺序图的运行时验证方法中容易产生冗余性质、二值语义的验证结果不准确、基于Maude工具引擎的重写逻辑验证算法效率较低等问题,提出一种基于活性顺序图的运行时验证的改进方法,以支持现有的运行时验证技术。实验表明,改进方法验证结果准确,且验证过程开销较小。Runtime verification is a lightweight formal verification method. Using visual requirements description lan- guage to model requirements specification scene is a hotspot in runtime verification. For the problems that existing veri- fication methods based on live sequence chart easily generate redundant properties, verification overhead is quite large, two true value semantics verification result is not accurate and the efficiency of existing verification algorithm of rewri- ting logic based on Maude is low, this paper proposed an improved runtime verification method based on live sequence chart to support existing runtime verification technologies. Experiments show that the result of improved method in this paper is accurate and verification overhead is low.

关 键 词：活性顺序图 线性时序逻辑 重写逻辑 运行时验证 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]