Deductive verification of real-time systems using STeP

1. J. Armstrong and L. Barroca. Specification and verification of reactive system behaviour: The railroad crossing example. Real-Time Systems, 10:143–178, 1996.

   Article  Google Scholar 

2. R. Alur and D.L. Dill. A theory of timed automata. Theor. Comp. Sci., 126:183–235, 1994.

   Article  MathSciNet  MATH  Google Scholar 

3. M. Abadi and L. Lamport. An old-fashioned recipe for real time. In Proceedings of the REX Workshop “Real-Time: Theory in Practice”, volume 600 of LNCS, pages 1–27. Springer-Verlag, 1992.

   Google Scholar 

4. N.S. Bjørner, A. Browne, E. Chang, M. Colón, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover, User's Manual. Technical Report STAN-CS-TR-95-1562, Computer Science Department, Stanford University, November 1995.

   Google Scholar 

5. N.S. Bjørner, A. Browne, E. Chang, M. Colón, A. Kapur, Z. Manna, H.B. Sipma, and T.E. Uribe. STeP: Deductive-algorithmic verification of reactive and real-time systems. In Proc. 8 ^th Intl. Conference on Computer Aided Verification, volume 1102 of LNCS, pages 415–418. Springer-Verlag, July 1996.

   Google Scholar 

6. N.S. Bjørner, A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. Theor. Comp. Sci., 173(1):49–87, February 1997.

   Article  MathSciNet  MATH  Google Scholar 

7. J. Bengtsson, K.G. Larson, F. Larsson, P. Pettersson, and W. Yi. Uppaal — a Tool Suite for Automatic Verification of Real-Time Systems. In Proc. of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems, volume 1066 of LNCS, pages 232–243, 1995.

   Google Scholar 

8. S. Bensalem, Y. Lakhnech, and H. Saidi. Powerful Techniques for the Automatic Generation of Invariants. In R. Alur and T. Henzinger, editors, Proc. 8 ^th Intl. Conference on Computer Aided Verification, volume 1102 of LNCS, pages 323–335. Springer-Verlag, 1996.

   Google Scholar 

9. A. Browne, Z. Manna, and H.B. Sipma. Generalized temporal verification diagrams. In 15th Conference on the Foundations of Software Technology and Theoretical Computer Science, volume 1026 of LNCS, pages 484–498, 1995.

   Google Scholar 

10. N.S. Bjørner, M.E. Stickel, and T.E. Uribe. A practical combination of first-order reasoning and decision procedures. In 14th Intl. Conference on Automated Deduction, LNCS. Springer-Verlag, July 1997. To appear.

    Google Scholar 

11. S. Campos and E. Clarke. Real-time symbolic model checking for discrete time models. In Theories and Experiences for Real-Time System Development., AMAST. World Scientific Publishing Company, 1995.

    Google Scholar 

12. E.S. Chang. Compositional Verification of Reactive and Real-Time Systems. PhD thesis, Computer Science Department, Stanford University, Stanford, California, 1993. Tech. Report STAN-CS-TR-94-1522.

    Google Scholar 

13. Z. Chaochen, C.A.R Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, 1992.

    Article  MathSciNet  MATH  Google Scholar 

14. E.S. Chang, Z. Manna, and A. Pnueli. Compositional verification of real-time systems. In Proc. 9th IEEE Symp. Logic in Comp. Sci., pages 458–465. IEEE Computer Society Press, 1994.

    Google Scholar 

15. C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool Kronos. In Hybrid Systems III, volume 1066 of LNCS, pages 208–219. Springer-Verlag, 1996.

    Google Scholar 

16. C. Daws and S. Yovine. Verification of multirate timed automata with KRONOS: two examples. Technical Report Spectre-95-06, VERIMAG, April 1995.

    Google Scholar 

17. E.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 995–1072. Elsevier Science Publishers (North-Holland), 1990.

    Google Scholar 

18. T.A. Henzinger and P.-H. Ho. HyTech: The Cornell hybrid technology tool. In Hybrid Systems II, volume 999 of LNCS, pages 265–293. Springer-Verlag, 1995.

    Google Scholar 

19. C. Heitmeyer, R. Jeffords, and B. Labaw. A benchmark for comparing different approaches for specifying and verifying real-time systems. In Proc. Tenth Intl. Workshop on Real-Time Operating Systems and Software, 1993.

    Google Scholar 

20. T.A. Henzinger and P. Kopke. Verification methods for the divergent runs of clock systems. In FTRTFT 94: Formal Techniques in Real-time and Fault-tolerant Systems, volume 863 of LNCS, pages 351–372. Springer-Verlag, 1994.

    Google Scholar 

21. C. Heitmeyer and N. Lynch. The generalized railroad crossing: A case study in formal verification of real-time systems. In Proc. ICCC Real-Time Systems Symposium, pages 120–131. IEEE Press, 1994.

    Google Scholar 

22. T.A. Henzinger, Z. Manna, and A. Pnueli. Temporal proof methodologies for timed transition systems. Inf. and Comp., 112(2):273–337, August 1994.

    Article  MathSciNet  MATH  Google Scholar 

23. Y. Kesten, Z. Manna, and A. Pnueli. Verifying clocked transition systems. In Hybrid Systems III, volume 1066 of LNCS, pages 13–40. Springer-Verlag, 1996.

    Google Scholar 

24. L. Lamport. Proving possibility properties. Technical Report 137, Digital Equipment Corporation, Systems Research Center, July 1995.

    Google Scholar 

25. O. Maler, Z. Manna, and A. Pnueli. From timed to hybrid systems. In Proceedings of the REX Workshop “Real-Time: Theory in Practice”, volume 600 of LNCS, pages 447–484. Springer-Verlag, 1992.

    Google Scholar 

26. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.

    MATH  Google Scholar 

27. Z. Manna and A. Pnueli. Temporal verification diagrams. In Proc. Int. Symp. on Theoretical Aspects of Computer Software, volume 789 of LNCS, pages 726–765. Springer-Verlag, 1994.

    Google Scholar 

28. Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.

    Book  MATH  Google Scholar 

29. Z. Manna and A. Pnueli. Clocked transition systems. Technical Report STAN-CS-TR-96-1566, Computer Science Department, Stanford University, April 1996.

    Google Scholar 

30. J.S. Ostroff. Temporal Logic of Real-Time Systems. Advanced Software Development Series. Research Studies Press (John Wiley & Sons), Taunton, England, 1990.

    Google Scholar 

31. J.S. Ostroff. A visual toolset for the design of real-time discrete event systems. IEEE Trans. on Control Systems Technology, May 1997. To appear.

    Google Scholar 

32. J.X. Su, D.L. Dill, and C.W. Barrett. Automatic generation of invariants for processor verification. In Formal Methods in Computer-Aided Design, volume 1166 of LNCS, pages 377–388. Springer-Verlag, November 1996.

    Google Scholar 

33. N. Shankar. Verification of real-time systems using PVS. In Proc. 5 ^th Intl. Conference on Computer Aided Verification, volume 697 of LNCS, pages 280–291. Springer-Verlag, June 1993.

    Google Scholar 

34. J.U. Skakkebæk. A Verification Assistant for a Real-Time Logic. PhD thesis, Technical University of Denmark, 1994.

    Google Scholar 

35. L. Urbina. The generalized railroad crossing: Its symbolic analysis in CLP(43-01). In Principles and Practice of Constraint Programming, volume 1118 of LNCS, pages 564–567, August 1996.

    Google Scholar 

Download references