Formal Development of Multi-Agent Systems with FPASSI: Towards Formalizing PASSI Methodology using Rewriting Logic

Mihoub Mazouz, Farid Mokhati, Mourad Badri

Abstract


Agent technology has showed its ability and efficiency in modeling complex distributed
applications. During the last two decades, several MAS development methodologies have been
proposed like, for instance, Gaia, Tropos, and PASSI. Although these methodologies have
made significant contributions to meet several challenges in the MAS development field, most
of them do not use formal techniques. Formal methods, as it is well known, play a significant
role in developing more reliable and robust MAS. This paper presents the Formal-PASSI
methodology, an extension of the well-known PASSI methodology. The extension consists
mainly of the integration of a new formal model to the design process. The new model is based
on the Maude language and its extension Maude-Strategy, and aims to offer a formal
description of the MAS under development by a Model-to-Text transformation. The generated
formal description is then used to: (1) validate some PASSI behavioral diagrams, and (2) check
properties of both single & multi agent(s) abstraction level before passing to the code model.
Integrating formal methods into PASSI design process seems a good way to assure the
development of high quality agent-based applications. The proposed approach is supported by
a tool (F-PTK) that we developed and illustrated throughout the ATM case study.


Full Text:

PDF

References


Cossentino, M. (2005). "From requirements to code with the PASSI methodology."

Agent-oriented methodologies 3690: 79-106.

Cossentino, M. and V. Seidita (2014). PASSI: Process for Agent Societies Specification

and Implementation. Handbook on Agent-Oriented Design Processes. M. Cossentino,

V. Hilaire, A. Molesini and V. Seidita, Springer Berlin Heidelberg: 287-329.

Cernuzzi, L., T. Juan, L. Sterling and F. Zambonelli (2004). The Gaia Methodology.

Methodologies and Software Engineering for Agent Systems: The Agent-Oriented

Software Engineering Handbook. F. Bergenti, M.-P. Gleizes and F. Zambonelli. Boston,

MA, Springer US: 69-88.

Cernuzzi, L., A. Molesini and A. Omicini (2014). The Gaia Methodology Process.

Handbook on Agent-Oriented Design Processes. M. Cossentino, V. Hilaire, A. Molesini

and V. Seidita. Berlin, Heidelberg, Springer Berlin Heidelberg: 141-172.

Bernon, C., M.-P. Gleizes, S. Peyruqueou and G. Picard (2003). ADELFE: A

Methodology for Adaptive Multi-agent Systems Engineering. Engineering Societies in

the Agents World III: Third International Workshop, ESAW 2002 Madrid, Spain,

September 16–17, 2002 Revised Papers. P. Petta, R. Tolksdorf and F. Zambonelli.

Berlin, Heidelberg, Springer Berlin Heidelberg: 156-169.

Bonjean, N., W. Mefteh, M. P. Gleizes, C. Maurel and F. Migeon (2014). ADELFE 2.0.

Handbook on Agent-Oriented Design Processes. M. Cossentino, V. Hilaire, A. Molesini

and V. Seidita. Berlin, Heidelberg, Springer Berlin Heidelberg: 19-63.

Mefteh, W., F. Migeon, M.-P. Gleizes and F. Gargouri (2015). ADELFE 3.0 Design,

Building Adaptive Multi Agent Systems Based on Simulation a Case Study.

Computational Collective Intelligence: 7th International Conference, ICCCI 2015,

Madrid, Spain, September 21-23, 2015, Proceedings, Part I. M. Núñez, T. N. Nguyen,

D. Camacho and B. Trawiński. Cham, Springer International Publishing: 19-28.

Winikoff, M. and L. Padgham (2004). The Prometheus Methodology. Methodologies

and Software Engineering for Agent Systems: The Agent-Oriented Software

Engineering Handbook. F. Bergenti, M.-P. Gleizes and F. Zambonelli. Boston, MA,

Springer US: 217-234.

Giorgini, P., M. Kolp, J. Mylopoulos and M. Pistore (2004). The Tropos Methodology.

Methodologies and Software Engineering for Agent Systems. F. Bergenti, M.-P. Gleizes

and F. Zambonelli, Springer US. 11: 89-106.

Pavón, J. and J. Gómez-Sanz (2003). Agent Oriented Software Engineering with

INGENIAS. Multi-Agent Systems and Applications III: 3rd International Central and

Eastern European Conference on Multi-Agent Systems, CEEMAS 2003 Prague, Czech

Republic, June 16–18, 2003 Proceedings. V. Mařík, M. Pěchouček and J. Müller.

Berlin, Heidelberg, Springer Berlin Heidelberg: 394-403.

Winikoff, M. (2010). Assurance of Agent Systems: What Role Should Formal

Verification Play? Specification and Verification of Multi-agent Systems. M. Dastani,

V. K. Hindriks and C. J.-J. Meyer. Boston, MA, Springer US: 353-383.

Cossentino, M. and C. Potts (2002). "PASSI: A process for specifying and

implementing multi-agent systems using UML." Retrieved October 8: 2007.

Basin, D., M. Clavel and J. Meseguer (2000). Rewriting Logic as a Metalogical

Framework. FST TCS 2000: Foundations of Software Technology and Theoretical

Computer Science: 20th Conference New Delhi, India, December 13–15, 2000

Proceedings. S. Kapoor and S. Prasad. Berlin, Heidelberg, Springer Berlin Heidelberg:

-80.

Meseguer, J. (2005). A Rewriting Logic Sampler. Theoretical Aspects of Computing –

ICTAC 2005: Second International Colloquium, Hanoi, Vietnam, October 17-21, 2005.

Proceedings. D. Hung and M. Wirsing. Berlin, Heidelberg, Springer Berlin Heidelberg:

-28.

Clavel, M., F. Durán, S. Eker, P. Lincoln, N. Martı́

-Oliet, J. Meseguer and J. F. Quesada

(2002). "Maude: specification and programming in rewriting logic." Theoretical

Computer Science 285(2): 187-243.

Clavel, M., F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, José, Meseguer and C. Talcott

(2007). All about maude - a high-performance logical framework: how to specify,

program and verify systems in rewriting logic, Springer-Verlag.

N. Martí-Oliet, José, Meseguer and A. Verdejo (2005). "Towards a Strategy Language

for Maude." Electron. Notes Theor. Comput. Sci. 117: 417-441.

Eker, S., J. Meseguer and A. Sridharanarayanan (2003). The Maude LTL Model

Checker and Its Implementation. Model Checking Software: 10th International SPIN

Workshop Portland, OR, USA, May 9–10, 2003 Proceedings. T. Ball and S. K.

Rajamani. Berlin, Heidelberg, Springer Berlin Heidelberg: 230-234.

Fallah-Seghrouchni, A., J. J. Gomez-Sanz and M. P. Singh (2011). Formal Methods in

Agent-Oriented Software Engineering. Agent-Oriented Software Engineering X: 10th

International Workshop, AOSE 2009, Budapest, Hungary, May 11-12, 2009, Revised

Selected Papers. M.-P. Gleizes and J. J. Gomez-Sanz. Berlin, Heidelberg, Springer

Berlin Heidelberg: 213-228.

Ball, E. (2008). An Incremental Process for the Development of Multi-agent Systems in

Event-B Doctoral, University of Southampton.

Ball, E. and M. Butler (2006). Using Decomposition to Model Multi-agent Interaction

Protocols in Event-B. FM'06 Doctoral Symposium, Springer.

Abrial, J.-R. (2010). Modeling in Event-B: System and Software Engineering,

Cambridge University Press.

Ball, E. and M. Butler (2009). Event-B Patterns for Specifying Fault-Tolerance in

Multi-agent Interaction. Methods, Models and Tools for Fault Tolerance. M. Butler, C.

Jones, A. Romanovsky and E. Troubitsyna. Berlin, Heidelberg, Springer Berlin

Heidelberg: 104-129.

Hadj-Kacem, A., A. Regayeg and M. Jmaiel (2007). "ForMAAD: A formal method for

agent-based application design." Web Intelli. and Agent Sys. 5(4): 435-454.

Graja, Z., A. Regayeg and A. H. Kacem (2011). ForMAAD : Towards a Model Driven

Approach for Agent Based Application Design. Agent-Oriented Software Engineering

XI: 11th International Workshop, AOSE 2010, Toronto, Canada, May 10-11, 2010,

Revised Selected Papers. D. Weyns and M.-P. Gleizes. Berlin, Heidelberg, Springer

Berlin Heidelberg: 148-164.

Cervenka, R. and I. Trencansky (2007). The Agent Modeling Language - AML: A

Comprehensive Approach to Modeling Multi-Agent Systems, Birkhäuser Basel.

Regayeg, A., Hadj-Kacem, A., Jmaiel, M. (2004). Specification and Verification of

Multi-Agent Applications using Temporal Z. In Proceedings of the IEEE/WIC/ACM

International Conference on Intelligent Agent Technology 2004 (IAT'2004), Beijing,

China: 260–266.

Fuxman, A., M. Pistore, J. Mylopoulos and P. Traverso (2001). Model checking early

requirements specifications in Tropos. Requirements Engineering, 2001. Proceedings.

Fifth IEEE International Symposium on, IEEE.

Dardenne, A., A. v. Lamsweerde and S. Fickas (1993). Goal-directed requirements

acquisition. Selected Papers of the Sixth International Workshop on Software

Specification and Design, Elsevier Science Publishers B. V.: 3-50.

Cimatti, A., E. Clarke, F. Giunchiglia and M. Roveri (2000). "NUSMV: a new symbolic

model checker." International Journal on Software Tools for Technology Transfer 2(4):

-425.

Montali, M., P. Torroni, N. Zannone, P. Mello and V. Bryl (2011). "Engineering and

verifying agent-oriented requirements augmented by business constraints with

Tropos." Autonomous Agents and Multi-Agent Systems 23(2): 193-223.

Bryl, V., P. Mello, M. Montali, P. Torroni and N. Zannone (2008).

Computational Logic in Multi-Agent Systems: 8th International Workshop, CLIMA

VIII, Porto, Portugal, September 10-11, 2007. Revised Selected and Invited Papers. F.

Sadri and K. Satoh. Berlin, Heidelberg, Springer Berlin Heidelberg: 157-176.

Alberti, M., F. Chesani, M. Gavanelli, E. Lamma, P. Mello and P. Torroni (2008).

"Verifiable agent interaction in abductive logic programming: The SCIFF framework."

ACM Trans. Comput. Logic 9(4): 1-43.

Fadil, H. and J.-L. Koning (2005). A Formal Approach to Model Multiagent

Interactions Using the B Formal Method. Advanced Distributed Systems: 5th

International School and Symposium, ISSADS 2005, Guadalajara, Mexico, January 24-

, 2005, Revised Selected Papers. F. F. Ramos, V. Larios Rosillo and H. Unger.

Berlin, Heidelberg, Springer Berlin Heidelberg: 516-528.

Abrial, J.-R. (1996). The B-book: assigning programs to meanings, Cambridge

University Press.

Robinson, K. (1997). The B method and the B toolkit. Algebraic Methodology and

Software Technology: 6th International Conference, AMAST'97 Sydney, Australia,

December13–17, 1997 Proceedings. M. Johnson. Berlin, Heidelberg, Springer Berlin

Heidelberg: 576-580.

Jemni Ben Ayed, L. and F. Siala (2008). Specification and Verification of Multi-agent

Systems Interaction Protocols Using a Combination of AUML and Event B. Interactive

Systems. Design, Specification, and Verification: 15th International Workshop, DSV-IS

Kingston, Canada, July 16-18, 2008 Revised Papers. T. C. N. Graham and P.

Palanque. Berlin, Heidelberg, Springer Berlin Heidelberg: 102-107.

Bauer, B., J. P. Müller and J. Odell (2001). Agent UML: A Formalism for Specifying

Multiagent Software Systems. Agent-Oriented Software Engineering: First International

Workshop, AOSE 2000 Limerick, Ireland, June 10, 2000 Revised Papers. P. Ciancarini

and M. J. Wooldridge. Berlin, Heidelberg, Springer Berlin Heidelberg: 91-103.

Alagar, V. S. and K. Periyasamy (1998). The Z Notation. Specification of Software

Systems. New York, NY, Springer New York: 281-360.

Regayeg , A., Hadj Kacem ,A., Jmaiel, M, (2005). Towards a formal methodology for

developing multi-agent applications using temporal Z. The 3rd ACS/IEEE International

Conference on Computer Systems and Applications (AICCSA'05), Cairo, Egypt.

Roungroongsom, C. and D. Pradubsuwun (2015). Formal Verification of Multi-agent

System Based on JADE: A Semi-runtime Approach. Recent Advances in Information

and Communication Technology 2015: Proceedings of the 11th International

Conference on Computing and Information Technology (IC2IT). H. Unger, P. Meesad

and S. Boonkrong. Cham, Springer International Publishing: 297-306.

Lapouchnian, A. and Y. Lespérance (2009). Using the ConGolog and CASL Formal

Agent Specification Languages for the Analysis, Verification, and Simulation of i*

Models. Conceptual Modeling: Foundations and Applications: Essays in Honor of John

Mylopoulos. A. T. Borgida, V. K. Chaudhri, P. Giorgini and E. S. Yu. Berlin,

Heidelberg, Springer Berlin Heidelberg: 483-503.

Yu, E. S.-K. (1996). Modelling strategic relationships for process reengineering,

University of Toronto.

De Giacomo, G., Y. Lespérance and H. J. Levesque (2000). "ConGolog, a concurrent

programming language based on the situation calculus." Artificial Intelligence 121(1):

-169.

Shapiro, S., Y. Lespérance and H. J. Levesque (2002). The cognitive agents

specification language and verification environment for multiagent systems.

Proceedings of the first international joint conference on Autonomous agents and

multiagent systems: part 1. Bologna, Italy, ACM: 19-26.

Wang, X. and Y. Lespérance (2001). "Agent-oriented requirements engineering using

ConGolog and i*." Agent-Oriented Information Systems Workshop (AOIS-2001).

Montreal, Canada: 59-78.

Lapouchnian, A. and Y. Lespérance (2006). Modeling Mental States in Agent-Oriented

Requirements Engineering. Advanced Information Systems Engineering: 18th

International Conference, CAiSE 2006, Luxembourg, Luxembourg, June 5-9, 2006.

Proceedings. E. Dubois and K. Pohl. Berlin, Heidelberg, Springer Berlin Heidelberg:

-494.

Xu, H. and S. M. Shatz "ADK: An Agent Development Kit Based on a Formal Design

Model for Multi-Agent Systems." Automated Software Engineering 10(4): 337-365.

Deng, Y., S. K. Chang, J. C. A. Figueired and A. Perkusich (1993). Integrating software

engineering methods and Petri nets for the specification and prototyping of complex

information systems. Application and Theory of Petri Nets 1993: 14th International

Conference Chicago, Illinois, USA, June 21–25, 1993 Proceedings. M. Ajmone Marsan.

Berlin, Heidelberg, Springer Berlin Heidelberg: 206-223.

Stamatopoulou, I., P. Kefalas and M. Gheorghe (2008). OPERAS: A Framework for the

Formal Modelling of Multi-Agent Systems and Its Application to Swarm-Based

Systems. Engineering Societies in the Agents World VIII: 8th International Workshop,

ESAW 2007, Athens, Greece, October 22-24, 2007, Revised Selected Papers. A.

Artikis, G. M. P. O’Hare, K. Stathis and G. Vouros. Berlin, Heidelberg, Springer Berlin

Heidelberg: 158-174.

Eilenberg, S. (1974). Automata, Languages, and Machines, Academic Press, Inc.

Bernardini, F. and Gheorghe, M (2004). "Population P Systems." Journal of Universal

Computer Science 10(5): 509–539.

Keller, R. M. (1976). "Formal verification of parallel programs." Commun. ACM 19(7):

-384.

Murata, T. (1989). "Petri nets: Properties, analysis and applications." Proceedings of the

IEEE 77(4): 541-580.

Milner, R. (1982). A Calculus of Communicating Systems, Springer-Verlag New York,

Inc.

Diaconescu, R. and Futatsugi, K. (1998). "CafeOBJ Report: The Language, Proof

Techniques, and Methodologies for Object-Oriented Algebraic Specification." AMAST

Series in Computing, vol. 6. World Scientific.

Ölveczky, P. C. and J. Meseguer (2008). The Real-Time Maude Tool. Tools and

Algorithms for the Construction and Analysis of Systems: 14th International

Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory

and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008.

Proceedings. C. R. Ramakrishnan and J. Rehof. Berlin, Heidelberg, Springer Berlin

Heidelberg: 332-336.

Chella, A., M. Cossentino and L. Sabatucci (2004). "Tools and patterns in designing

multi-agent systems with PASSI." WSEAS Transactions on Communications 3(1): 352-

Caire, G., M. Cossentino, A. Negri, A. Poggi and P. Turci (2004). Multi-agent systems

implementation and testing, na.

Mazouz, M., F. Mokhati and M. Badri (2015). Towards an Explicit Bidirectional

Requirement-to-Code Traceability Meta-model for the PASSI Methodology.

Proceedings of the International Conference on Agents and Artificial (ICAART-2015),

Lisbon, Portugal: 203-209.




Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 License.