Agent-oriented Software Engineering (AOSE)
ASPECS - Agent-oriented Software Process for Engineering Complex Systems
Our team proposes a methodology, named ASPECS, covering the analysis, design and implementation of (holonic) multi-agent systems (H/MAS). This methodology is based upon an holonic organisational metamodel and provides a step-by-step guide from requirements to code allowing the modelling of a system at different levels of details using a set of refinement methods. It integrates design models and philosophies from both object- and agent-oriented software engineering (OOSE and AOSE). It has been built by adopting the Model Driven Architecture (MDA) and thus we defined three levels of models. The main concepts of the organizational metamodels are roles, interactions and organizations. These concepts allow for abstraction and decomposition of MAS and HMAS. ASPECS uses UML as modelling language, the UML semantics and notation are used as reference points, but they have been extended by introducing new specific profiles to fulfil the specific needs of agents and holonic organisational design. The Janus platform provides an implementation and execution environment for models designed with ASPECS.
Multi-Agent Systems formal specification and verification
Associated to the ASPECS methodology, we have defined a multi-formalisms notation, named OZS, integrating Object-Z and Statecharts. An operational semantic have been defined for this formal notation. With this semantic, we are able to use specific software environments such as Statemate, STeP or SAL which enable validation and/or verification of specifications. The validation is based upon statecharts animations and/or specification simulations using tools such as path finder or random trace generators. The verification part uses theorem provers and model checkers. In order to reduce complexity issues related to proofs we are investigating compositional proofs and abstraction techniques.
