Formal Development of Multi-Agent Systems with FPASSI: Towards Formalizing PASSI Methodology using Rewriting Logic
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:
PDFReferences
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.
This work is licensed under a Creative Commons Attribution 3.0 License.