Qualitative Verification of Multi-Agents Reactive Decisional System Using Business Process Modeling Notation

A Reactive system is one that is in continual interaction with its environment, and executes at a pace determined by that environment. Due to their complex nature, reactive systems are extremely difficult to specify and validate. In this paper, we propose a new formal model for verification of such systems using Business Process Modeling Notation (BPMN). This approach considers a Reactive System as a Reactive Multi-Agent System consisting of concurrent reactive agents that cooperate with each other to achieve the desired functionality. BPMN is used as a verification tool in order to verify the systems behaviors.