关键词: 运行时验证,监控器,属性序列图,面向方面编程

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