Computer Science ›› 2014, Vol. 41 ›› Issue (9): 84-87.doi: 10.11896/j.issn.1002-137X.2014.09.015

Previous Articles     Next Articles

PSC2GS:A Tool for Generating Monitors Based on Property Sequence Charts

YU Jun,ZHANG Peng-cheng,ZHOU Yu-peng and LIU Zong-lei   

  • Online:2018-11-14 Published:2018-11-14

Abstract: In open and dynamic environments,unsafe run-time changes of system or environments may compromise the correct execution of the entire system.It may eventually lead to the occurrence of software failures.Run-time verification techniques based on monitors have become the basic means of detecting software failures in open environments.This tool proposes an automated approach to generate monitors from property sequence charts based on game theory.The monitors are interpreted in multi-valued semantics:satisfied,infinitely controllable,system finitely controllable,system urgently controllable,environment finitely controllable,environment urgently controllable,and violated.The monitors can provide enough information to help the system to take measures for failure prediction or prevention.This paper described a novel tool called ‘PSC2GS’,which is able to design property sequence charts,generate game structure based on property sequence charts and generate Aspect Oriented Programming codes (the Monitor) based on game structure.The tool chain provides a completely graphical front-end which can make software designers do not have to deal with any particular textual and logical formalism.

Key words: Run-time verification,Monitor,Property sequence charts,Aspect oriented programming

[1] de Alfaro L,Stoelinga M.Interfaces:A game-theoretic framework for reasoning about component-based systems[J].Electr.Notes Theor.Comput.Sci.,2004,97:3-23
[2] Zhang X,Leucker M,Dong W.Runtime verification with predictive semantics[C]∥NASA Formal Methods.2012:418-432
[3] Giannakopoulou D,Havelund K.Automata- based verification of temporal properties on running programs[C]∥ASE 2001 .IEEE Computer Society,2001:412-416
[4] Harel D,Segall I.Synthesis from scenario-based specifications[J].J.Comput.Syst.Sci.,2012,78(3):970-980
[5] 张鹏程,李宣东,李雯睿.基于博弈论的开放环境下场景规约监控语义[J].中国科学信息科学,2013
[6] Zhang P,Yu J,Li W,et al.Game-based monitors for scenario-based specifications[C]∥The 18th International Conference on Engineering of Complex Computer Systems (ICECCS2013).2013:264-267
[7] PSC Project.PSC Web site.http://www.di.univaq.it/psc2ba,2005
[8] Autili M,Inverardi P,Elliccione P P.A scenario based notation for specifying temporal properties [C]∥The 5th SCESM06,ICSE06.Shanghai,2006
[9] The AspectJ Project.AspectJ Web site.http://eclipse.org/aspectj/
[10] Ehlers R,Finkbeiner B.Monitoring realizability[C]∥RV 2011.2011:427-441
[11] Jin D,Meredith P O,Lee C,et al.Javamop:Efficient parametric runtime monitoring framework[C]∥ICSE.2012:1427-1430
[12] Allan C,Avgustinov P,Christensen A S,et al.Adding tracematching with free variables to aspectj[C]∥OOPSLA.2005:345-364

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!