{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T18:27:45Z","timestamp":1767637665415,"version":"3.48.0"},"reference-count":61,"publisher":"Maximum Academic Press","issue":"3","license":[{"start":{"date-parts":[[2014,11,13]],"date-time":"2014-11-13T00:00:00Z","timestamp":1415836800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Knowledge Engineering Review"],"published-print":{"date-parts":[[2015,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    The complexity of\n                    <jats:italic>pervasive systems<\/jats:italic>\n                    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.\n                  <\/jats:p>","DOI":"10.1017\/s0269888914000228","type":"journal-article","created":{"date-parts":[[2014,11,13]],"date-time":"2014-11-13T04:54:12Z","timestamp":1415854452000},"page":"324-341","source":"Crossref","is-referenced-by-count":5,"title":["A roadmap to pervasive systems verification"],"prefix":"10.48130","volume":"30","author":[{"given":"Savas","family":"Konur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"27968","published-online":{"date-parts":[[2014,11,13]]},"reference":[{"volume-title":"An Introduction to Multiagent Systems","year":"2002","author":"Wooldridge","key":"S0269888914000228_ref61"},{"key":"S0269888914000228_ref60","doi-asserted-by":"publisher","DOI":"10.1145\/159544.159617"},{"key":"S0269888914000228_ref59","doi-asserted-by":"publisher","DOI":"10.1109\/MPRV.2002.993143"},{"key":"S0269888914000228_ref58","doi-asserted-by":"crossref","unstructured":"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\u201312. IEEE Computer Society.","DOI":"10.1109\/ASE.2000.873645"},{"key":"S0269888914000228_ref57","unstructured":"van Hoof R. 2000. Brahms website. http:\/\/www.agentisolutions.com."},{"volume-title":"Advances in Home Care Technologies: Results of the MATCH Project","year":"2012","author":"Turner","key":"S0269888914000228_ref56"},{"key":"S0269888914000228_ref53","doi-asserted-by":"crossref","unstructured":"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\u201912, 385\u2013397. Springer-Verlag.","DOI":"10.1007\/978-3-642-33353-8_30"},{"key":"S0269888914000228_ref52","doi-asserted-by":"publisher","DOI":"10.1109\/MIS.2002.1039830"},{"key":"S0269888914000228_ref51","unstructured":"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)."},{"key":"S0269888914000228_ref50","unstructured":"Sierhuis M. 2006. Multiagent modeling and simulation in human-robot mission operations. http:\/\/ic.arc.nasa.gov\/ic\/publications)."},{"key":"S0269888914000228_ref47","unstructured":"RoboSafe 2013. Trustworthy robotic assistants project. http:\/\/www.robosafe.org."},{"key":"S0269888914000228_ref46","unstructured":"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\u2013319. IEEE Press."},{"key":"S0269888914000228_ref45","unstructured":"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\u2013449."},{"key":"S0269888914000228_ref42","doi-asserted-by":"crossref","unstructured":"Ranganathan A. & Campbell R. H. 2008. Provably correct pervasive computing environments. In IEEE International Conference on Pervasive Computing and Communications, 160\u2013169.","DOI":"10.1109\/PERCOM.2008.116"},{"key":"S0269888914000228_ref41","unstructured":"PRISM 2013. Probabilistic symbolic model checker. http:\/\/www.cs.bham.ac.uk\/ dxp\/prism."},{"key":"S0269888914000228_ref40","unstructured":"NASA (Astronaut-Robot-Team-Concept). NASA astronaut robot partner. http:\/\/history.nasa.gov\/DPT\/DPT.htm."},{"key":"S0269888914000228_ref39","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M. , Norman G. & Parker D. 2002. PRISM: probabilistic symbolic model checker, Lecture Notes in Computer Science 2324, 200\u2013204. Springer.","DOI":"10.1007\/3-540-46029-2_13"},{"key":"S0269888914000228_ref35","doi-asserted-by":"publisher","DOI":"10.3166\/ria.22.549-568"},{"key":"S0269888914000228_ref34","doi-asserted-by":"crossref","unstructured":"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\u2013237. Springer.","DOI":"10.1007\/978-3-642-14977-1_17"},{"key":"S0269888914000228_ref32","unstructured":"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\u2013876. IFAAMAS."},{"volume-title":"Spin Model Checker, The: Primer and Reference Manual","year":"2003","author":"Holzmann","key":"S0269888914000228_ref31"},{"key":"S0269888914000228_ref28","unstructured":"Hepple A. 2010. Agents, Context, and Logic. PhD thesis, Department of Computer Science, University of Liverpool."},{"key":"S0269888914000228_ref27","doi-asserted-by":"crossref","unstructured":"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\u201386.","DOI":"10.1109\/PERCOM.2004.1276847"},{"volume-title":"Everyware","year":"2006","author":"Greenfield","key":"S0269888914000228_ref26"},{"key":"S0269888914000228_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-5316(02)00100-1"},{"volume-title":"Many-Dimensional Modal Logics: Theory and Applications","year":"2003","author":"Gabbay","key":"S0269888914000228_ref23"},{"key":"S0269888914000228_ref21","first-page":"1","volume-title":"Multi-Agent Programming: Languages, Tools and Applications","author":"Fisher","year":"2009"},{"key":"S0269888914000228_ref19","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1305\/ndjfl\/1040046087","article-title":"Combining temporal logic systems","volume":"37","author":"Finger","year":"1996","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"S0269888914000228_ref18","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2010.14"},{"key":"S0269888914000228_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1186778.1186782"},{"key":"S0269888914000228_ref43","unstructured":"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\u2013752. Springer-Verlag."},{"key":"S0269888914000228_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2500468.2494558"},{"key":"S0269888914000228_ref55","unstructured":"Strang T. & Popien C. L. 2004. A context modeling survey. In Workshop on Advanced Context Modelling, Reasoning and Management, UbiComp 2004 \u2013 The Sixth International Conference on Ubiquitous Computing."},{"key":"S0269888914000228_ref48","doi-asserted-by":"crossref","unstructured":"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\u20132107.","DOI":"10.1109\/WCNC.2012.6214139"},{"key":"S0269888914000228_ref54","doi-asserted-by":"crossref","unstructured":"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\u201911, 259\u2013274. Springer-Verlag.","DOI":"10.1007\/978-3-642-22359-4_18"},{"key":"S0269888914000228_ref49","unstructured":"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."},{"key":"S0269888914000228_ref2","first-page":"9","article-title":"Introduction to special section on formal methods in pervasive computing","volume":"6","author":"Bakhouya","year":"2012","journal-title":"ACM Transactions on Autonomous and Adaptive Systems"},{"volume-title":"Multi-Agent Programming: Languages, Tools and Applications","year":"2009","author":"Bordini","key":"S0269888914000228_ref5"},{"key":"S0269888914000228_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/s11704-013-2195-2"},{"key":"S0269888914000228_ref29","doi-asserted-by":"crossref","unstructured":"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\u2013188. Springer-Verlag.","DOI":"10.1007\/978-3-540-85058-8_5"},{"key":"S0269888914000228_ref10","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888904000025"},{"key":"S0269888914000228_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/b137449"},{"key":"S0269888914000228_ref6","doi-asserted-by":"crossref","unstructured":"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\u201378.","DOI":"10.1109\/ASE.2008.17"},{"key":"S0269888914000228_ref24","unstructured":"Georgeff M. P. & Lansky A. L. 1987. Reactive reasoning and planning. In Proceedings of the 6th National Conference on Artificial Intelligence (AAAI), 677\u2013682. AAAI Press, ."},{"key":"S0269888914000228_ref38","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2013.07.012"},{"key":"S0269888914000228_ref14","unstructured":"Dennis L. A. & Farwer B. 2008. Gwendolen: a BDI language for verifiable agents. In Proceedings of the AISB\u201908 Workshop on Logic and the Simulation of Interaction and Reasoning, L\u00f6we, B. (ed.). AISB."},{"key":"S0269888914000228_ref44","unstructured":"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."},{"key":"S0269888914000228_ref1","first-page":"1","article-title":"Towards the verification of pervasive systems","volume":"22","author":"Arapinis","year":"2009","journal-title":"ECEASST Electronic Communications of the EASST"},{"volume-title":"Model Checking","year":"1999","author":"Clarke","key":"S0269888914000228_ref12"},{"key":"S0269888914000228_ref8","doi-asserted-by":"crossref","unstructured":"Bordini R. H. , H\u00fcbner 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\u201337.","DOI":"10.1007\/0-387-26350-0_1"},{"key":"S0269888914000228_ref30","doi-asserted-by":"crossref","unstructured":"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\u2013243. Springer-Verlag.","DOI":"10.1007\/3-540-44631-1_16"},{"key":"S0269888914000228_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-013-0277-4"},{"key":"S0269888914000228_ref15","doi-asserted-by":"crossref","unstructured":"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\u2013156. Springer.","DOI":"10.1007\/978-3-540-88833-8_8"},{"key":"S0269888914000228_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-006-5955-7"},{"key":"S0269888914000228_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2005.12.012"},{"key":"S0269888914000228_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-011-0088-x"},{"key":"S0269888914000228_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s10489-009-0187-6"},{"key":"S0269888914000228_ref13","doi-asserted-by":"crossref","unstructured":"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\u201367.","DOI":"10.1007\/0-387-26350-0_2"},{"key":"S0269888914000228_ref3","unstructured":"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\u2013658."},{"key":"S0269888914000228_ref9","unstructured":"Boytsov A. & Zaslavsky A. 2011. Formal Verification of the Context Model \u2014 Enhanced Context Spaces Theory Approach. Technical report, Department of Computer Science, Space and Electrical Engineering, SE-971 87, Lulea University of Technology."},{"key":"S0269888914000228_ref11","unstructured":"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\u201311. AAAI Press."}],"container-title":["The Knowledge Engineering Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0269888914000228","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T14:42:01Z","timestamp":1767624121000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0269888914000228\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,13]]},"references-count":61,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,5]]}},"alternative-id":["S0269888914000228"],"URL":"https:\/\/doi.org\/10.1017\/s0269888914000228","relation":{},"ISSN":["0269-8889","1469-8005"],"issn-type":[{"type":"print","value":"0269-8889"},{"type":"electronic","value":"1469-8005"}],"subject":[],"published":{"date-parts":[[2014,11,13]]}}}