Abstract
We introduce a formal framework to provide an efficient event-based monitoring technique, and we describe its current implementation as the MahaRAJA software tool. The framework enables the quantitative runtime verification of temporal properties extracted from occurring events on Java programs. The monitor continuously evaluates the conformance of the concrete implementation with respect to its formal specification given in terms of Time Basic Petri nets, a particular timed extension of Petri nets. The system under test is instrumented by using simple Java annotations on methods to link the implementation to its formal model. This allows a separation between implementation and specification that can be used for other purposes such as formal verification, simulation, and model-based testing. The tool has been successfully used to monitor at runtime and test a number of benchmarking case-studies. Experiments show that our approach introduces bounded overhead and effectively reduces the involvement of the monitor at run time by using negligible auxiliary memory. A comparison with a number of state-of-the-art runtime verification tools is also presented.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Monitoring at Runtime of temporAl properties on Java Applications.
- 2.
\(b \in Bag({X}) \) is a map \(X \rightarrow \mathbb {N}\), formally expressed as a weighted sum of X elements.
- 3.
The source code, binaries, and some runnable examples can be found at [17].
- 4.
They are recorded in class files by the compiler and retained by the virtual machine at run time, so they can be read reflectively by the Observer component.
- 5.
Additional information about the configurations of MahaRAJA and the JVM is available at [17].
References
Delgado, N., Gates, A.Q., Roach, S.: A taxonomy and catalog of runtime software-fault monitoring tools. IEEE Trans. Softw. Eng. 30(12), 859–872 (2004)
Ghezzi, C., Mandrioli, D., Morasca, S., Pezzè, M.: A unified high-level Petri net formalism for time-critical systems. IEEE Trans. Softw. Eng. 17, 160–172 (1991)
Chen, F., D’Amorim, M., Roşu, G.: A formal monitoring-based framework for software development and analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 357–372. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30482-1_31
Arcaini, P., Gargantini, A., Riccobene, E.: Combining model-based testing and runtime monitoring for program testing in the presence of nondeterminism. In: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation Workshops (ICSTW), pp. 178–187, March 2013
Liang, H., Dong, J.S., Sun, J., Wong, W.E.: Software monitoring through formal specification animation. Innov. Syst. Softw. Eng. 5(4), 231–241 (2009)
Felder, M., Gargantini, A., Morzenti, A.: A theory of implementation and refinement in timed Petri nets. Theoret. Comput. Sci. 202(12), 127–161 (1998)
Bengtsson, J., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. Springer, Heidelberg (2004)
Gurevich, Y.: Sequential abstract-state machines capture sequential algorithms. ACM Trans. Comput. Log. 1(1), 77–111 (2000)
Ramchandani, C.: Analysis of asynchronous concurrent systems by timed Petri nets. Technical report, Cambridge, MA, USA (1974)
Iglesia, D.G.D.L., Weyns, D.: MAPE-K formal templates to rigorously design behaviors for self-adaptive systems. ACM Trans. Auton. Adapt. Syst. 10(3), 15:1–15:31 (2015)
Lee, W.J., Cha, S.D., Kwon, Y.R.: Integration and analysis of use cases using modular Petri nets in requirements engineering. IEEE Trans. Softw. Eng. 24(12), 1115–1130 (1998)
Zhu, H., Dwyer, M.B., Goddard, S.: Predictable runtime monitoring. In: Proceedings of the 2009 21st Euromicro Conference on Real-Time Systems, ser. ECRTS 2009, pp. 173–183. IEEE Computer Society, Washington, DC (2011)
Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998). doi:10.1007/3-540-65306-6_21
Gomaa, H.: Designing Concurrent, Distributed, and Real-Time Applications with UML, 1st edn. Addison-Wesley Longman Publishing Co., Inc., Boston (2000)
Camilli, M., Gargantini, A., Scandurra, P.: Specifying and verifying real-time self-adaptive systems. In: 2015 IEEE 26th International Symposium on Software Reliability Engineering (ISSRE), pp. 303–313, November 2015
Bellettini, C., Capra, L.: Reachability analysis of time basic Petri nets: a time coverage approach. In: Proceedings of the 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, ser. SYNASC 2011, pp. 110–117. IEEE Computer Society, Washington, DC (2011)
Maharaja framework. http://camilli.di.unimi.it/maharaja/. Accessed Dec 2016
Hillah, L.M., Kordon, F., Petrucci, L., Trèves, N.: PNML framework: an extendable reference implementation of the Petri net markup language. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 318–327. Springer, Heidelberg (2010). doi:10.1007/978-3-642-13675-7_20
Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of AspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 327–354. Springer, Heidelberg (2001). doi:10.1007/3-540-45337-7_18
Chronicle Software: Java Thread Affinity Library (2016). http://chronicle.software/products/thread-affinity/. Accessed Jan 2016
Li, T., Baumberger, D., Hahn, S.: Efficient and scalable multiprocessor fair scheduling using distributed weighted round-robin. SIGPLAN Not. 44(4), 65–74 (2009)
Arcaini, P., Gargantini, A., Riccobene, E.: CoMA: conformance monitoring of Java programs by abstract state machines. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 223–238. Springer, Heidelberg (2012). doi:10.1007/978-3-642-29860-8_17
Havelund, K., Roşu, G.: An overview of the runtime verification tool Java PathExplorer. Formal Methods Syst. Des. 24(2), 189–215 (2004)
Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance approach for Java programs. Form. Methods Syst. Des. 24(2), 129–155 (2004)
d’Amorim, M., Havelund, K.: Event-based runtime verification of Java programs. SIGSOFT Softw. Eng. Notes 30(4), 1–7 (2005)
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24622-0_5
Colombo, C., Pace, G.J., Schneider, G.: Dynamic event-based runtime monitoring of real-time and contextual properties. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 135–149. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03240-0_13
Bonakdarpour, B., Navabpour, S., Fischmeister, S.: Time-triggered runtime verification. Formal Methods Syst. Des. 43(1), 29–60 (2013)
Navabpour, S., Bonakdarpour, B., Fischmeister, S.: Path-aware time-triggered runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 199–213. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35632-2_21
Mastrangelo, L., Hauswirth, M.: JNIF: Java native instrumentation framework. In: Proceedings of the International Conference on Principles and Practices of Programming on the Java Platform: Virtual Machines, Languages, and Tools, ser. PPPJ 2014, pp. 194–199. ACM, New York (2014)
de Lemos, R., Garlan, D., Ghezzi, C., Giese, H.: Software engineering for self-adaptive systems: assurances (Dagstuhl Seminar 13511). Dagstuhl Rep. 3(12), 67–96 (2014). http://drops.dagstuhl.de/opus/volltexte/2014/4508
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Camilli, M., Gargantini, A., Scandurra, P., Bellettini, C. (2017). Event-Based Runtime Verification of Temporal Properties Using Time Basic Petri Nets. In: Barrett, C., Davies, M., Kahsai, T. (eds) NASA Formal Methods. NFM 2017. Lecture Notes in Computer Science(), vol 10227. Springer, Cham. https://doi.org/10.1007/978-3-319-57288-8_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-57288-8_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-57287-1
Online ISBN: 978-3-319-57288-8
eBook Packages: Computer ScienceComputer Science (R0)