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.