Abstract
Runtime verification is an emerging discipline that investigates methods and tools to enable the verification of program properties during the execution of the application. The goal is to complement static analysis approaches, in particular when static verification leads to the explosion of states. Non-functional properties, such as the ones present in real-time systems are an ideal target for this kind of verification methodology, as are usually out of the range of the power and expressiveness of classic static analyses. In this paper, we present a framework that allows real-time programs written in Ada to be augmented with runtime verification capabilities. Our framework provides the infrastructures which is needed to instrument the code with runtime monitors. These monitors are responsible for observing the system and reaching verdicts about whether its behavior is compliant with its non-functional properties. We also sketch a contract language to extend the one currently provided by Ada, with the long term goal of having an elegant way in which runtime monitors can be automatically synthesized and instrumented into the target systems. The usefulness of the proposed approach is demonstrated by showing its use for an application scenario.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bauer, A., Leucker, M., Schallhart, C.: Runtime Verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1–14:64 (2011)
Bellini, P., Mattolini, R., Nesi, P.: Temporal logics for real-time system specification. ACM Comput. Surv. 32(1), 12–42 (2000)
Burns, A., Lin, T.M.: An engineering process for the verification of real-time systems. Form. Asp. Comput. 19(1), 111–136 (2007)
Burns, A., Lister, A.M.: A framework for building dependable systems. Comput. J. 34(2), 173–181 (1991)
Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)
de Matos Pedro, A., Pereira, D., Pinho, L.M., Pinto, J.S.: Monitors provided for the Mine Drainage System Simulator, http://webpages.cister.isep.ipp.pt/~anmap/adaeurope14/examples/mine_drainage/monitors/ (accessed: December 15, 2013)
de Matos Pedro, A., Pereira, D., Pinho, L.M., Pinto, J.S.: Runtime Monitoring Library for RMF4Ada, http://webpages.cister.isep.ipp.pt/~anmap/adaeurope14/ (accessed: December 15, 2013)
de Matos Pedro, A., Pereira, D., Pinho, L.M., Pinto, J.S.: The Mine Drainage Simulator Code, http://webpages.cister.isep.ipp.pt/~anmap/adaeurope14/examples/mine_drainage/system/ (accessed: December 15, 2013)
de Matos Pedro, A., Pereira, D., Pinho, L.M., Pinto, J.S.: Logic-based Schedulability Analysis for Compositional Hard Real-Time Embedded Systems. In: Proceedings of the 6th International Workshop on Compositional Theory and Technology for Real-Time Embedded Systems, CRTS 2013 (2013)
de Matos Pedro, A., Pereira, D., Pinho, L.M., Pinto, J.S.: A Compositional Monitoring Framework for Hard Real-Time Systems. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 16–30. Springer, Heidelberg (2014)
Havelund, K., Rosu, G.: Monitoring Java Programs with Java PathExplorer. Electronic Notes in Theoretical Computer Science 55(2), 200–217 (2001)
Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5), 293–303 (2009)
Pike, L., Niller, S., Wegmann, N.: Runtime verification for ultra-critical systems. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 310–324. Springer, Heidelberg (2012)
Pike, L., Wegmann, N., Niller, S., Goodloe, A.: Copilot: Monitoring embedded systems. Innovations in Systems and Software Engineering: Special Issue on Software Health Management (2012)
Pucella, R.: On equivalences for a class of timed regular expressions. Electr. Notes Theor. Comput. Sci. 106, 315–333 (2004)
Aldea Rivas, M., González Harbour, M.: MaRTE OS: An Ada Kernel for Real-Time Embedded Applications. In: Strohmeier, A., Craeynest, D. (eds.) Ada-Europe 2001. LNCS, vol. 2043, pp. 305–316. Springer, Heidelberg (2001)
Sen, K.: Generating optimal monitors for extended regular expressions. In: Proc. of the 3rd Workshop on Runtime Verification (RV 2003). ENTCS, vol. 89, pp. 162–181 (2003)
Zamorano, J., Alonso, A., Pulido, J.A., de la Puente, J.A.: Implementing execution-time clocks for the ada ravenscar profile. In: Llamosí, A., Strohmeier, A. (eds.) Ada-Europe 2004. LNCS, vol. 3063, pp. 132–143. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
de Matos Pedro, A., Pereira, D., Pinho, L.M., Pinto, J.S. (2014). Towards a Runtime Verification Framework for the Ada Programming Language. In: George, L., Vardanega, T. (eds) Reliable Software Technologies – Ada-Europe 2014. Ada-Europe 2014. Lecture Notes in Computer Science, vol 8454. Springer, Cham. https://doi.org/10.1007/978-3-319-08311-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-08311-7_6
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08310-0
Online ISBN: 978-3-319-08311-7
eBook Packages: Computer ScienceComputer Science (R0)