Abstract
This paper presents a formal specification-based software monitoring approach that can dynamically and continuously monitor the behaviors of a target system and explicitly recognize undesirable behaviors in the implementation with respect to its formal specification. The key idea of our approach is in building a monitoring module that connects a specification animator with a program debugger. The requirements information about expected dynamic behaviors of the target system are gathered from the formal specification animator, while the actual behaviors of concrete implementations of the target system are obtained through the program debugger. Based on the information obtained from both sides, the judgement on the conformance of the concrete implementation with respect to the formal specification is made timely while the target system is running. Furthermore, the proposed formal specification-based software monitoring technique does not embed any instrumentation codes to the target system nor does it annotate the target system with any formal specifications. It can detect implementation errors in a real-time manner, and help the developers and users of the system to react to the problems before critical failure occurs.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
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’02)
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–69
Bartetzko D, Fischer C, Moller M, Wehrheim H (2001) Jass—Java with assertions. In: Proceedings of first workshop on runtime verification, RV’01
Chen F, D’Amorim M, Roşu G (2004) A formal monitoring-based framework for software development and analysis. In: Proceedings of the 6th international conference on formal engineering methods (ICFEM’04), Springer, Heidelberg, pp 357–373
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–330
Havelund K, Roşu G (2001) Java PathExplorer—a runtime verification tool. In: Proceedings of 6th international symposium on artificial intelligence, robotics and automation in space, ISAIRAS’01
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
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’01
Karaorman M, Abercrombie P (2005) jContractor: introducing design-by-contract to Java using reflective bytecode instrumentation. Formal Methods Syst Des 27(3): 275–312
Satpathy M, Leuschel M, Butler MJ (2005) ProTest: an automatic test environment for B specifications. Electron. Notes Theor Comp Sci 111: 113–136
Liang H, Dong JS, Sun J, Duke R, Seviora RE (2006) Formal Specification-based Online Monitoring. In: ICECCS ’06: proceedings of the 11th IEEE international conference on engineering of complex computer systems, Washington, DC, USA, IEEE Computer Society, Los Alamitos, pp 152–160
Jacky J (1997) The way of Z: practical programming with formal methods. Cambridge University Press, Cambridge
Spivey J (1989) The Z notation: a reference manual. Prentice-Hall, Englewood Cliffs
Woodcock J, Davies J (1996) Using Z: specification, refinement, and proof. Prentice-Hall, Englewood Cliffs
Miller T, Strooper P (2000) A framework for systematic specification animation. Technical report 02-35, The University of Queensland
Miller T, Strooper P (2002) Model-based specification animation using testgraphs. In: ICFEM ’02: proceedings of the 4th international conference on formal engineering methods, Springer, Heidelberg, pp 192–203
Hewitt MA, O’Halloran C, Sennett CT (1997) Experiences with PiZA, an animator for Z. In: ZUM ’97: Proceedings of the 10th international conference of Z users on the Z formal specification notation, Springer, Heidelberg, pp 37–51
Hazel D, Strooper P, Traynor O (1997) Possum: an animator for the SUM specification language. In: APSEC ’97: proceedings of the fourth Asia-Pacific software engineering and international computer science conference, IEEE Computer Society, Los Alamitos, p 42
Hazel D, Strooper P, Traynor O (1998) Requirements engineering and verification using specification animation. In: ASE ’98: Proceedings of the Thirteenth IEEE Conference on Automated Software Engineering, IEEE Computer Society, Los Alamitos, p 302
Waeselynck H, Behnia S (1998) B model animation for external verification. In: Proceedings of the second IEEE international conference on formal engineering methods, ICFEM ’98, pp 36–45
Utting M (2000) Data structures for Z testing tools. In: Proceedings of FM-TOOLS
jdb - The Java debugger. (http://java.sun.com/)
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 ’95), pp 310–313
Alagar VS, Ramanathan G (1991) Functional specification and proof of correctness for time dependent behaviour of reactive systems. Formal Aspect Comput 3(3): 253–283
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’96)
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
Curtis SA, Truszkowski WF, Rilee ML, Clark PE (2003) ANTS for human exploration and development of space. In: Proceedings of IEEE aerospace conference
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 ’07: Proceedings of the 21st international conference on advanced networking and applications, pp 250–257
Truszkowski WE, Hinchey MG, Rash JL, Rouff CA (2004) NASA’s swarm missions: the challenge of building autonomous software. IT Prof 6(5): 47–52
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–291
Hinchey MG, Rouff CA, Rash JL, Truszkowski WF (2005) Requirements of an integrated formal method for intelligent swarms. In: FMICS ’05: Proceedings of the 10th international workshop on formal methods for industrial critical systems, pp 125–133
Schroeder BA (1995) On-line monitoring: a tutoiral. IEEE Comp 28(6): 72–78
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Liang, H., Dong, J.S., Sun, J. et al. Software monitoring through formal specification animation. Innovations Syst Softw Eng 5, 231–241 (2009). https://doi.org/10.1007/s11334-009-0096-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11334-009-0096-1