Monitoring Temporal Properties of Continuous Signals

1. Abarbanel, Y., Beer, I., Glushovsky, L., Keidar, S., Wolfsthal, Y.: FoCs: Automatic Generation of Simulation Checkers from Formal Specifications. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 538–542. Springer, Heidelberg (2000)

   Chapter  Google Scholar 

2. Alur, R., Feder, T., Henzinger, T.A.: The Benefits of Relaxing Punctuality. Journal of the ACM 43(1), 116–146 (1996)

   Article  MATH  MathSciNet  Google Scholar 

3. Alur, R., Henzinger, T.A.: Logics and Models of Real-Time: A Survey. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992)

   Chapter  Google Scholar 

4. Beer, I., Ben David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The Temporal Logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 363. Springer, Heidelberg (2001)

   Chapter  Google Scholar 

5. Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., McKenzie, P.: Systems and Software Verification: Model-Checking Techniques and Tools. Springer, Heidelberg (2001)

   MATH  Google Scholar 

6. Bensalem, S., Bozga, M., Krichen, M., Tripakis, S.: Testing Conformance of Real-time Applications with Automatic Generation of Observers. In: Proc. RV 2004 (2004) (to appear in ENTCS)

   Google Scholar 

7. Bendotti, P.: Steam Generator Water Level Control Problem. Technical report, CC project (2002)

   Google Scholar 

8. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)

   Google Scholar 

9. Donzé, A.: Etude d’un Modèle de Contrôleur Hybride. Master’s thesis, INPG (2003)

   Google Scholar 

10. Drusinsky, D.: The Temporal Rover and the ATG Rover. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 323–330. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

11. Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with Temporal Logic on Truncated Paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

12. Geilen, M.C.W., Dams, D.R.: An On-the-fly Tableau Construction for a Realtime Temporal Logic. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 276–290. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

13. Geilen, M.C.W.: Formal Techniques for Verification of Complex Real-time Systems. PhD thesis, Eindhoven University of Technology (2002)

    Google Scholar 

14. Geilen, M.C.W.: An Improved On-the-fly Tableau Construction for a Real-time Temporal Logic. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 394–406. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

15. Henzinger, T.A.: It’s about Time: Real-time Logics Reviewed. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 439–454. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

16. Havelund, K., Rosu, G.: Java PathExplorer - a Runtime Verification Tool. In: Proc. ISAIRAS 2001 (2001)

    Google Scholar 

17. Havelund, K., Rosu, G. (eds.): Runtime Verification RV 2002. ENTCS, vol. 70(4) (2002)

    Google Scholar 

18. Havelund, K., Rosu, G.: Synthesizing Monitors for Safety Properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

19. Kim, M., Lee, I., Sammapun, U., Shin, J., Sokolsky, O.: Monitoring, Checking, and Steering of Real-time Systems. In: Proc. RV 2002. ENTCS, vol. 70(4) (2002)

    Google Scholar 

20. Kristoffersen, K.J., Pedersen, C., Andersen, H.R.: Runtime Verification of Timed LTL using Disjunctive Normalized Equation Systems. In: Proc. RV 2003. ENTCS, vol. 89(2) (2003)

    Google Scholar 

21. Krichen, M., Tripakis, S.: Black-box Conformance Testing for Real-time Systems. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 109–126. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

22. Kurshan, R.: Computer-aided Verification of Coordinating Processes: The Automata-theoretic Approach. Princeton University Press, Princeton (1994)

    Google Scholar 

23. Mosterman, P.J.: An Overview of Hybrid Simulation Phenomena and their Support by Simulation Packages. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 165–177. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

24. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)

    Google Scholar 

25. Maler, O., Pnueli, A.: On Recognizable Timed Languages. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 348–362. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

26. Pnueli, A.: Verification of Reactive Systems. Lecture Notes, NYU (2003), http://cs.nyu.edu/courses/fall03/G22.3033-007/lecture4.pdf

27. Sokolsky, O., Viswanathan, M. (eds.): Runtime Verification RV 2003. ENTCS, vol. 89(2) (2003)

    Google Scholar 

28. Thati, P., Rosu, G.: Monitoring Algorithms for Metric Temporal Logic Specifications. In: Proc. of RV 2004 (2004)

    Google Scholar 

29. Tripakis, S.: Fault Diagnosis for Timed Automata. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 205–224. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

30. Vardi, M.Y., Wolper, P.: An Automata-theoretic Approach to Automatic Program Verification. In: Proc. LICS 1986, pp. 322–331. IEEE, Los Alamitos (1986)

    Google Scholar 

Download references