FSP and FLTL framework for specification and verification of middle-agents

Amelia Bădică; Costin Bădică

International Journal of Applied Mathematics and Computer Science (2011)

  • Volume: 21, Issue: 1, page 9-25
  • ISSN: 1641-876X

Abstract

top
Agents are a useful abstraction frequently employed as a basic building block in modeling service, information and resource sharing in global environments. The connecting of requester with provider agents requires the use of specialized agents known as middle-agents. In this paper, we propose a formal framework intended to precisely characterize types of middle-agents with a special focus on matchmakers, brokers and front-agents by formally modeling their interactions with requesters and providers. Our approach is based on capturing interaction protocols between requesters, providers and middle-agents as finite state processes represented using FSP process algebra. The resulting specifications are formally verifiable using FLTL temporal logic. The main results of this work include (i) precise specification of interaction protocols depending on the type of middle-agent (this can also be a basis for characterizing types of middle-agents), (ii) improvement of communication between designers and developers and facilitation of formal verification of agent systems, (iii) guided design and implementation of agent-based software systems that incorporate middle-agents.

How to cite

top

Amelia Bădică, and Costin Bădică. "FSP and FLTL framework for specification and verification of middle-agents." International Journal of Applied Mathematics and Computer Science 21.1 (2011): 9-25. <http://eudml.org/doc/208041>.

@article{AmeliaBădică2011,
abstract = {Agents are a useful abstraction frequently employed as a basic building block in modeling service, information and resource sharing in global environments. The connecting of requester with provider agents requires the use of specialized agents known as middle-agents. In this paper, we propose a formal framework intended to precisely characterize types of middle-agents with a special focus on matchmakers, brokers and front-agents by formally modeling their interactions with requesters and providers. Our approach is based on capturing interaction protocols between requesters, providers and middle-agents as finite state processes represented using FSP process algebra. The resulting specifications are formally verifiable using FLTL temporal logic. The main results of this work include (i) precise specification of interaction protocols depending on the type of middle-agent (this can also be a basis for characterizing types of middle-agents), (ii) improvement of communication between designers and developers and facilitation of formal verification of agent systems, (iii) guided design and implementation of agent-based software systems that incorporate middle-agents.},
author = {Amelia Bădică, Costin Bădică},
journal = {International Journal of Applied Mathematics and Computer Science},
keywords = {multi-agent system; interaction protocol; process algebra; formal specification},
language = {eng},
number = {1},
pages = {9-25},
title = {FSP and FLTL framework for specification and verification of middle-agents},
url = {http://eudml.org/doc/208041},
volume = {21},
year = {2011},
}

TY - JOUR
AU - Amelia Bădică
AU - Costin Bădică
TI - FSP and FLTL framework for specification and verification of middle-agents
JO - International Journal of Applied Mathematics and Computer Science
PY - 2011
VL - 21
IS - 1
SP - 9
EP - 25
AB - Agents are a useful abstraction frequently employed as a basic building block in modeling service, information and resource sharing in global environments. The connecting of requester with provider agents requires the use of specialized agents known as middle-agents. In this paper, we propose a formal framework intended to precisely characterize types of middle-agents with a special focus on matchmakers, brokers and front-agents by formally modeling their interactions with requesters and providers. Our approach is based on capturing interaction protocols between requesters, providers and middle-agents as finite state processes represented using FSP process algebra. The resulting specifications are formally verifiable using FLTL temporal logic. The main results of this work include (i) precise specification of interaction protocols depending on the type of middle-agent (this can also be a basis for characterizing types of middle-agents), (ii) improvement of communication between designers and developers and facilitation of formal verification of agent systems, (iii) guided design and implementation of agent-based software systems that incorporate middle-agents.
LA - eng
KW - multi-agent system; interaction protocol; process algebra; formal specification
UR - http://eudml.org/doc/208041
ER -

References

top
  1. Alagar, V. and Holliday, J. (2002). Agent types and their formal descriptions, Technical Report COEN-2002-09-19A, Santa Clara University, Santa Clara, CA. 
  2. Bergstra, J., Ponse, A. and Smolka, S. (2001). Handbook of Process Algebra, Elsevier Science, Amsterdam. Zbl0971.00006
  3. Brazier, F.M.T., Cornelissen, F., Gustavsson, R., Jonker, C.M., Lindeberg, O., Polak, B. and Treur, J. (2004). Compositional verification of a multi-agent system for one-to-many negotiation, Applied Intelligence 20(2): 95-117. Zbl1080.68684
  4. Bădică, A. and Bădică, C. (2008a). Conceptualizing interactions with matchmakers and front-agents using formal verification methods, in D. Dochev, M. Pistore and P. Traverso (Eds.), Proceedings of the 13th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA 2008), Lecture Notes in Artificial Intelligence, Vol. 5253, Springer-Verlag, Berlin, pp. 390-394. 
  5. Bădică, A. and Bădică, C. (2008b). Formal specification of matchmakers, front-agents, and brokers in agent environments using FSP, Proceedings of the 6th International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems (MSVVEIS 2008), Barcelona, Spain, pp. 9-18. Zbl1216.68184
  6. Bădică, A. and Bădică, C. (2008c). Formalizing agent-based english auctions using finite state process algebra, Journal of Universal Computer Science 14(7): 1118-1135. 
  7. Bădică, A. and Bădică, C. (2008d). Modeling interactions in agent-based English auctions with matchmaking capabilities, in C. Bădică, G. Mangioni, V. Carchiolo and D.D. Burdescu (Eds.), Intelligent Distributed Computing, Systems and Applications (IDC 2008), Studies in Computational Intelligence, Vol. 162, Springer-Verlag, Berlin, pp. 45-54. 
  8. Bădică, A. and Bădică, C. (2008e). Specification and verification of agent interactions in matchmaking processes using FSP and FLTL, Proceedings of the 23rd International Symposium on Computer and Information Sciences (ISCIS 2008), Istanbul, Turkey, pp. 1-6. Zbl1216.68184
  9. Bădică, A. and Bădică, C. (2009a). Formalizing agent interactions in matchmaking processes using FSP and FLTL, Scientific Bulletin of 'Politehnica' University of Timisoara, Transactions on Automatic Control and Computer Science 54(68)(1): 13-18. 
  10. Bădică, A. and Bădică, C. (2009b). Specification and verification of an agent-based auction service, in G.A. Papadopoulos, W. Wojtkowski, G. Wojtkowski, S. Wrycza, and J. Zupancic (Eds.) Information System Development. Towards a Service Provision Society (ISD 2008), Springer-Verlag, New York, NY, pp. 239-248. Zbl1216.68184
  11. Bădică, A., Bădică, C. and Liţoiu, L. (2003). Role activity diagrams as finite state processes, Proceedings of the 2nd International Symposium on Parallel and Distributed Computing (ISPDC 2003), Ljubljana, Slovenia, pp. 15-22. 
  12. Bădică, A., Bădică, C. and Liţoiu, L. (2007). Middle-agents interactions as finite state processes: Overview and example, Proceedings of the 16th IEEE International Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE 2007), Paris, France, pp. 12-17. 
  13. Bădică, A., Bădică, C., Popescu, E. and Scafes, M. (2009). A process algebraic framework for service coordination, Proceedings of the 5th International Symposium on Applied Computational Intelligence and Informatics (SACI 2009), Timişoara, Romania, pp. 515-520. 
  14. Bădică, C., Ganzha, M. and Paprzycki, M. (2007). Developing a model agent-based e-commerce system, in J. Lu, G. Zhang and D. Ruan (Eds.), E-Service Intelligence: Methodologies, Technologies and Applications, Studies in Computational Intelligence, Vol. 55, Springer-Verlag, Berlin, pp. 555-578. 
  15. Clarke, E.M., Emerson, E.A. and Sistla, A.P. (1986). Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems 8(2): 244-263. Zbl0591.68027
  16. Decker, K., Sycara, K.P. and Williamson, M. (1997). Middleagents for the internet, Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI'97), Nagoya, Aichi, Japan, Vol. 1, pp. 578-583. 
  17. D'Ippolito, N., Fischbein, D., Chechik, M. and Uchitel, S. (2008). MTSA: The modal transition system analyser, Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering, ASE'08, L'Aquila, Italy, pp. 475-476. 
  18. Dobriceanu, A., Bîscu, L., Bădică, A. and Bădică, C. (2009). The design and implementation of an agent-based auction service, International Journal of Agent Oriented Software Engineering 3(2/3): 188-211. 
  19. Dwyer, M.B., Avrunin, G.S. and Corbett, J.C. (1999). Patterns in property specifications for finite-state verification, Proceedings of the 21st International Conference on Software Engineering (ICSE 1999), Los Angeles, CA, USA, pp. 411-420. 
  20. Esterline, A., Rorie, T. and Homaifar, A. (2006). A processalgebraic agent abstraction, in C.A. Rouff, M. Hinchey, J. Rash, W. Truszkowski and D. Gordon-Spears (Eds.), Agent Technology from a Formal Perspective, NASA Monographs in Systems and Software Engineering, Springer-Verlag, London, pp. 88-137. 
  21. Fasli, M. (2007). Agent Technology for E-Commerce, John Wiley & Sons, Chichester. 
  22. Fokkink, W. (2007). Texts in Theoretical Computer Science, EATCS Series, Springer-Verlag, Berlin/Heidelberg. 
  23. Foster, H., Uchitel, S., Magee, J. and Kramer, J. (2006). LTSAWS: A tool for model-based verification of web service compositions and choreography, in L.J. Osterweil, H.D. Rombach and M.L. Soffa (Eds.), Proceedings of the 28th International Conference on Software Engineering (ICSE 2006), Shanghai, China, pp. 771-774. 
  24. Goh, S., Chhetri, M.B. and Kowalczyk, R. (2007). JADE-FSMengine: A deployment tool for flexible agent behaviours in JADE, Proceedings of the 2007 IEEE/WIC/ACM International Conference on Intelligent Agent Technology, IAT'2007, Silicon Valley, CA, USA, pp. 524-527. 
  25. Hennicker, R. and Ludwig, M. (2005). Property-driven development of a coordination model for distributed simulations, in M. Steffen and G. Zavattaro (Eds.), Formal Methods for Open Object-Based Distributed Systems, Lecture Notes in Computer Science, Vol. 3535, Springer, Berlin/Heidelberg, pp. 290-305. 
  26. Hoare, C.A.R. (1985). Communicating Sequential Processes, Prentice Hall International Series in Computer Science, Upper Saddle River, NJ. Zbl0637.68007
  27. Hristozova, M. and Sterling, L. (2003). Experiences with ontology development for value-added publishing, in S. Cranefield, T.W. Finin, V.A.M. Tamma and S. Willmott (Eds.), Proceedings of the International Workshop on Ontologies in Agent Systems (OAS 2003), CEUR Workshop Proceedings, Vol. 73, pp. 17-24. 
  28. Klusch, M. and Sycara, K.P. (2001). Brokering and matchmaking for coordination of agent societies: A survey, in A. Omicini, F. Zambonelli, M. Klusch and R. Tolksdorf (Eds.), Coordination of Internet Agents: Models, Technologies, and Applications, Springer, Berlin/Heidelberg/New York, NY, pp. 197-224. 
  29. Magee, J. and Kramer, J. (2006). Concurrency. State Models and Java Programs, 2nd Edn., John Wiley & Sons, Chichester. Zbl0924.68026
  30. Mbala, A., Padgham, L. and Winikoff, M. (2006). Design options for subscription managers, in G.A. Vouros and T. Panayiotopoulos (Eds.), Agent-Oriented Information Systems III, Lecture Notes in Computer Science, Vol. 3529, Springer, London, pp. 259-274. 
  31. Merayo, M., Núñez, M., and Rodríguez, I. (2007). Specification of multi-agent systems by using EUSMs, Proceedings of the International Symposium on Fundamentals of Software Engineering (FSEN'2007), Lecture Notes in Computer Science, Vol. 4767, Springer, Berlin/Heidelberg/New York, NY, pp. 318-333. Zbl1141.68478
  32. Miller, T. and McBurney, P. (2007). Using constraints and process algebra for specification of first-class agent interaction protocols, Engineering Societies in the Agents World VII (ESAW 2006), Lecture Notes in Computer Science, Vol. 4457, Springer, Berlin/Heidelberg/New York, NY, pp. 245-254. 
  33. Milner, R. (1999). Communicating and Mobile Systems: The π-Calculus, Cambridge University Press, Cambridge. Zbl0942.68002
  34. Podorozhny, R.M., Khurshid, S., Perry, D.E. and Zhang, X. (2007). Verification of multi-agent negotiations using the alloy analyzer, Proceedings of the 6th International Conference Integrated Formal Methods (IFM'2007), Lecture Notes in Computer Science, Vol. 4591, Springer, Berlin/Heidelberg/New York, NY, pp. 501-517. 
  35. Rahimi, S., Cobb, M., Ali, D. and Petry, F. (2002). A modeling tool for intelligent-agent based systems: Api-calculus, in V. Loia (Ed.), Soft Computing Agents: A New Perspective for Dynamic Systems, Frontiers in Artificial Intelligence and Applications, IOS Press, Amsterdam, pp. 165-186. 
  36. Rouff, C., Rash, J., Hinchey, M. and Truszkowski, W. (2006). Formal methods at NASA Goddard Space Flight Center, in C.A. Rouff, M. Hinchey, J. Rash, W. Truszkowski and D. Gordon-Spears (Eds.), Agent Technology from a Formal Perspective, NASA Monographs in Systems and Software Engineering, Springer-Verlag, London, pp. 287-309. 
  37. Wang, F. (2002). Self-organising communities formed by middle agents, Proceedings of the 1st International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS'02, Bologna, Italy, pp. 1333-1339. 
  38. Wong, H.C. and Sycara, K. (2000). A taxonomy of middleagents for the Internet, Proceedings of the 4th International Conference on MultiAgent Systems (ICMAS-2000), Boston, MA, USA, pp. 465-466. 
  39. Xu, D.-X., El-Ariss, O., Xu, W.-F. and Wang, L.-Z. (2009). Aspect-oriented modeling and verification with finite state machines, Journal of Computer Science and Technology 24(5): 949-961. 
  40. Yarom, I., Rosenschein, J.S. and Goldman, C.V. (2003). The role of middle-agents in electronic commerce, IEEE Intelligent Systems 18(6): 15-21. 
  41. Zhang, P., Muccini, H. and Li, B. (2010). A classification and comparison of model checking software architecture techniques, Journal of Systems and Software 83(5): 723-744. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.