基于博弈论的开放环境下场景规约监控语义

在开放环境中,环境和系统本身行为的改变可能使得软件系统的实现不再满足原来规约,从而最终导致软件失效的发生.运行时监控是一种轻量级的形式化动态验证技术,已成为开放环境下检测软件失效的基本手段.针对基于场景的规约属性序列图,从博弈论的角度定义其多值监控语义:满足、无限可控、系统有限可控、系统紧急可控、环境有限可控、环境紧急可控和违例.通过多值监控语义的定义,监控器能够根据当前轨迹尽可能早地检测到系统失效或异常,并提供足够信息为失效的预防和恢复服务.实例研究表明了属性序列图多值监控语义的实用价值,并显示了其广泛的应用前景.

Game-based monitors for a scenario-based specification in open environments

In open environments, unsafe run-time changes of systems and environments may compromise the correct execution of the entire systems and make the software systems do not meet the original specifications which may eventually lead to the occurrence of software failures. Runtime monitor which is a lightweight formal dynamic verification technology has become the basic means of detecting software failures in open environments For scenario-based specification property sequence charts, this paper defines the multi-valued monitoring semantics from the perspective of game theory： satisfied, infinitely controllable, the system is finitely controllable, the system is emergency controllable, the environment is finitely controllable, tile environment is emergency controllable violated. Through the multi-valued semantics definition, the monitor can detect failures as early as possible and also provide sufficient information to help the system to take measures for failure prevention and recovery. Finally the property sequence chart used in RailCab case study shows its extensive application prospect