计算机科学 ›› 2016, Vol. 43 ›› Issue (8): 137-141.doi: 10.11896/j.issn.1002-137X.2016.08.029
叶俊民,张坤,叶竹君,陈盼,陈曙
YE Jun-min, ZHANG Kun, YE Zhu-jun, CHEN Pan and CHEN Shu
摘要： 运行时验证是一种轻量级的形式化验证方法,使用可视化的需求规约描述语言建模需求规约场景是运行时验证领域的研究热点。针对目前基于活性顺序图的运行时验证方法中容易产生冗余性质、二值语义的验证结果不准确、基于Maude工具引擎的重写逻辑验证算法效率较低等问题,提出一种基于活性顺序图的运行时验证的改进方法,以支持现有的运行时验证技术。实验表明,改进方法验证结果准确,且验证过程开销较小。
| [1] Chen F,Rosu G.Java-MOP:A Monitoring Oriented Programming Environment for Java[M]∥Tools and Algorithms for the Construction and Analysis of Systems.Springer,2005:546-550 [2] ONeil P M,Jin D Y,et al.Efficient Monitoring of ParametricContext-free Patterns[J].Automated Software Engineering,2010,17(2):149-180 [3] Bruegge B,Dutoit A H.Object-Oriented Software Engineering.Using UML,Patterns,and Java(Third Edition)[M].Ye Jun-min,et al.Beijing:Tsinghua University Press,2011(in Chinese) Bruegge B,Dutoit A H.面向对象软件工程(第3版)[M].叶俊民,等译.北京:清华大学出版社,2011 [4] Harel D,Thiagarajan P S.Message Sequence Charts[M]∥UML for Real.Springer,US,2003:537-558 [5] Wang H Y,Wang L,Zhang J C,et al.Control Flow Analysis of UML2.0 Sequence Diagram Based on Message Semantic[J].Journal of Jilin University,2007,5(4):595-600 [6] Damm W,Harel D.LSCs:Breathing Life into Message Sequence Charts[J].Formal Methods in System Design,2001,19(1):45-80 [7] Li Wen-rui,Wang Zhi-jian,Zhang Peng-cheng.Formal Seman-tics of Universal Modal Sequence Diagram[J].Journal of Software,2011,22(4):659-675(in Chinese) 李雯睿,王志坚,张鹏程.模态顺序图uMSD的形式化语义[J].软件学报,2011,22(4):659-675 [8] Larsen K G,Li S.Scenario-based analysis and synthesis of real-time systems using Uppaal[C]∥Proc 13th Conference on Design,Automation,and Test in Europe.2010:447-452 [9] Fu Ming-hui,Zhou Qing-lei,Zhang Bing.Transfer methods from live sequence charts to temporal logic[J].Computer Engineering and Design,2012,33(9):3437-3441(in Chinese) 付明慧,周清雷,张兵.从活性顺序图到时态逻辑的转化方法[J].计算机工程与设计,2012,33(9):3437-3441 [10] Chai M,Schlingloff B H.Monitoring Systems with ExtendedLive Sequence Charts[C]∥14th International Conference on Runtime Verification.Springer,2014:48-63 [11] Kugler H,Harel D,Pnueli A,et al.Temporal logic for scenario-based specifications[C]∥Proc.of the 11th Int.Conf.on Tools and Algorithms for the Construction and Analysis of Systems (TACAS05).2005,3440:445-460 [12] Clavel,Duran,Marti-Oliet,et al.Maude Manual(version 2.6)[M].University of Illinois,Urbana-Champaign 1,2011:1-491 [13] Martí-Oliet N.An Introduction to Maude and Some of Its Applications[M]∥Practical Aspects of Declarative Languages.Springer Berlin Heidelberg,2010:4-9 [14] Zhao Lin,Tang Tao,Xu Tian-hua,et al.Runtime Verificationand its Applications in Train Control System[J].Railway Society,2011,33(12):65-71(in Chinese) 赵琳,唐涛,徐田华,等.运行时验证及其在列车运行控制系统中的应用[J].铁道学报,2011,33(12):65-71 [15] Niu Ru,Cao Yuan,Tang Tao.Formal Modelling and Analysis of RBC Handover protocol for ETCS Level 2 Using Stochastic Petri Nets[J].Railway Society,2009,31(4):52-58(in Chinese) 牛儒,曹源,唐涛.ETCS-2级列控系统RBC交接协议的形式化分析[J].铁道学报,2009,31(4):52-58 [16] ERTMS/ETCS Subset-098:ERTMS/ETCs Class 1 RBC-RBC safe communication interface[EB/OL].http://www.aeif.org/db/docs/ccm/SUBSET-052 v222.2005 [17] Zhao Lin,Tang Tao,Xu Tian-hui,et al.Runtime Verification and its Applications in Train Control Systems[J].Journal of The China Railway Society,2011,3(12):65-71(in Chinese) 赵琳,唐涛,徐田华,等.运行时验证及其在列车运行控制系统中的应用[J].铁道学报,2011,3(12):65-71 |
| No related articles found! |
|
||
首页