Assurance of agent systems: What role should formal verification play?

In this paper 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.Unpublished[1] N. Alechina, M. Dastani, B.S. Logan, and J.-J. Ch. Meyer. A logic of agent programs. In Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence (AAAI), pages 795–800, 2007. [2] N. Alechina, M. Dastani, B.S. Logan, and J.-J. Ch. Meyer. Reasoning about agent deliberation. In Gerhard Brewka and Jérôme Lang, editors, Proceedings, Eleventh International Conference on Principles of Knowledge Representation and Reasoning, pages 16–26, 2008. [3] Natasha Alechina, Mehdi Dastani, Brian Logan, and John-Jules Ch. Meyer. Reasoning about agent execution strategies (short paper). In Autonomous Agents and Multi-Agent Systems (AAMAS), pages 1455–1458, 2008. [4] Randall D. Beer. A dynamical systems perspective on agent-environment interaction. Artificial Intelligence, 72:173–215, 1995. [5] P. Bishop, R. Bloomfield, and S. Guerra. 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, pages 390–395, 2004. [6] Rafael H. Bordini, Louise A. Dennis, Berndt Farwer, and Michael Fisher. Automated verification of multi-agent programs. In 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE2008), pages 69–78, L’Aquila, Italy, September 2008. IEEE. [7] Rafael H. Bordini, Michael Fisher, Carmen Pardavila, and Michael Wooldridge. Model checking AgentSpeak. In Autonomous Agents and Multiagent Systems (AAMAS), pages 409–416, 2003. [8] Rafael H. Bordini, Michael Fisher, and Maarten Sierhuis. Analysing human-agent teamwork. In 10th ESA Workshop on Advanced Space Technologies for Robotics and Automation (ASTRA 2008), Noordwijk, The Netherlands., November 2008. [9] Rafael H. Bordini, Michael Fisher, Willem Visser, and Michael Wooldridge. State-space reduction techniques in agent verification. In Autonomous Agents and Multi-Agent Systems (AAMAS), pages 896–903, 2004. [10] Rafael H. Bordini, Michael Fisher, Willem Visser, and Michael Wooldridge. Verifying multi-agent programs by model checking. Journal of Autonomous Agents and Multi-Agent Systems (JAAMAS), 12:239–256, 2006. [11] Christopher Cheong and Michael Winikoff. Hermes: Designing flexible and robust agent interactions. In Virginia Dignum, editor, Multi-Agent Systems – Semantics and Dynamics of Organizational Models, chapter 5, pages 105–139. IGI, 2009. [12] Amit K. Chopra and Munindar P. Singh. An architecture for multiagent systems: An approach based on commitments. In Workshop on Programming Multiagent Systems (ProMAS), 2009. [13] Amit K. Chopra and Munindar P. Singh. Multiagent commitment alignment. In Autonomous Agents and Multi-Agent Systems (AAMAS), pages 937–944, 2009. [14] Judith Crow, Denis Javaux, and John Rushby. Models and mechanized methods that integrate human factors into automation design. In International Conference on Human-Computer Interaction in Aeronautics: HCI-Aero, sep 2000. [15] Paul Curzon, Rimvydas Rukšėnas, and Ann Blandford. An approach to formal verification of human–computer interaction. Formal Aspects of Computing, 19(4):513–550, 2007. [16] Josh Dehlinger and Joanne Bechta Dugan. 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), pages 429–434. IEEE Computer Society, 2008. [17] Greg Dennis, Kuat Yessenov, and Daniel Jackson. Bounded verification of voting software. In Second International Conference on Verified Software: Theories, Tools, Experiments, volume 5295 of LNCS, pages 130–145. Springer, 2008. [18] Louise A. Dennis, Berndt Farwer, Rafael H. Bordini, and Michael Fisher. A flexible framework for verifying agent programs. In Autonomous Agents and Multi-Agent Systems (AAMAS), pages 1303–1306. IFAAMAS, 2008. [19] Edsger W. Dijkstra. 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. [20] David L. Dill. What’s between simulation and formal verification? (extended abstract). In DAC ’98: Proceedings of the 35th annual conference on Design automation, pages 328–329, New York, NY, USA, 1998. ACM. [21] D.A. Duce and D.J. Duke. Syndetic modelling:: Computer science meets cognitive psychology. Electronic Notes in Theoretical Computer Science, 43:50 – 74, 2001. 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). [22] Simon Duff, James Harland, and John Thangarajah. On proactive and maintenance goals. In Autonomous Agents and Multi-Agent Systems (AAMAS), pages 1033–1040. ACM, 2006. [23] Matthew B. Dwyer, George S. Avrunin, and James C. Corbett. Patterns in property specifications for finite-state verification. In International Conference on Software Engineering (ICSE), pages 411–420, 1999. [24] Erdem Eser Ekinci, Ali Murat Tiryaki, and Övünç Çetin. Goal-oriented agent testing revisited. In Jorge J. Gomez-Sanz and Michael Luck, editors, Ninth International Workshop on Agent-Oriented Software Engineering (AOSE), pages 85–96, 2008. [25] Jonathan Ezekiel and Alessio Lomuscio. Combining fault injection and model checking to verify fault tolerance in multi-agent systems. In Autonomous Agents and Multi-Agent Systems (AAMAS), pages 113–120, 2009. [26] Jimin Gao, Mats Heimdahl, David Owen, and Tim Menzies. 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. [27] Jorge J. Gomez-Sanz, Juan Botía, Emilio Serrano, and Juan Pavón. Testing and debugging of MAS interactions with INGENIAS. In Jorge J. Gomez-Sanz and Michael Luck, editors, Ninth International Workshop on Agent-Oriented Software Engineering (AOSE), pages 133–144, 2008. [28] Kenwood H. Hall, Raymond J. Staron, and Pavel Vrba. Experience with holonic and agent-based control systems and their adoption by industry. In V. Mařík, R.W. Brennan, and M. Pěchouček, editors, HoloMAS 2005, volume 3593 of Lecture Notes in Artificial Intelligence (LNAI), pages 1–10, 2005. [29] Daniel Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press, 2006. [30] Daniel Jackson. A direct path to dependable software. CACM, 52(4):78–88, April 2009. [31] Cliff Jones. What can we do (technically) to get ‘the right specification’?, October 2005. IFIP TC2 Working Conference, VSTTE, ETH Zurich. [32] Cliff B. Jones, Ian J. Hayes, and Michael A. Jackson. Deriving specifications for systems that are connected to the physical world. In Cliff B. Jones, Zhiming Liu, and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems: Essays in Honour of Dines Bjørner and Zhou Chaochen on the Occassion of Their 70th Birthdays, volume 4700 of Lecture Notes in Computer Science, pages 364–390. Springer Verlag, 2007. [33] Edmund Kazmierczak, Philip Dart, Leon Sterling, and Michael Winikoff. Verifying requirements through mathematical modelling and animation. International Journal of Software Engineering and Knowledge Engineering, 10(2):251–273, 2000. [34] T. Kelly and R. Weaver. The goal structuring notation–a safety argument notation. In Proc. DSN Workshop on Assurance Cases: Best Practices, Possible Obstacles, and Future Opportunities, 2004. [35] Rob Kremer and Roberto Flores. Using a performative subsumption lattice to support commitment-based conversations. In Frank Dignum, Virginia Dignum, Sven Koenig, Sarit Kraus, Munindar P. Singh, and Michael Wooldridge, editors, Autonomous Agents and Multi-Agent Systems (AAMAS), pages 114–121. ACM Press, 2005. [36] M. Lowry, M. Boyd, and D. Kulkami. Towards a theory for integration of mathematical verification and empirical testing. In 13th IEEE International Conference on Automated Software Engineering, pages 322–331, 1998. [37] Donald MacKenzie. Knowing Machines: Essays on Technical Change. MIT Press, 1996. ISBN 0-262-13315-6. [38] Donald MacKenzie. Mechanizing Proof: Computing, Risk, and Trust. MIT Press, 2001. ISBN 0-262-13393-8. [39] Bruno Mermet, Gaële Simon, Bruno Zanuttini, and Arnaud Saval. Specifying and Verifying a MAS: The Robots on Mars Case Study. In Post Proceedings ProMAS’07, volume 4908 of Lecture Notes in Artificial Intelligence (LNAI), pages 172–189, 2008. Detailed model and proofs available at http://users.info.unicaen.fr/~zanutti/ data/articles/mssz07companion.pdf. [40] S. Munroe, T. Miller, R.A. Belecheanu, M. Pechoucek, P. McBurney, and M. Luck. Crossing the agent technology chasm: Experiences and challenges in commercial applications of agents. Knowledge Engineering Review, 21(4):345–392, 2006. [41] Cu D. Nguyen, Anna Perini, and Paolo Tonella. Experimental evaluation of ontology-based test generation for multi-agent systems. In Jorge J. Gomez-Sanz and Michael Luck, editors, Ninth International Workshop on Agent-Oriented Software Engineering (AOSE), pages 165–176, 2008. [42] Cu D. Nguyen, Anna Perini, Paolo Tonella, Simon Miles, Mark Harman, and Michael Luck. Evolutionary testing of autonomous software agents. In Autonomous Agents and Multi-Agent Systems (AAMAS), pages 521–528, 2009. [43] David Owen and Tim Menzies. Lurch: a lightweight alternative to model checking. In Software Engineering and Knowledge Engineering (SEKE), pages 158–165, 2003. [44] David R. Owen. Combining Complementary Formal Verification Strategies to Improve Performance and Accuracy. PhD thesis, West Virginia University, Lane Department of Computer Science and Electrical Engineering, 2007. [45] Vaughan Pratt. Semantical considerations on floyd-hoare logic. In Proc. 17th Annual IEEE Symposium on Foundations of Computer Science, pages 109–121. IEEE Computer Society, 1976. [46] Michal Pěchouček and Vladimír Mařík. Industrial deployment of multi-agent technologies: review and selected case studies. Journal of Autonomous Agents and Multi-Agent Systems, 17:397–431, 2008. [47] Franco Raimondi and Alessio Lomuscio. Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams. J. Applied Logic, 5(2):235–251, 2007. [48] Anand S. Rao. AgentSpeak(L): BDI agents speak out in a logical computable language. In Walter Van de Velde and John Perrame, editors, Agents Breaking Away: Proceedings of the Seventh European Workshop on Modelling Autonomous Agents in a Multi-Agent World (MAAMAW’96), pages 42–55. Springer Verlag, LNAI 1038, 1996. [49] Greg Reeve and Steve Reeves. Experiences using Z animation tools. Number Working Paper 01/3. Department of Computer Science, University of Waikato, May 2001. [50] D. J. Richardson and L. A. Clarke. Partition analysis: A method combining testing and verification. IEEE Transactions on Software Engineering, 11(12):1477–1490, dec 1985. [51] John Rushby. Analyzing cockpit interfaces using formal methods. In H. Bowman, editor, Proceedings of FM-Elsewhere, volume 43 of Electronic Notes in Theoretical Computer Science, pages 1–14, Pisa, Italy, oct 2000. Elsevier. 10.1016/S1571-0661(04)80891-0. [52] John Rushby. Using model checking to help discover mode confusions and other automation surprises. Reliability Engineering & System Safety, 75(2):167 – 177, 2002. [53] John Rushby. A safety-case approach for certifying adaptive systems. In AIAA Infotech@Aerospace Conference, apr 2009. [54] Stuart Russell and Peter Norvig. Artificial Intelligence: A Modern Approach. Prentice Hall, 1995. [55] Nathan Schurr, Janusz Marecki, John P. Lewis, Milind Tambe, and Paul Scerri. The defacto system: Coordinating human-agent teams for the future of disaster response. In Rafael H. Bordini, Mehdi Dastani, Jürgen Dix, and Amal El Fallah-Seghrouchni, editors, Multi-Agent Programming: Languages, Platforms and Applications, volume 15 of Multiagent Systems, Artificial Societies, and Simulated Organizations, pages 197–215. Springer, 2005. [56] S. Shapiro, Y. Lespérance, and H.J. Levesque. 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: part 1, pages 19–26. ACM New York, NY, USA, 2002. [57] Wei-Tek Tsai, Rama Vishnuvajjala, and Du Zhang. Verification and validation of knowledge-based systems. IEEE Transactions on Knowledge and Data Engineering, 11(1):202–212, 1999. [58] Michael Winikoff. Implementing flexible and robust agent interactions using distributed commitment machines. Multiagent and Grid Systems, 2(4):365–381, 2006. [59] Michael Winikoff. Implementing commitment-based interactions. In Autonomous Agents and Multi-Agent Systems (AAMAS), pages 873–880, 2007. [60] Michael Winikoff and Stephen Cranefield. 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. [61] Michael Wooldridge, Michael Fisher, Marc-Philippe Huget, and Simon Parsons. Model checking multi-agent systems with MABLE. In Autonomous Agents and Multi-Agent Systems (AAMAS), pages 952–959, 2002. [62] Pınar Yolum and Munindar P. Singh. 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), pages 527–534, 2002. [63] M. Young and R.N. Taylor. Rethinking the taxonomy of fault detection techniques. In 11th International Conference on Software Engineering, pages 52–63, 1989. [64] Zhiyong Zhang, John Thangarajah, and Lin Padgham. Automated unit testing for agent systems. In Second International Working Conference on Evaluation of Novel Approaches to Software Engineering (ENASE), pages 10–18, 2007. [65] Zhi Quan Zhou, D.H. Huang, T.H. Tse, Zongyuan Yang, Haitao Huang, and T.Y. Chen. 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-12