Runtime verification of programs using rulebased active system

Runtime verification, monitoring and checking runtime behaviors, plays an increasingly important role to realize tasks that have become inefficient with static verification and implementation testing. In this paper, we propose a new approach based on a framework to dynamic verification programs. The framework exploits capabilities of active systems for verifying programs. Active systems are ones those act based on occurrence of events and therefore it facilitates trapping events and monitoring program s states. The active system is a rule-based system and we use ECA rules to show active rules in the active system. Thus, defining active behavior is facilitated by ECA rules. ECA rules are verifier rules in form of event-condition-action. These rules, forming runtime monitor, verify behavior of system whenever an event occur during program execution. Exploiting active systems as event based environments and using ECA rules in context of them, are main contributions of our approach to runtime verification. An active system, forming runtime environment, sets a trap to catch runtime events and then check them by the ECA rules. We apply our approach to a classical Abstract Data Type (ADT), stack, and express how one can use an active environment to verify safety properties of a stack.