Computer Science ›› 2016, Vol. 43 ›› Issue (8): 137-141.doi: 10.11896/j.issn.1002-137X.2016.08.029

Previous Articles     Next Articles

Research of Runtime Verification Based on Live Sequence Chart

YE Jun-min, ZHANG Kun, YE Zhu-jun, CHEN Pan and CHEN Shu   

  • Online:2018-12-01 Published:2018-12-01

Abstract: Runtime verification is a lightweight formal verification method.Using visual requirements description language to model requirements specification scene is a hotspot in runtime verification.For the problems that existing verification 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 rewriting 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.

Key words: Live sequence chart,Linear temporal logic,Rewriting logic,Runtime verification

[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!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!