Advertisement

Towards a Runtime Verification Framework for the Ada Programming Language

  • André de Matos Pedro
  • David Pereira
  • Luís Miguel Pinho
  • Jorge Sousa Pinto
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8454)

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.

Keywords

Event Manager Schedulability Analysis Abstract Data Type Runtime Monitoring Static Analysis Approach 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in to check access.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bauer, A., Leucker, M., Schallhart, C.: Runtime Verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1–14:64 (2011)Google Scholar
  2. 2.
    Bellini, P., Mattolini, R., Nesi, P.: Temporal logics for real-time system specification. ACM Comput. Surv. 32(1), 12–42 (2000)CrossRefGoogle Scholar
  3. 3.
    Burns, A., Lin, T.M.: An engineering process for the verification of real-time systems. Form. Asp. Comput. 19(1), 111–136 (2007)CrossRefzbMATHGoogle Scholar
  4. 4.
    Burns, A., Lister, A.M.: A framework for building dependable systems. Comput. J. 34(2), 173–181 (1991)CrossRefGoogle Scholar
  5. 5.
    Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (1999)Google Scholar
  6. 6.
    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)
  7. 7.
    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)
  8. 8.
    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)
  9. 9.
    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)Google Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    Havelund, K., Rosu, G.: Monitoring Java Programs with Java PathExplorer. Electronic Notes in Theoretical Computer Science 55(2), 200–217 (2001)CrossRefGoogle Scholar
  12. 12.
    Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5), 293–303 (2009)CrossRefzbMATHGoogle Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    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)Google Scholar
  15. 15.
    Pucella, R.: On equivalences for a class of timed regular expressions. Electr. Notes Theor. Comput. Sci. 106, 315–333 (2004)CrossRefMathSciNetGoogle Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    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)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • André de Matos Pedro
    • 1
  • David Pereira
    • 1
  • Luís Miguel Pinho
    • 1
  • Jorge Sousa Pinto
    • 2
  1. 1.CISTER/INESC TEC, ISEPPolytechnic Institute of PortoPortugal
  2. 2.HASLab/INESC TEC & Universidade do MinhoPortugal

Personalised recommendations

Cite paper

Buy options