Specification and analysis of resource-bound real-time systems

  • Richard Gerber
  • Insup Lee
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 600)


We describe a layered approach to the specification and verification of real-time systems. Application processes are specified in the CSR application language, which includes high-level language constructs such as timeouts, deadlines, periodic processes, interrupts and exception-handling. Then, a configuration schema is used to map the processes to system resources, and to specify the physical communication links between them. To analyze and execute the entire system, we automatically translate the result of the mapping into the CCSR process algebra. CCSR characterizes CSR's resource-based computation model by a prioritysensitive, operational semantics, which yields a set of equivalence-preserving proof rules. Using this proof system, we perform the algebraic verification of our original real-time system.


Real-time specification configuration verification proof systems process algebras programming languages 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    R. Alur, C. Courcoubetis, and D. Dill. Model-Checking for Real-Time Systems. In Proc. of IEEE Symposium on Logic in Computer Science, 1990.Google Scholar
  2. [2]
    R. Cleaveland and M. Hennessy. Priorities in Process Algebras. Information and Computation, 87:58–77, 1990.CrossRefGoogle Scholar
  3. [3]
    M.K. Franklin and A. Gabrielian. A Transformational Method for Verifying Safety Properties in Real-Time Systems. In Proc. IEEE Real-Time Systems Symposium, pages 112–123, December 1989.Google Scholar
  4. [4]
    R. Gerber. Communicating Shared Resrouces: A Model for Distributed Real-Time Systems. PhD thesis, Department of Computer and Information Science, University of Pennsylvania, 1991.Google Scholar
  5. [5]
    R. Gerber and I. Lee. Communicating Shared Resources: A Model for Distributed Real-Time Systems. In Proc. 10th IEEE Real-Time Systems Symposium, 1989.Google Scholar
  6. [6]
    R. Harper. Introduction to standard ML. Technical Report ECS-LFCS-86-14, Department of Computer Science, University of Edinburgh, The King's Buildings-Edinburgh EH9 3JZ-Scotland, 1986.Google Scholar
  7. [7]
    J. Hooman. Specification and Compositional Verification of Real-Time Systems. PhD thesis, Eindhoven University of Technology, 1991.Google Scholar
  8. [8]
    C. Huizing, R. Gerth, and W.P. de Roever. Full Abstraction of a Denotational Semantics for Real-time Concurrency. In Proc. 14th ACM Symposium on Principles of Programming Languages, pages 223–237, 1987.Google Scholar
  9. [9]
    M. Joseph and A. Goswami. What's ‘Real’ about Real-time Systems? In IEEE Real-Time Systems Symposium, 1988.Google Scholar
  10. [10]
    J.E. Coolahan Jr. and N. Roussopoulos. Timing Requirements for Time-Driven Systems Using Augmented Petri Nets. IEEE Trans. Software Eng., SE-9(5):603–616, September 1983.Google Scholar
  11. [11]
    I. Lee and V. Gehlot. Language Constructs for Distributed Real-Time Programming. In Proc. IEEE Real-Time Systems Symposium, 1985.Google Scholar
  12. [12]
    N. Lynch and M. Tuttle. An Introduction to Input/Output Automata. Technical Report MIT/LCS/TM-373, Laboratory for Computer Science, Massachusetts Institute of Technology, 1988.Google Scholar
  13. [13]
    R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
  14. [14]
    J.S. Qstroff and W.M. Wonham. Modelling, Specifying and Verifying Real-time Embedded Computer Systems. In Proc. IEEE Real-Time Systems Symposium, pages 124–132, December 1987.Google Scholar
  15. [15]
    G.M. Reed and A.W. Roscoe. Metric Spaces as Models for Real-Time Concurrency. In Proceedings of Math. Found. of Computer Science, LNCS 298, 1987.Google Scholar
  16. [16]
    A.C. Shaw. Reasoning About Time in Higher-Level Language Software. IEEE Transactions on Software Engineering, 15(7):875–889, 1989.CrossRefGoogle Scholar
  17. [17]
    W. Yi. Ccs + time = an interleaving model for real time systems. In ICALP, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Richard Gerber
    • 1
  • Insup Lee
    • 2
  1. 1.Dept. of Computer ScienceUniversity of MarylandCollege Park
  2. 2.Dept. of Computer and Info. ScienceUniversity of PennsylvaniaPhiladelphia

Personalised recommendations