Search
2015 Volume 30
Article Contents
RESEARCH ARTICLE   Open Access    

A roadmap to pervasive systems verification

More Information
  • Abstract: The complexity of pervasive systems arises from the many different aspects that such systems possess. A typical pervasive system may be autonomous, distributed, concurrent and context based, and may involve humans and robotic devices working together. If we wish to formally verify the behaviour of such systems, the formal methods for pervasive systems will surely also be complex. In this paper, we move towards being able to formally verify pervasive systems and outline our approach wherein we distinguish four distinct dimensions within pervasive system behaviour and utilize different, but appropriate, formal techniques for verifying each one.
  • 加载中
  • Arapinis M., Calder M., Dennis L. A., Fisher M., Gray P. D., Konur S., Miller A., Ritter E., Ryan M., Schewe S., Unsworth C. & Yasmin R.2009. Towards the verification of pervasive systems. ECEASST Electronic Communications of the EASST22, 1–15.

    Google Scholar

    Bakhouya M., Campbell R., Coronato A., de Pietro G. & Ranganathan A.2012. Introduction to special section on formal methods in pervasive computing. ACM Transactions on Autonomous and Adaptive Systems6(1–6), 9.

    Google Scholar

    Birkedal L., Bundgaard M., Damgaard T. C., Debois S., Elsborg E., Glenstrup A. J., Hildebr T., Milner R. & Niss H.2006. Bigraphical programming languages for pervasive computing. In Proceedings of the International Workshop on Combining Theory and Systems Building in Pervasive Computing, 653–658.

    Google Scholar

    Bordini R. H., Dastani M., Dix J. & El Fallah Seghrouchni A. (eds) 2005. Multi-Agent Programming: Languages, Platforms and Applications, Springer.

    Google Scholar

    Bordini R. H., Dastani M., Dix J. & El Fallah-Seghrouchni A. (eds) 2009. Multi-Agent Programming: Languages, Tools and Applications, Springer.

    Google Scholar

    Bordini R. H., Dennis L. A., Farwer B. & Fisher M.2008. Automated verification of multi-agent programs. In Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE), 69–78.

    Google Scholar

    Bordini R. H., Fisher M., Visser W. & Wooldridge M.2006. Verifying multi-agent programs by model checking. Journal of Autonomous Agents and Multi-Agent Systems12(2), 239–256.

    Google Scholar

    Bordini R. H., Hübner J. F. & Vieira R.2005. Jason and the Golden Fleece of agent-oriented programming, chapter 1. In Bordini, R. H., Dastani, M., Dix, J. & Seghrouchni, E. F (eds), 3–37.

    Google Scholar

    Boytsov A. & Zaslavsky A.2011. Formal Verification of the Context Model — Enhanced Context Spaces Theory Approach. Technical report, Department of Computer Science, Space and Electrical Engineering, SE-971 87, Lulea University of Technology.

    Google Scholar

    Chen H., Finin T. & Joshi A.2003. An ontology for context-aware pervasive computing environments. Knowledge Engineering Review. Special Issue on Ontologies for Distributed Systems, 18, 197–207.

    Google Scholar

    Clancey W., Sierhuis M., Kaskiris C. & van Hoof R.2003. Advantages of Brahms for specifying and implementing a multiagent human-robotic exploration system. In Proceedings of the Sixteenth International Florida Artificial Intelligence Research Society Conference (FLAIRS), 7–11. AAAI Press.

    Google Scholar

    Clarke E. M., Grumberg O. & Peled D. A.1999. Model Checking, MIT Press.

    Google Scholar

    Dastani M., van Riemsdijk M. B. & Meyer J.-J. C.2005. Programming multi-agent systems in 3APL, chapter 2. In Multi-Agent Programming, Bordini, R. H., Dastani, M., Dix, J. & Seghrouchni, E. F (eds), Springer, 39–67.

    Google Scholar

    Dennis L. A. & Farwer B.2008. Gwendolen: a BDI language for verifiable agents. In Proceedings of the AISB’08 Workshop on Logic and the Simulation of Interaction and Reasoning, Löwe, B. (ed.). AISB.

    Google Scholar

    Dennis L. A., Fisher M. & Hepple A.2008. Language constructs for multi-agent programming. In Proceedings of the 8th Workshop on Computational Logic in Multi-Agent Systems (CLIMA), LNAI 5056, 137–156. Springer.

    Google Scholar

    Dennis L. A., Fisher M., Webster M. & Bordini R. H.2012. Model checking agent programming languages. Automated Software Engineering19(1), 5–63.

    Google Scholar

    Dobson S., Denazis S., Fernández A., Gati D., Gelenbe E., Massacci F., Nixon P., Saffre F., Schmidt N. & Zambonelli F.2006. A survey of autonomic communications. ACM Transactions on Autonomous and Adaptive Systems1(2), 223–259.

    Google Scholar

    Dobson S., Sterritt R., Nixon P. & Hinchey M.2010. Fulfilling the vision of autonomic computing. IEEE Computer43(1), 35–41.

    Google Scholar

    Finger M. & Gabbay D. M.1996. Combining temporal logic systems. Notre Dame Journal of Formal Logic37(2), 204–232.

    Google Scholar

    Fisher M., Dennis L. & Webster M.2013. Verifying autonomous systems. Communications of the ACM56(9), 84–93.

    Google Scholar

    Fisher M. & Hepple A.2009. Executing logical agent specifications. In Multi-Agent Programming: Languages, Tools and Applications R. H. Bordini, M. Dastani, J. Dix & A. El Fallah-Seghrouchni (eds), 1–27Springer.

    Google Scholar

    Fisher M., Singh M., Spears D. & Wooldridge M.2007. Guest editorial: logic-based agent verification. Journal of Applied Logic5(2), 193–195.

    Google Scholar

    Gabbay D., Kurucz A., Wolter F. & Zakharyaschev M.2003. Many-Dimensional Modal Logics: Theory and Applications. Studies in Logic and the Foundations of Mathematics, 148Elsevier Science.

    Google Scholar

    Georgeff M. P. & Lansky A. L.1987. Reactive reasoning and planning. In Proceedings of the 6th National Conference on Artificial Intelligence (AAAI), 677–682. AAAI Press, .

    Google Scholar

    Gorrieri R., Herzog U. & Hillston J.2002. Unified specification and performance evaluation using stochastic process algebras. Performance Evaluation50(2/3), 79–82.

    Google Scholar

    Greenfield A.2006. Everyware, New Riders Publishing.

    Google Scholar

    Henricksen K. & Indulska J.2004. A software engineering framework for context-aware pervasive computing. In Proceedings 2nd IEEE Conference on Pervasive Computing and Communications, 77–86.

    Google Scholar

    Hepple A.2010. Agents, Context, and Logic. PhD thesis, Department of Computer Science, University of Liverpool.

    Google Scholar

    Hepple A., Dennis L. A. & Fisher M.2008. A common basis for agent organisations in BDI languages. In Proceedings of the International Workshop on Languages, Methodologies and Development Tools for Multi-Agent Systems (LADS), Lecture Notes in Artificial Intelligence 5118, 171–188. Springer-Verlag.

    Google Scholar

    Hindriks K., de Boer F., van der Hoek W. & Meyer J.-J.2001. Agent programming with declarative goals. In Intelligent Agents VII, Lecture Notes in Artificial Intelligence 1986, 228–243. Springer-Verlag.

    Google Scholar

    Holzmann G.2003. Spin Model Checker, The: Primer and Reference Manual, 1st edition. Addison-Wesley Professional.

    Google Scholar

    Hunter J., Raimondi F., Rungta N. & Stocker R.2013. A synergistic and extensible framework for multi-agent system verification. In Proceedings of International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS), 869–876. IFAAMAS.

    Google Scholar

    Isern D., Moreno A., Sanchez D., Hajnal A., Pedone G. & Varga L.2011. Agent-based execution of personalised home care treatments. Applied Intelligence34, 155–180.

    Google Scholar

    Jongmans S.-S. T. Q., Hindriks K. V. & van Riemsdijk M. B.2010. Model checking agent programs by using the program interpreter. In Proceedings of the 11th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA), LNCS 6245, 219–237. Springer.

    Google Scholar

    Knox S., Shannon R., Coyle L., Clear A., Dobson S., Quigley A. & Nixon P.2008. Scatterbox: context-aware message management. Revue dIntelligence Artificielle22(5), 549–568.

    Google Scholar

    Konur S.2013. A survey on temporal logics for specifying and verifying real-time systems. Frontiers of Computer Science7(3), 370–403.

    Google Scholar

    Konur S., Fisher M., Dobson S. & Knox S.2014. Formal verification of a pervasive messaging system. Formal Aspects of Computing26(4), 677–694.

    Google Scholar

    Konur S., Fisher M. & Schewe S.2013. Combined model checking for temporal, probabilistic, and real-time logics. Theoretical Computer Science503, 61–88.

    Google Scholar

    Kwiatkowska M., Norman G. & Parker D.2002. PRISM: probabilistic symbolic model checker, Lecture Notes in Computer Science 2324, 200–204. Springer.

    Google Scholar

    NASA (Astronaut-Robot-Team-Concept). NASA astronaut robot partner. http://history.nasa.gov/DPT/DPT.htm.

    Google Scholar

    PRISM2013. Probabilistic symbolic model checker. http://www.cs.bham.ac.uk/ dxp/prism.

    Google Scholar

    Ranganathan A. & Campbell R. H.2008. Provably correct pervasive computing environments. In IEEE International Conference on Pervasive Computing and Communications, 160–169.

    Google Scholar

    Rao A. S.1996. AgentSpeak(L): BDI agents speak out in a logical computable language. In Proceedings of the 7th European Workshop on Modelling Autonomous Agents in a Multi-Agent World, (MAAMAW), LNAI 1038, 748–752. Springer-Verlag.

    Google Scholar

    Rao A. S. & Georgeff M. P.1991. Modeling agents within a BDI-architecture. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (KR). Morgan Kaufmann.

    Google Scholar

    Rao A. S. & Georgeff M. P.1992. An abstract architecture for rational agents. In Proceedings of the International Conference on Knowledge Representation and Reasoning (KR), 439–449.

    Google Scholar

    Rao A. S. & Georgeff M. P.1995. BDI agents: from theory to practice. In Proceedings of the 1st International Conference on Multi-Agent Systems (ICMAS), 312–319. IEEE Press.

    Google Scholar

    RoboSafe2013. Trustworthy robotic assistants project. http://www.robosafe.org.

    Google Scholar

    Rosa P. M. P., Dias J. A., Lopes I. M. C., Rodrigues J. J. P. C. & Lin K.2012. An ubiquitous mobile multimedia system for events agenda. In WCNC, 2103–2107.

    Google Scholar

    Sierhuis M.2001. Modeling and Simulating Work Practice. BRAHMS: A Multiagent Modeling and Simulation Language for Work System Analysis and Design. PhD thesis, SIKS Dissertation Series No. 2001-10, Social Science and Informatics (SWI), University of Amsterdam.

    Google Scholar

    Sierhuis M.2006. Multiagent modeling and simulation in human-robot mission operations. http://ic.arc.nasa.gov/ic/publications).

    Google Scholar

    Sierhuis M., Bradshaw J. M., Acquisti A., Hoof R. V., Jeffers R. & Uszok A.2003. Human-agent teamwork and adjustable autonomy in practice. In Proceedings of the 7th International Symposium on Artificial Intelligence, Robotics and Automation in Space (i-SAIRAS).

    Google Scholar

    Sierhuis M. & Clancey W. J.2002. Modeling and simulating work practice: a human-centered method for work systems design. IEEE Intelligent Systems17(5), 32–41.

    Google Scholar

    Stocker R., Dennis L., Dixon C. & Fisher M.2012. Verifying Brahms human-robot teamwork models. In Proceedings of the 13th European Conference on Logics in Artificial Intelligence, JELIA’12, 385–397. Springer-Verlag.

    Google Scholar

    Stocker R., Sierhuis M., Dennis L., Dixon C. & Fisher M.2011. A formal semantics for Brahms. In Proceedings of the 12th International Conference on Computational Logic in Multi-Agent Systems, CLIMA’11, 259–274. Springer-Verlag.

    Google Scholar

    Strang T. & Popien C. L.2004. A context modeling survey. In Workshop on Advanced Context Modelling, Reasoning and Management, UbiComp 2004 – The Sixth International Conference on Ubiquitous Computing.

    Google Scholar

    Turner K. J.2012. Advances in Home Care Technologies: Results of the MATCH Project, IOS Press.

    Google Scholar

    van Hoof R.2000. Brahms website. http://www.agentisolutions.com.

    Google Scholar

    Visser W., Havelund K., Brat G. & Park S.2000. Model checking programs. In Proceedings of the 15th International Conference on Automated Software Engineering (ASE), 3–12. IEEE Computer Society.

    Google Scholar

    Want R., Pering T., Borriello G. & Farkas K.2002. Disappearing hardware. Pervasive Computing1(1), 36–47.

    Google Scholar

    Weiser M.1993. Some computer science issues in ubiquitous computing. Communications of the ACM36(7), 74–84.

    Google Scholar

    Wooldridge M.2002. An Introduction to Multiagent Systems, John Wiley & Sons.

    Google Scholar

  • Cite this article

    Savas Konur, Michael Fisher. 2015. A roadmap to pervasive systems verification. The Knowledge Engineering Review 30(3)324−341, doi: 10.1017/S0269888914000228
    Savas Konur, Michael Fisher. 2015. A roadmap to pervasive systems verification. The Knowledge Engineering Review 30(3)324−341, doi: 10.1017/S0269888914000228

Article Metrics

Article views(23) PDF downloads(14)

Other Articles By Authors

RESEARCH ARTICLE   Open Access    

A roadmap to pervasive systems verification

The Knowledge Engineering Review  30 2015, 30(3): 324−341  |  Cite this article

Abstract: Abstract: The complexity of pervasive systems arises from the many different aspects that such systems possess. A typical pervasive system may be autonomous, distributed, concurrent and context based, and may involve humans and robotic devices working together. If we wish to formally verify the behaviour of such systems, the formal methods for pervasive systems will surely also be complex. In this paper, we move towards being able to formally verify pervasive systems and outline our approach wherein we distinguish four distinct dimensions within pervasive system behaviour and utilize different, but appropriate, formal techniques for verifying each one.

    • The work described in this paper is partially supported in the United Kingdom by the following EPSRC projects: ‘Verifying Interoperability Requirements in Pervasive Systems’ (EP/F033567) and ‘ROADBLOCK’ (EP/I031812).

    • Our thanks to an anonymous reviewer for highlighting this.

    • © Cambridge University Press 2014 2014Cambridge University Press
References (61)
  • About this article
    Cite this article
    Savas Konur, Michael Fisher. 2015. A roadmap to pervasive systems verification. The Knowledge Engineering Review 30(3)324−341, doi: 10.1017/S0269888914000228
    Savas Konur, Michael Fisher. 2015. A roadmap to pervasive systems verification. The Knowledge Engineering Review 30(3)324−341, doi: 10.1017/S0269888914000228
  • Catalog

      /

      DownLoad:  Full-Size Img  PowerPoint
      Return
      Return