Runtime verification and monitoring of embedded systems

Runtime verification and monitoring of embedded systems

For access to this article, please select a purchase option:

Buy article PDF
(plus tax if applicable)
Buy Knowledge Pack
10 articles for £75.00
(plus taxes if applicable)

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Your details
Why are you recommending this title?
Select reason:
IET Software — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

Ensuring the correctness of software applications is a difficult task. The area of runtime verification, which combines the approaches of formal verification and testing, offers a practical but limited solution that can help in finding many errors in software. Runtime verification relies upon tools for monitoring software execution. There are particular difficulties with regard to monitoring embedded systems. The concerns for arranging non-intrusive monitoring of embedded systems in a way that is suitable for use in runtime verification methods are considered here. A number of existing runtime verification tools are referenced, highlighting their requirement for monitoring solutions. Established and emerging approaches for the monitoring of software execution using execution monitors are reviewed, with an emphasis on the approaches that are best suited for use with embedded systems. A suggested solution for non-intrusive monitoring of embedded systems is presented. The conclusions summarise the possibilities for arranging non-intrusive monitoring of embedded systems, and the potential for runtime verification to utilise such monitoring approaches.


    1. 1)
      • Havelund, K., Goldberg, A.: `Verify your runs', Proc. Verified Software: Theories, Tools, Experiments (VSTTE'05), 10–13 October 2005, Zurich, Switzerland
    2. 2)
      • Havelund, K., Roşu, G.: `Monitoring Java programs with Java Pathexplorer', Proc. 1st Workshop on Runtime Verification (RV'2001) (13th Conf. Computer Aided Verification, CAV'01), 23 July 2001, Paris, France, Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier vol 55, (2), pp. 200–217
    3. 3)
      • Lee, I., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: `Runtime assurance based on formal specifications', Proc. Int. Conf. Parallel and Distributed Processing Techniques and Applications (PDPTA 1997), 30 June–3 July 1997, CSREA Press, Las Vegas, Nevada, USA
    4. 4)
    5. 5)
      • Monitoring program execution: a survey
    6. 6)
    7. 7)
      • Tutorial: computer system monitors
    8. 8)
      • Real-time execution monitoring
    9. 9)
      • Thane, H.: `Monitoring, testing and debugging distributed real-time systems', 2000, PhD, Kungliga Tekniska Högskolan, Stockholm, Sweden
    10. 10)
      • Gates, A.Q., Roach, S., Mondragon, O., Delgado, N.: `DynaMICs: comprehensive support for run-time monitoring', Proc. 1st Workshop on Runtime Verification (RV'2001) (13th Conf. Computer Aided Verification, CAV'01), 23 July 2001, Paris, France, 55, Elsevier, p. 164–180, Electronic Notes in Theoretical Computer Science (ENTCS)
    11. 11)
      • Mok, A.K., Liu, G.: `Efficient run-time monitoring of timing constraints', Proc. 3rd IEEE Real-Time Technology and Applications Symp. (RTAS'97), 9–11 June 1997, IEEE Computer Society Press, Montréal, Canada, p. 252–262
    12. 12)
      • Drusinsky, D.: `The temporal rover and the ATG rover', Proc. 7th Int. SPIN Workshop on SPIN Model Checking and Software Verification, 30 August–1 September 2000, 1885, Springer-Verlag, Stanford, California, USA, p. 323–330, Lecture Notes in Computer Science (LNCS)
    13. 13)
      • A noninterference monitoring and replay mechanism for real-time software testing and debugging
    14. 14)
      • Online system performance measurements with software and hybrid monitors
    15. 15)
      • A hybrid monitor for behavior and performance analysis of distributed systems
    16. 16)
      • Harelick, M., Stoyen, A.: `Concepts from deadline non-intrusive monitoring', Proc. 24th IFAC/IFIP Workshop on Real-Time Programming (WRTP '99), 30 May–3 June 1999, Elsevier, Wadern, Germany
    17. 17)
      • Fryer, R.: `Low and non-intrusive software instrumentation: a survey of requirements and methods', Proc. 17th AIAA/IEEE/SAE Digital Avionics Systems Conf. (DASC), 31 October–7 November 1998, 1, IEEE Press, Bellevue, Washington, USA, p. C22/1–C22/8
    18. 18)
      • Pneuli, A.: `The temporal logic of programs', Proc. 18th IEEE Symp. Foundations of Computer Science (FOCS 1977), 1977, p. 46–77
    19. 19)
      • Kim, M., Viswanathan, M., Ben-Abdallah, H., Kannan, S., Lee, I., Sokolsky, O.: `Formally specified monitoring of temporal properties', Proc. 11th Euromicro Conf. Real-Time Systems (Euromicro RTS'99), 9–11 June 1999, IEEE Computer Society Press, York, England, UK, p. 114–122
    20. 20)
      • Havelund, K., Roşu, G.: `Synthesizing monitors for safety properties', Proc. 8th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2002) (part of Joint European Conf. Theory and Practice of Software, ETAPS 2002), 8–12 April 2002, 2280, Springer-Verlag, Grenoble, France, p. 342–356, Lecture Notes in Computer Science (LNCS)
    21. 21)
      • JTrek, Digital Equipment Corporation (Compaq, HP), 1997
    22. 22)
      • Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.F.: `The maude system', Proc. 10th Int. Conf. Rewriting Techniques and Applications (RTA-99), July 1999, 1631, Springer-Verlag, Trento, Italy, p. 240–243, Lecture Notes in Computer Science (LNCS)
    23. 23)
    24. 24)
      • Havelund, K., Roşu, G.: `Java Pathexplorer – a runtime verification tool', 6thInt. Symp. on Artificial Intelligence, Robots and Automation in Space (i-SAIRAS'01), 18–21 June 2001, Montréal, Canada
    25. 25)
      • Eraser: a dynamic data race detector for multithreaded programs
    26. 26)
      • Drusinsky, D.: `Monitoring temporal rules combined with time series', Proc. 15th Int. Conf. Computer-Aided Verification (CAV '03), 8–12 July 2003, 2725, Springer-Verlag, Boulder, Colorado, USA, p. 114–117, Lecture Notes in Computer Science (LNCS)
    27. 27)
      • Sammapun, U., Easwaran, A., Lee, I., Sokolsky, O.: `Simulation of simultaneous events in regular expressions for run-time verification', Proc. 4th Workshop on Runtime Verification (RV 2004) (in conj. w. 7th European Joint Conf. Theory and Practice of Software, ETAPS'04), 3 April 2004, 113, Elsevier, Barcelona, Spain, p. 123–143, Electronic Notes in Theoretical Computer Science (ENTCS)
    28. 28)
      • Barringer, H., Goldberg, A., Havelund, K., Sen, K.: `Rule-based runtime verification', Proc. 5th Int. Conf. Verification, Model Checking and Abstract Interpretation (VMCAI'04), 11–13 January 2004, 2937, Springer-Verlag, Venice, Italy, p. 44–57, Lecture Notes in Computer Science (LNCS)
    29. 29)
      • D'Amorim, M., Havelund, K.: `Event-based runtime verification of java programs', Proc. 3rd Int. Workshop on Dynamic Analysis (WODA 2005), 17 May 2005, 30, ACM Press, St. Louis, Missouri, USA, p. 1–7, ACM SIGSOFT Software Engineering Notes
    30. 30)
      • On-line monitoring: a tutorial
    31. 31)
      • Thane, H., Sundmark, D., Huselius, J., Petterson, A.: `Replay debugging of real-time systems using time machines', Proc. 17th Int. Parallel and Distributed Processing Symp. (IPDPS '03), 22–26 April 2003, IEEE Computer Society Press, Nice, France, p. 288–295
    32. 32)
      • System performance evaluation: survey and appraisal
    33. 33)
      • Karush, A.D.: `Two approaches for measuring the performance of time-sharing systems', Proc. 2nd ACM Symp. Operating Systems Principles (SOSP'69), 20–22 October 1969, ACM Press, Princeton, New Jersey, USA, p. 159–166
    34. 34)
      • Performance evaluation and monitoring
    35. 35)
      • Gallo, A., Wilder, R.P.: `Performance measurement of data communications systems with emphasis on open system interconnections (OSI)', Proc. 8th Annual Symp. Computer Architecture (ICSA'81), 12–14 May 1981, IEEE Computer Society Press, Minneapolis, Minnesota, USA, p. 149–161
    36. 36)
    37. 37)
      • El Shobaki, M., Lindh, L.: `A hardware and software monitor for high-level system-on-chip verification', Proc. IEEE 2001 2nd Int. Symp. Quality Electronic Design (ISQED 2001), 26–28 March 2001, IEEE Computer Society Press, San Jose, California, USA, p. 56–61
    38. 38)
      • Measurement of system operational statistics
    39. 39)
      • A real-time monitor for a distributed real-time operating system
    40. 40)
      • Performance monitoring in computer systems: a structured approach
    41. 41)
      • Deniston, W.R.: `SIPE: A TSS/360 software measurement technique', Proc. 24th Nat. Conf. ACM, 26–28 August 1969, ACM Press
    42. 42)
      • Rota, S.R., de Almeida, J.R.: `Run-time monitoring for dependable systems: an approach and a case study', Proc. 23rd IEEE Int. Symp. Reliable Distributed Systems (SRDS 2004), 18–20 October 2004, IEEE Computer Society Press, Florianópolis, Brazil, p. 41–49
    43. 43)
    44. 44)
      • El Shobaki, M.: `On-chip monitoring of single- and multiprocessor hardware real-time operating systems', Proc. 8th Int. Conf. Real-Time Computing Systems and Applications (RTCSA 2002), 18–20 March 2002, Tokyo, Japan
    45. 45)
      • Walters, G., King, E., Kessinger, R., Fryer, R.: `Processor Design and Implementation for Real-Time Testing of Embedded Systems', Proc. 17th AIAA/IEEE/SAE Digital Avionics Systems Conf. (DASC), 31 October–7 November 1998, 1, IEEE Press, Bellevue, Washington, USA, p. B44/1–B44/8
    46. 46)
    47. 47)
      • MacNamee, C., Heffernan, D.: `Implementation approaches for requirements-based monitors for embedded systems', Proc. IEEE IC Test Workshop (ICTW 2004), 13–14 September 2004, University of Limerick, E&CE Dept, Limerick, Ireland
    48. 48)
      • Drechsler, R.: `Synthesizing checkers for on-line verification of system-on-chip designs', Proc. 2003 IEEE Int. Symp. Circuits and Systems (ISCAS'03), 25–28 May 2003, IV, IEEE, Bangkok, Thailand, p. 748–751
    49. 49)
      • IEEE 1850-2005: ‘IEEE Standard for property specification language (PSL)’, IEEE Standards Association, 2005
    50. 50)
      • Peterson, K., Savaria, Y.: `Assertion-based on-line verification and debug environment for complex hardware systems', Proc. 2004 IEEE Int. Symp. Circuits and Systems, 23–26 May 2004, II, IEEE, Vancouver, British Columbia, Canada, p. 685–688
    51. 51)
      • FPGA based CPU instrumentation for hard real-time embedded system testing

Related content

This is a required field
Please enter a valid email address