Formal Modeling and Verification of Real-Time Multi-Agent Systems: the REMM Framework

Multi Agent Systems represent a new approach for modeling complex and distributed systems. Many efforts of software engineering aim at providing methodologies and tools for designing and developing MAS. However formal verification of MAS dependability is still an open issue. Here we focus on modeling, design and verification of real-time properties in MASs. We propose a methodology that supports developers in different phases of MAS developing cycle. We also present an integrated environment that allows for UML design, code generation, time constraints verification and testing of soft-real time MASs. A case of study is described to demonstrate an application of such methodology and the utilization of developed tools.