Critical systems verification in MetaMORP(h)OSY

Multi Agent Systems (MAS) methodologies are emerging as a new approach for modeling and developing complex distributed sys- tems. When complex constraints have to be veried on critical systems Model Driven Engineering (MDE) methodologies allow for the design and implementation of systems correct by construction. Usually verication is enforced by formal analysis. This paper presents MetaMORP(h)OSY (Meta-modeling of Mas Object-based with Real-time specication in Project Of complex SYstems) methodology and framework. They pro- vide a mean for building MAS models used to verify properties (and requirements) of Critical Systems following a MDE approach. In partic- ular, this work describes model transformation algorithms used in Meta- MORP(h)OSY to verify real-time and timed reachability requirements.