Abstract
We address the problem of runtime monitoring for hard real-time programs—a domain in which correctness is critical yet has largely been overlooked in the runtime monitoring community. We describe the challenges to runtime monitoring for this domain as well as an approach to satisfy the challenges. The core of our approach is a language and compiler called Copilot. Copilot is a stream-based dataflow language that generates small constant-time and constant-space C programs, implementing embedded monitors. Copilot also generates its own scheduler, obviating the need for an underlying real-time operating system.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Axelsson, E., Claessen, K., Dvai, G., Horvth, Z., Keijzer, K., Lyckegrd, B., Persson, A., Sheeran, M., Svenningsson, J., Vajda, A.: Feldspar: a domain specific language for digital signal processing algorithms. In: 8th ACM/IEEE Int. Conf. on Formal Methods and Models for Codesign (2010)
Chen, F., D’Amorim, M., Roşu, G.: A formal monitoring-base framewrok for software development analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 357–373. Springer, Heidelberg (2004)
Dwyer, M.B., Diep, M., Elbaum, S.: Reducing the cost of path property monitoring through sampling. In: Proceedings of the 23rd International Conference on Automated Software Engineering, pp. 228–237 (2008)
D’Angelo, B., Sankaranarayanan, S., Snchez, C., Robinson, W., Manna, Z., Finkbeiner, B., Spima, H., Mehrotra, S.: LOLA: Runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning, pp. 166–174. IEEE, Los Alamitos (2005)
Fishmeister, S., Lam, P.: On time-aware insrumentation of programs. In: RTAS 2009: 15h IEEE Real-Time and Embedded Technology and Application Symposium (2009)
Frama-C., http://frama-c.com/index.html (accessed August, 2010)
Goossens, J., Richard, P.: Overview of real-time scheduling problems (invited paper). In: Euro Workshop on Project Management and Scheduling (2004)
Havelund, K.: Runtime verification of C programs. In: Suzuki, K., Higashino, T., Ulrich, A., Hasegawa, T. (eds.) TestCom/FATES 2008. LNCS, vol. 5047, pp. 7–22. Springer, Heidelberg (2008)
Hawkins, T.: Controlling hybrid vehicles with Haskell. Presentation. Commercial Users of Functional Programming, CUFP (2008), http://cufp.galois.com/2008/schedule.html
Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language Lustre. Proceedings of the IEEE 79(9) (September 1991)
RTCA Inc. Software considerations in airborne systems and equipment certification, RCTA/DO-178B (1992)
Jones, S.P. (ed.): Haskell 1998 Language and Libraries: The Revised Report (2002), http://haskell.org/
Kim, M., Lee, I., Kannan, S., Sokolsky, O.: Java-MaC: a run-time assurance tool for Java. Formal Methods in System Design 24(1), 129–155 (2004)
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Communications of the ACM 21(7), 558–565 (1978)
Miner, P.: Hardware verification using coinductive assertions. PhD thesis, Indiana University, Bloomington, Adviser-Johnson, Steven D (1998)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)
Pellizzoni, R., Meredith, P., Caccamo, M., Rosu, G.: Hardware runtime monitoring for dependable cots-based real-time embedded systems. In: RTSS 2008: Proceedings of the 29th IEEE Real-Time System Symposium, pp. 481–491 (2008)
Pike, L., Shields, M., Matthews, J.: A verifying core for a cryptographic language compiler. In: Proceedings of the 6th Intl. Workshop on the ACL2 Theorem Prover and its Applications, pp. 1–10. ACM, New York (2006)
Sammapun, U., Lee, I., Sokolsky, O., Regehr, J.: Statistical runtime checking of probabilistic properties. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 164–175. Springer, Heidelberg (2007)
Zhu, H., Dwyer, M., Goddard, S.: Predictable runtime monitoring. In: ECRTS 2009: 21st Euromicro Conference on Real-Time Systems, pp. 173–183 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pike, L., Goodloe, A., Morisset, R., Niller, S. (2010). Copilot: A Hard Real-Time Runtime Monitor. In: Barringer, H., et al. Runtime Verification. RV 2010. Lecture Notes in Computer Science, vol 6418. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16612-9_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-16612-9_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16611-2
Online ISBN: 978-3-642-16612-9
eBook Packages: Computer ScienceComputer Science (R0)