Advertisement

Assurance of Agent Systems: What Role Should Formal Verification Play?

Chapter

Abstract

In this chapter we consider the broader issue of gaining assurance that an agent system will behave appropriately when it is deployed. We ask to what extent this problem is addressed by existing research into formal verification. We identify a range of issues with existing work which leads us to conclude that, broadly speaking, verification approaches on their own are too narrowly focussed. We argue that a shift in direction is needed, and outline some possibilities for such a shift in direction.

Keywords

Model Check Agent System Abstract Model Agent Program Generate Test Case 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Notes

Acknowledgements

I would like to thank Stephen Cranefield for discussions relating to this work, and for comments on a draft of this chapter. I would also like to thank the anonymous reviewers for their comments which were helpful in improving this paper.

References

  1. 349.
    Pěchouček, M., Mařík, V.: Industrial deployment of multi-agent technologies: review and selected case studies. Journal of Autonomous Agents and Multi-Agent Systems 17, 397–431 (2008). DOI 10.1007/s10458-008-9050-0CrossRefGoogle Scholar
  2. 148.
    Dill, D.L.: What’s between simulation and formal verification? (extended abstract). In: DAC ’98: Proceedings of the 35th annual conference on Design automation, pp. 328–329. ACM, New York, NY, USA (1998). DOI 10.1145/277044.277138Google Scholar
  3. 249.
    Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press (2006)Google Scholar
  4. 140.
    Dennis, L.A., Farwer, B., Bordini, R.H., Fisher, M.: A flexible framework for verifying agent programs. In: Autonomous Agents and Multi-Agent Systems (AAMAS), pp. 1303–1306. IFAAMAS (2008)Google Scholar
  5. 448.
    Zhou, Z.Q., Huang, D., Tse, T., Yang, Z., Huang, H., Chen, T.: Metamorphic testing and its applications. In: Proceedings of the 8th International Symposium on Future Software Technology (ISFST 2004) (2004). Published as Hong Kong University (HKU) Computer Science (CS) Technical Report TR-2004-12Google Scholar
  6. 369.
    Richardson, D.J., Clarke, L.A.: Partition analysis: A method combining testing and verification. IEEE Transactions on Software Engineering 11(12), 1477–1490 (1985). DOI 10.1109/TSE.1985.231892CrossRefGoogle Scholar
  7. 347.
    Pratt, V.: Semantical considerations on Floyd-Hoare logic. In: Proc. of the 17th IEEE Symp. on Foundations of Computer Science, pp. 109–121 (1976)Google Scholar
  8. 273.
    Kremer, R., Flores, R.: Using a performative subsumption lattice to support commitment-based conversations. In: F. Dignum, V. Dignum, S. Koenig, S. Kraus, M.P. Singh, M. Wooldridge (eds.) Autonomous Agents and Multi-Agent Systems (AAMAS), pp. 114–121. ACM Press (2005)Google Scholar
  9. 443.
    Yolum, P., Singh, M.P.: Flexible protocol specification and execution: Applying event calculus planning using commitments. In: Proceedings of the 1st Joint Conference on Autonomous Agents and MultiAgent Systems (AAMAS), pp. 527–534 (2002)Google Scholar
  10. 151.
    Duce, D., Duke, D.: Syndetic modelling:: Computer science meets cognitive psychology. Electronic Notes in Theoretical Computer Science 43, 50 – 74 (2001). DOI 10.1016/S1571-0661(04)80894-6. Formal Methods Elsewhere (a Satellite Workshop of FORTE-PSTV-2000 devoted to applications of formal methods to areas other than communication protocols and software engineering)CrossRefGoogle Scholar
  11. 29.
    Beer, R.D.: A dynamical systems perspective on agent-environment interaction. Artificial Intelligence 72, 173–215 (1995)CrossRefGoogle Scholar
  12. 97.
    Chopra, A.K., Singh, M.P.: Multiagent commitment alignment. In: Autonomous Agents and Multi-Agent Systems (AAMAS), pp. 937–944 (2009)Google Scholar
  13. 69.
    Bordini, R.H., Fisher, M., Sierhuis, M.: Analysing human-agent teamwork. In: 10th ESA Workshop on Advanced Space Technologies for Robotics and Automation (ASTRA 2008). Noordwijk, The Netherlands. (2008)Google Scholar
  14. 447.
    Zhang, Z., Thangarajah, J., Padgham, L.: Automated unit testing for agent systems. In: Second International Working Conference on Evaluation of Novel Approaches to Software Engineering (ENASE), pp. 10–18 (2007)Google Scholar
  15. 378.
    Rushby, J.: A safety-case approach for certifying adaptive systems. In: AIAA Infotech@Aerospace Conference (2009)Google Scholar
  16. 377.
    Rushby, J.: Using model checking to help discover mode confusions and other automation surprises. Reliability Engineering & System Safety 75(2), 167 – 177 (2002). DOI 10.1016/S0951-8320(01)00092-8CrossRefGoogle Scholar
  17. 72.
    Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: State-Space Reduction Techniques in Agent Verification. In: Proceedings of the 3rd International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), pp. 896–903. IEEE Computer Society (2004)Google Scholar
  18. 118.
    Crow, J., Javaux, D., Rushby, J.: Models and mechanized methods that integrate human factors into automation design. In: International Conference on Human-Computer Interaction in Aeronautics: HCI-Aero (2000)Google Scholar
  19. 95.
    Cheong, C., Winikoff, M.: Hermes: Designing flexible and robust agent interactions. In: V. Dignum (ed.) Multi-Agent Systems – Semantics and Dynamics of Organizational Models, chap. 5, pp. 105–139. IGI (2009)Google Scholar
  20. 250.
    Jackson, D.: A direct path to dependable software. CACM 52(4), 78–88 (2009). DOI 10.1145/1498765.1498787Google Scholar
  21. 269.
    Kazmierczak, E., Dart, P., Sterling, L., Winikoff, M.: Verifying requirements through mathematical modelling and animation. International Journal of Software Engineering and Knowledge Engineering 10(2), 251–273 (2000)CrossRefGoogle Scholar
  22. 187.
    Gao, J., Heimdahl, M., Owen, D., Menzies, T.: On the distribution of property violations in formal models: An initial study. In: Proceedings of the 30th Annual International Computer Software and Applications Conference (COMPSAC’06). IEEE Computer Society (2006)Google Scholar
  23. 357.
    Rao, A.S.: AgentSpeak(L): BDI agents speak out in a logical computable language. In: W.V. de Velde, J. Perrame (eds.) Agents Breaking Away: Proceedings of the Seventh European Workshop on Modelling Autonomous Agents in a Multi-Agent World (MAAMAW’96), pp. 42–55. Springer Verlag, LNAI 1038 (1996)Google Scholar
  24. 292.
    Lowry, M., Boyd, M., Kulkami, D.: Towards a theory for integration of mathematical verification and empirical testing. In: 13th IEEE International Conference on Automated Software Engineering, pp. 322–331 (1998). 10.1109/ASE.1998.732690Google Scholar
  25. 434.
    Winikoff, M.: Implementing flexible and robust agent interactions using distributed commitment machines. Multiagent and Grid Systems 2(4), 365–381 (2006)Google Scholar
  26. 96.
    Chopra, A.K., Singh, M.P.: An architecture for multiagent systems: An approach based on commitments. In: Workshop on Programming Multiagent Systems (ProMAS) (2009)Google Scholar
  27. 152.
    Duff, S., Harland, J., Thangarajah, J.: On Proactivity and Maintenance Goals. In: Proceedings of the fifth international joint conference on autonomous agents and multiagent systems (AAMAS’06), pp. 1033–1040. Hakodate (2006)Google Scholar
  28. 295.
    MacKenzie, D.: Mechanizing Proof: Computing, Risk, and Trust. MIT Press (2001). ISBN 0-262-13393-8Google Scholar
  29. 136.
    Dehlinger, J., Dugan, J.B.: Dynamic Event/Fault Tree Analysis of Multi-Agent Systems using Galileo. In: Integration of Software Engineering and Agent Technology (ISEAT), published as part of the Eighth International Conference on Quality Software (QSIC), pp. 429–434. IEEE Computer Society (2008). DOI 10.1109/QSIC.2008.14Google Scholar
  30. 419.
    Tsai, W.T., Vishnuvajjala, R., Zhang, D.: Verification and validation of knowledge-based systems. IEEE Transactions on Knowledge and Data Engineering 11(1), 202–212 (1999). DOI 10.1109/69.755629CrossRefGoogle Scholar
  31. 153.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: International Conference on Software Engineering (ICSE), pp. 411–420 (1999)Google Scholar
  32. 73.
    Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying Multi-Agent Programs by Model Checking. Journal of Autonomous Agents and Multi-Agent Systems 12(2), 239–256 (2006)CrossRefGoogle Scholar
  33. 312.
    Mermet, B., Simon, G., Zanuttini, B., Saval, A.: Specifying and Verifying a MAS: The Robots on Mars Case Study. In: Post Proceedings ProMAS’07, Lecture Notes in Artificial Intelligence (LNAI), vol. 4908, pp. 172–189 (2008). Detailed model and proofs available at http://users.info.unicaen.fr/zanutti/data/articles/mssz07companion.pdf
  34. 323.
    Nguyen, C.D., Perini, A., Tonella, P., Miles, S., Harman, M., Luck, M.: Evolutionary testing of autonomous software agents. In: Autonomous Agents and Multi-Agent Systems (AAMAS), pp. 521–528 (2009)Google Scholar
  35. 355.
    Raimondi, F., Lomuscio, A.: Automatic Verification of Multi-agent Systems by Model Checking via Ordered Binary Decision Diagrams. Journal of Applied Logic 5(2), 235–251 (2007)MATHCrossRefMathSciNetGoogle Scholar
  36. 395.
    Shapiro, S., Lespérance, Y., Levesque, H.J.: The cognitive agents specification language and verification environment for multiagent systems. In: Proceedings of the first international joint conference on autonomous agents and multiagent systems (AAMAS’02), pp. 19–26 (2002)Google Scholar
  37. 436.
    Winikoff, M., Cranefield, S.: On the testability of BDI agent systems. Information Science Discussion Paper Series 2008/03, University of Otago, Dunedin, New Zealand (2008). http://www.business.otago.ac.nz/infosci/pubs/papers/dpsall.htm
  38. 261.
    Jones, C.: What can we do (technically) to get ‘the right specification’? (2005). IFIP TC2 Working Conference, VSTTE, ETH ZurichGoogle Scholar
  39. 363.
    Reeve, G., Reeves, S.: Experiences using Z animation tools. Working Paper 01/3. Department of Computer Science, University of Waikato (2001). http://www.cs.waikato.ac.nz/pubs/wp/2001/
  40. 379.
    Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach. Prentice Hall (1995)Google Scholar
  41. 138.
    Dennis, G., Yessenov, K., Jackson, D.: Bounded verification of voting software. In: Second International Conference on Verified Software: Theories, Tools, Experiments, LNCS, vol. 5295, pp. 130–145. Springer (2008)Google Scholar
  42. 67.
    Bordini, R.H., Dennis, L.A., Farwer, B., Fisher, M.: Automated Verification of Multi-Agent Programs. In: Proc. 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 69–78 (2008)Google Scholar
  43. 322.
    Nguyen, C.D., Perini, A., Tonella, P.: Experimental evaluation of ontology-based test generation for multi-agent systems. In: J.J. Gomez-Sanz, M. Luck (eds.) Ninth International Workshop on Agent-Oriented Software Engineering (AOSE), pp. 165–176 (2008)Google Scholar
  44. 294.
    MacKenzie, D.: Knowing Machines: Essays on Technical Change. MIT Press (1996). ISBN 0-262-13315-6Google Scholar
  45. 147.
    Dijkstra, E.W.: EWD611: On the fact that the Atlantic Ocean has two sides. http://www.cs.utexas.edu/users/EWD/index06xx.html, originally published as pages 268–276 of Selected Writings on Computing: A Personal Perspective, Springer-Verlag. ISBN 0–387–90652–5. (1982)
  46. 157.
    Ekinci, E.E., Tiryaki, A.M., Çetin, Ö.: Goal-oriented agent testing revisited. In: J.J. Gomez-Sanz, M. Luck (eds.) Ninth International Workshop on Agent-Oriented Software Engineering (AOSE), pp. 85–96 (2008)Google Scholar
  47. 46.
    Bishop, P., Bloomfield, R., Guerra, S.: The future of goal-based assurance cases. In: Proceedings of Workshop on Assurance Cases. Supplemental Volume of the 2004 International Conference on Dependable Systems and Networks, pp. 390–395 (2004)Google Scholar
  48. 376.
    Rushby, J.: Analyzing cockpit interfaces using formal methods. In: H. Bowman (ed.) Proceedings of FM-Elsewhere, Electronic Notes in Theoretical Computer Science, vol. 43, pp. 1–14. Elsevier, Pisa, Italy (2000). 10.1016/S1571-0661(04)80891-0Google Scholar
  49. 199.
    Gomez-Sanz, J.J., Botía, J., Serrano, E., Pavón, J.: Testing and debugging of MAS interactions with INGENIAS. In: J.J. Gomez-Sanz, M. Luck (eds.) Ninth International Workshop on Agent-Oriented Software Engineering (AOSE), pp. 133–144 (2008)Google Scholar
  50. 435.
    Winikoff, M.: Implementing Commitment-Based Interactions. In: Proc. 6th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), pp. 1–8. ACM, New York, NY, USA (2007)Google Scholar
  51. 329.
    Owen, D., Menzies, T.: Lurch: a lightweight alternative to model checking. In: Software Engineering and Knowledge Engineering (SEKE), pp. 158–165 (2003)Google Scholar
  52. 119.
    Curzon, P., Rukšėnas, R., Blandford, A.: An approach to formal verification of human–computer interaction. Formal Aspects of Computing 19(4), 513–550 (2007). DOI 10.1007/s00165-007-0035-6MATHCrossRefGoogle Scholar
  53. 330.
    Owen, D.R.: Combining complementary formal verification strategies to improve performance and accuracy. Ph.D. thesis, West Virginia University, Lane Department of Computer Science and Electrical Engineering (2007)Google Scholar
  54. 68.
    Bordini, R.H., Fisher, M., Pardavila, C., Wooldridge, M.: Model checking AgentSpeak. In: Autonomous Agents and Multiagent Systems (AAMAS), pp. 409–416 (2003)Google Scholar
  55. 204.
    Hall, K.H., Staron, R.J., Vrba, P.: Experience with holonic and agent-based control systems and their adoption by industry. In: V. Mařík, R. Brennan, M. Pěchouček (eds.) HoloMAS 2005, Lecture Notes in Artificial Intelligence (LNAI), vol. 3593, pp. 1–10 (2005)Google Scholar
  56. 262.
    Jones, C.B., Hayes, I.J., Jackson, M.A.: Deriving specifications for systems that are connected to the physical world. In: C.B. Jones, Z. Liu, J. Woodcock (eds.) Formal Methods and Hybrid Real-Time Systems: Essays in Honour of Dines Bjørner and Zhou Chaochen on the Occassion of Their 70th Birthdays, Lecture Notes in Computer Science, vol. 4700, pp. 364–390. Springer Verlag (2007). DOI 10.1007/978-3-540-75221-9_16Google Scholar
  57. 168.
    Ezekiel, J., Lomuscio, A.: Combining fault injection and model checking to verify fault tolerance in multi-agent systems. In: Autonomous Agents and Multi-Agent Systems (AAMAS), pp. 113–120 (2009)Google Scholar
  58. 389.
    Schurr, N., Marecki, J., Lewis, J.P., Tambe, M., Scerri, P.: The defacto system: Coordinating human-agent teams for the future of disaster response. In: R.H. Bordini, M. Dastani, J. Dix, A.E. Fallah-Seghrouchni (eds.) Multi-Agent Programming: Languages, Platforms and Applications, Multiagent Systems, Artificial Societies, and Simulated Organizations, vol. 15, pp. 197–215. Springer (2005)Google Scholar
  59. 441.
    Wooldridge, M., Fisher, M., Huget, M.P., Parsons, S.: Model checking multi-agent systems with MABLE. In: Autonomous Agents and Multi-Agent Systems (AAMAS), pp. 952–959 (2002). DOI 10.1145/544862.544965Google Scholar
  60. 270.
    Kelly, T., Weaver, R.: The goal structuring notation–a safety argument notation. In: Proc. DSN Workshop on Assurance Cases: Best Practices, Possible Obstacles, and Future Opportunities (2004)Google Scholar
  61. 444.
    Young, M., Taylor, R.: Rethinking the taxonomy of fault detection techniques. In: 11th International Conference on Software Engineering, pp. 52–63 (1989)Google Scholar

Copyright information

© Springer Science+Business Media, LLC 2010

Authors and Affiliations

  1. 1.University of OtagoDunedinNew Zealand

Personalised recommendations