A Model-Driven CASE tool for developing and verifying regulated open MAS

This paper describes a CASE tool for developing complex systems in which heterogeneous and autonomous agents may need to coexist in a complex social and legal framework. Model-Driven Technologies are used to integrate the design of systems of this kind with the verification of the models and with the generation of executable code from these models. The verification module is based on model-checking techniques to check the coherence of a modeled legal context at design time is presented and it is exemplified with a case study.

► We describe a development process for Regulated Open Multi-agent Systems.
► Eclipse technology is used to integrate a modeling tool with a verifier module.
► Xpand plug-in is used to automatically transform models into verifiable code.
► Models are verified by means of the SPIN model checker.