{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T06:27:10Z","timestamp":1750746430888},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2009,8,5]],"date-time":"2009-08-05T00:00:00Z","timestamp":1249430400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2009,12]]},"DOI":"10.1007\/s11334-009-0096-1","type":"journal-article","created":{"date-parts":[[2009,8,4]],"date-time":"2009-08-04T08:47:56Z","timestamp":1249375676000},"page":"231-241","source":"Crossref","is-referenced-by-count":18,"title":["Software monitoring through formal specification animation"],"prefix":"10.1007","volume":"5","author":[{"given":"Hui","family":"Liang","sequence":"first","affiliation":[]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[]},{"given":"Jing","family":"Sun","sequence":"additional","affiliation":[]},{"given":"W. Eric","family":"Wong","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,8,5]]},"reference":[{"key":"96_CR1","unstructured":"Abercrombie P, Karaorman M (2002) jContractor: Bytecode instrumentation techniques for implementing design by contract in Java. In: Proceedings of second workshop on runtime verification (RV\u201902)"},{"key":"96_CR2","unstructured":"Barnett M, Rustan K, Schulte W (2004) The Spec# programming system: an overview. In: Proceedings of international workshop on construction and analysis of safe, secure, and interoperable smart devices, pp 49\u201369"},{"key":"96_CR3","unstructured":"Bartetzko D, Fischer C, Moller M, Wehrheim H (2001) Jass\u2014Java with assertions. In: Proceedings of first workshop on runtime verification, RV\u201901"},{"key":"96_CR4","doi-asserted-by":"crossref","unstructured":"Chen F, D\u2019Amorim M, Ro\u015fu G (2004) A formal monitoring-based framework for software development and analysis. In: Proceedings of the 6th international conference on formal engineering methods (ICFEM\u201904), Springer, Heidelberg, pp 357\u2013373","DOI":"10.1007\/978-3-540-30482-1_31"},{"key":"96_CR5","doi-asserted-by":"crossref","unstructured":"Drusinsky D (2000) The temporal rover and the ATG rover. In: Proceedings of the 7th international SPIN workshop on SPIN model checking and software verification, pp 323\u2013330","DOI":"10.1007\/10722468_19"},{"key":"96_CR6","unstructured":"Havelund K, Ro\u015fu G (2001) Java PathExplorer\u2014a runtime verification tool. In: Proceedings of 6th international symposium on artificial intelligence, robotics and automation in space, ISAIRAS\u201901"},{"key":"96_CR7","doi-asserted-by":"crossref","unstructured":"Hlady M, Kovacevic R, Li JJ, Pekilis B, Prairie D, Savor T, Seviora R, Simser D, Vorobiev A (1995) An approach to automatic detection of software failures. In: Proceedings of sixth international symposium on software reliability engineering","DOI":"10.1109\/ISSRE.1995.497672"},{"key":"96_CR8","unstructured":"Kim M, Kannan S, Lee I, Sokolsky O (2001) Java-MaC: a run-time assurance tool for Java. In: Proceedings of first workshop on runtime verification, RV\u201901"},{"issue":"3","key":"96_CR9","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/s10703-005-3400-1","volume":"27","author":"M Karaorman","year":"2005","unstructured":"Karaorman M, Abercrombie P (2005) jContractor: introducing design-by-contract to Java using reflective bytecode instrumentation. Formal Methods Syst Des 27(3): 275\u2013312","journal-title":"Formal Methods Syst Des"},{"key":"96_CR10","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/j.entcs.2004.12.009","volume":"111","author":"M Satpathy","year":"2005","unstructured":"Satpathy M, Leuschel M, Butler MJ (2005) ProTest: an automatic test environment for B specifications. Electron. Notes Theor Comp Sci 111: 113\u2013136","journal-title":"Electron. Notes Theor Comp Sci"},{"key":"96_CR11","doi-asserted-by":"crossref","unstructured":"Liang H, Dong JS, Sun J, Duke R, Seviora RE (2006) Formal Specification-based Online Monitoring. In: ICECCS \u201906: proceedings of the 11th IEEE international conference on engineering of complex computer systems, Washington, DC, USA, IEEE Computer Society, Los Alamitos, pp 152\u2013160","DOI":"10.1109\/ICECCS.2006.1690364"},{"key":"96_CR12","volume-title":"The way of Z: practical programming with formal methods","author":"J Jacky","year":"1997","unstructured":"Jacky J (1997) The way of Z: practical programming with formal methods. Cambridge University Press, Cambridge"},{"key":"96_CR13","volume-title":"The Z notation: a reference manual","author":"J Spivey","year":"1989","unstructured":"Spivey J (1989) The Z notation: a reference manual. Prentice-Hall, Englewood Cliffs"},{"key":"96_CR14","volume-title":"Using Z: specification, refinement, and proof","author":"J Woodcock","year":"1996","unstructured":"Woodcock J, Davies J (1996) Using Z: specification, refinement, and proof. Prentice-Hall, Englewood Cliffs"},{"key":"96_CR15","unstructured":"Miller T, Strooper P (2000) A framework for systematic specification animation. Technical report 02-35, The University of Queensland"},{"key":"96_CR16","doi-asserted-by":"crossref","unstructured":"Miller T, Strooper P (2002) Model-based specification animation using testgraphs. In: ICFEM \u201902: proceedings of the 4th international conference on formal engineering methods, Springer, Heidelberg, pp 192\u2013203","DOI":"10.1007\/3-540-36103-0_21"},{"key":"96_CR17","doi-asserted-by":"crossref","unstructured":"Hewitt MA, O\u2019Halloran C, Sennett CT (1997) Experiences with PiZA, an animator for Z. In: ZUM \u201997: Proceedings of the 10th international conference of Z users on the Z formal specification notation, Springer, Heidelberg, pp 37\u201351","DOI":"10.1007\/BFb0027282"},{"key":"96_CR18","doi-asserted-by":"crossref","unstructured":"Hazel D, Strooper P, Traynor O (1997) Possum: an animator for the SUM specification language. In: APSEC \u201997: proceedings of the fourth Asia-Pacific software engineering and international computer science conference, IEEE Computer Society, Los Alamitos, p 42","DOI":"10.1109\/APSEC.1997.640160"},{"key":"96_CR19","doi-asserted-by":"crossref","unstructured":"Hazel D, Strooper P, Traynor O (1998) Requirements engineering and verification using specification animation. In: ASE \u201998: Proceedings of the Thirteenth IEEE Conference on Automated Software Engineering, IEEE Computer Society, Los Alamitos, p 302","DOI":"10.1109\/ASE.1998.732685"},{"key":"96_CR20","doi-asserted-by":"crossref","unstructured":"Waeselynck H, Behnia S (1998) B model animation for external verification. In: Proceedings of the second IEEE international conference on formal engineering methods, ICFEM \u201998, pp 36\u201345","DOI":"10.1109\/ICFEM.1998.730568"},{"key":"96_CR21","unstructured":"Utting M (2000) Data structures for Z testing tools. In: Proceedings of FM-TOOLS"},{"key":"96_CR22","unstructured":"jdb - The Java debugger. ( http:\/\/java.sun.com\/ )"},{"key":"96_CR23","doi-asserted-by":"crossref","unstructured":"Achuthan R, Alagar VS, Radhakrishnan T (1995) An object-oriented modeling of real-time robotic assembly system. In: Proceedings of the 1st IEEE international conference on engineering of complex computer systems (ICECCS \u201995), pp 310\u2013313","DOI":"10.1109\/ICECCS.1995.479350"},{"issue":"3","key":"96_CR24","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/BF01245633","volume":"3","author":"VS Alagar","year":"1991","unstructured":"Alagar VS, Ramanathan G (1991) Functional specification and proof of correctness for time dependent behaviour of reactive systems. Formal Aspect Comput 3(3): 253\u2013283","journal-title":"Formal Aspect Comput"},{"key":"96_CR25","unstructured":"Dong JS, Colton J, Zucconi L (1996) A formal object approach to real-time specification. In: Proceedings of the 3rd Asia-Pacific software engineering conference (APSEC\u201996)"},{"key":"96_CR26","unstructured":"Curtis SA, Mica J, Nuth J, Marr G, Rilee ML, Bhat MK (2000) ANTS (Autonomous Nano-Technology Swarm): an artificial intelligence approach to asteroid belt resource exploration. In: Proceedings of international astronautical federation, 51st Congress"},{"key":"96_CR27","doi-asserted-by":"crossref","unstructured":"Curtis SA, Truszkowski WF, Rilee ML, Clark PE (2003) ANTS for human exploration and development of space. In: Proceedings of IEEE aerospace conference","DOI":"10.1109\/AERO.2003.1235057"},{"key":"96_CR28","doi-asserted-by":"crossref","unstructured":"Hinchey MG, Dai YS, Rouff CA, Rash JL, Qi MR (2007) Modeling for NASA autonomous nano-technology swarm missions and model-driven autonomic computing. In: AINA \u201907: Proceedings of the 21st international conference on advanced networking and applications, pp 250\u2013257","DOI":"10.1109\/AINA.2007.93"},{"issue":"5","key":"96_CR29","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1109\/MITP.2004.66","volume":"6","author":"WE Truszkowski","year":"2004","unstructured":"Truszkowski WE, Hinchey MG, Rash JL, Rouff CA (2004) NASA\u2019s swarm missions: the challenge of building autonomous software. IT Prof 6(5): 47\u201352","journal-title":"IT Prof"},{"issue":"3","key":"96_CR30","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/TSMCC.2006.871600","volume":"36","author":"WE Truszkowski","year":"2006","unstructured":"Truszkowski WE, Hinchey MG, Rash JL, Rouff CA (2006) Autonomous and autonomic systems: a paradigm for future space exploration mission. IEEE Trans Syst Man Cybermet Part C Appl Rev 36(3): 279\u2013291","journal-title":"IEEE Trans Syst Man Cybermet Part C Appl Rev"},{"key":"96_CR31","doi-asserted-by":"crossref","unstructured":"Hinchey MG, Rouff CA, Rash JL, Truszkowski WF (2005) Requirements of an integrated formal method for intelligent swarms. In: FMICS \u201905: Proceedings of the 10th international workshop on formal methods for industrial critical systems, pp 125\u2013133","DOI":"10.1145\/1081180.1081196"},{"issue":"6","key":"96_CR32","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1109\/2.386988","volume":"28","author":"BA Schroeder","year":"1995","unstructured":"Schroeder BA (1995) On-line monitoring: a tutoiral. IEEE Comp 28(6): 72\u201378","journal-title":"IEEE Comp"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-009-0096-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-009-0096-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-009-0096-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T13:47:44Z","timestamp":1559396864000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-009-0096-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,8,5]]},"references-count":32,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["96"],"URL":"https:\/\/doi.org\/10.1007\/s11334-009-0096-1","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,8,5]]}}}