Real-time systems: A survey of approaches to formal specification and verification

1. Bellettini, C., Felder, M., Pezzè, M.: MERLOT: A tool for analysis of real-time specifications. Proceedings of the 7th International Workshop on Software Specifications and Design, Los Angeles, California, 1993. (to appear)

   Google Scholar 

2. Clarke, C., Emerson, E., Sistla, S.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM-Transactions on Programming Languages and Systems, Vol. 8, No. 2, April 1986.

   Google Scholar 

3. Coen, A., Morzenti, A., Sciuto, D.: Specification and verification of hardware systems using the temporal logic language TRIO. In Computer hardware description languages and their application, Borrione, D. and Waxman, R., IFIP, North-Holland, Marseille, France, April 1991, pp. 43–62.

   Google Scholar 

4. Dillon, L.K., Avrunin, G.S., Wileden, J.C.: Constrained expressions: Toward broad applicability of analysis methods for distributed software systems. ACM-Transactions on Programming Languages and Systems, Vol. 10, No. 3, pp. 374–402, July 1988.

   Google Scholar 

5. Felder, M., Ghezzi, C., Pezzè M.: Analyzing refinements of state based specifications: the case of TB nets. Proceedings of International Symposium on Software Testing and Analysis 1993, Cambridge, Massachusetts. (to appear)

   Google Scholar 

6. Felder, M., Mandrioli, D., Morzenti, A.: Proving properties of real-time systems through logical Specifications and Petri Nets Models. IEEE-Transactions on Software Engineering (to appear). Also in Tech-Report 91-072, Dip. di Elettronica-Politecnico di Milano, December 1991.

   Google Scholar 

7. Felder, M., Morzenti, A.: Specification testing for real-time systems by history checking in TRIO. Proceedings of the 14th International Conference on Software Engineering, Melbourne, Australia, May 1992.

   Google Scholar 

8. Ghezzi, C., Kemmerer, R.A.: ASTRAL: An assertion language for specifying real-time systems. Proceedings of the 3rd European Software Engineering Conference, Milano, Italy, October 1991.

   Google Scholar 

9. Ghezzi, C., Kemmerer, R.A.: Executing formal specifications: the ASTRAL to TRIO translation approach. TAV'91, Symposium on Testing, Analysis and Verification, Victoria, Canada, October 1991.

   Google Scholar 

10. Ghezzi, C., Mandrioli, D., Morasca, S., Pezzè, M.: A general way to put time in Petri nets. Proceedings of the 4th International Workshop on Software Specifications and Design, Monterey, California, April 3–4, 1987.

    Google Scholar 

11. Ghezzi, C., Mandrioli, D., Morasca, S., Pezzè, M.: A unified high-level Petri net formalism for time-critical systems. IEEE Transactions on Software Engineering, Vol. 17, No. 2, February 1991.

    Google Scholar 

12. Ghezzi, C., Mandrioli, D., Morasca, S., Pezzè, M.: Symbolic execution of concurrent programs using Petri nets. Computer Languages, April 1989.

    Google Scholar 

13. Ghezzi, C., Mandrioli, D., Morzenti, A.: TRIO: A logic language for executable specifications of real-time systems. Journal of Systems and Software, June 1990.

    Google Scholar 

14. Ghezzi, C., Morasca, S., Pezzè, M.: Timing analysis of time basic nets”. submitted for publication

    Google Scholar 

15. Gomaa, H.: Software development of real-time systems. Communications of the ACM, Vol. 29, No. 7, July 1986.

    Google Scholar 

16. Hatley, D.J., Pirbai, I.A.: Strategies for Real-Time System Specification. Dorset House, 1988.

    Google Scholar 

17. Henzinger, T., Manna, Z., Pnueli, A.: Temporal proof methodologies for real time systems. Proceedings of the 18th ACM Symposium on Principles of Programming Languages, pp. 353–366, 1991.

    Google Scholar 

18. Howden, W.E.: Functional Program Testing & Analysis. Mc Graw Hill, 1987.

    Google Scholar 

19. Kemmerer, R.A.: Testing software specifications to detect design errors. IEEE Transactions on Software Engineering, Vol. 11, No. 1, January 1985.

    Google Scholar 

20. Koymans, R.: Specifying Message Passing and Time-Critical Systems with Temporal Logic. PhD Thesis, Eindhoven University of Technology, 1989.

    Google Scholar 

21. Mandrioli, D., Morzenti, A. and Morasca, S.: Functional test case generation for real-time sytems. Proceedings of 3rd International Working Conference on Dependable Computing for Critical Applications, IFIP, 1992 pp.13–26.

    Google Scholar 

22. Mendelson, E.: Introduction to mathematical logic. Van Nostrand Reinold Company, New York, 1963.

    Google Scholar 

23. Morasca, S. and Pezzè, M.: Validation of concurrent Ada programs using symbolic execution. Proceedings of the 2nd European Software Engineering Conference, LNCS 387, pages 469–486. Springer-Verlag, 1989.

    Google Scholar 

24. Morzenti, A., Mandrioli, D., Ghezzi, C.: A model parametric real-time logic. ACM Transactions on Programming Languages and Systems, Vol. 14, No. 4, pp. 521–573, October, 1982.

    Google Scholar 

25. Morzenti, A.: The Specification of Real-Time Systems: Proposal of a Logic Formalism. PhD Thesis, Dipartimento di Elettronica, Politecnico di Milano, 1989.

    Google Scholar 

26. Morzenti, A., San Pietro, P.: An object oriented logic language for modular system specification. Proceedings of the European Conference on Object Oriented Programming '91, LNCS 512, Springer Verlag, July 1991.

    Google Scholar 

27. Nagl, M.: A tutorial and bibliography survey on graph grammars. LNCS 166, Springer Verlag, 1985.

    Google Scholar 

28. Ostrof, J.: Temporal Logic For Real-Time Systems. Research Studies Press LTD., Advanced Software Development Series, Taunton, Somerset, England, 1989.

    Google Scholar 

29. Pezzè, M. and Ghezzi, C.: Cabernet: a customizable environment for the specification and analysis of real-time systems. submitted for publication, 1993.

    Google Scholar 

30. Quirk, W.J.: Verification and Validation of Real-Time Software. Springer Verlag, Berlin, 1985.

    Google Scholar 

31. Reisig, W.: Petri Nets: an Introduction. Springer Verlag, 1985.

    Google Scholar 

32. Smullian, R.M.: First. Order Logic. Springer Verlag, Berlin, 1968.

    Google Scholar 

33. Taylor, R.: A general-purpose algorithm for analyzing concurrent programs. Communications of the ACM, Vol. 26, No.5, pp. 362–376, May 1983.

    Google Scholar 

Download references