Advertisement

Specification and Verification of Distributed Real-Time Systems

  • M. J. Wieczorek
  • J. Vytopil
Conference paper

Abstract

What makes the design of distributed real-time systems hard and their validation expensive is their great complexity. Thereby, complexity comprises things such as the degree of dispersion and the diversity of the system components. Timing constraints and reliability aspects, beside many more topics, are as important as correct functionality but render more difficult. Therefore, suitable ways and means must be available from the very beginning of the development process to support the developer in his creative work to take adequate decisions at the various stages of system development. Formal methods are needed to gain the benefits from mathematically based techniques to specify systems.

Compositionality is now seen as an important property of formal specification languages and formal proof methods in the area of distributed real-time systems. But many such languages are derivatives or extensions of traditional sequential ones. In this paper we present a language supporting a property-oriented approach for the specification, construction, and verification of distributed real-time systems, called RDSL. Main constituents of RDSL are: First RSL, a three-sorted modal logic for the specification of system requirements, i. e. the required behaviour of a system. Second DSL, a combinator language for the specification of system design, i. e. the structure of a system designed to achieve a certain behaviour. Because referential transparency is one characteristic of DSL a compositional proof system can naturally be provided as third part of RDSL. The principle of separation of concerns is more rigourously incorporated in RDSL than in other approaches.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    S. Aggarwal, C. Courcoubetis, P. Wolper “Adding liveness properties to coupled finite state machines” in: ACMTOPLAS, 1990Google Scholar
  2. [2]
    H. Barringer, M. Fisher, D. Gabbay, G. Gough, R. Owens “MetateM: A Framework for Programming in Temporal Logic” University of Manchester, Department of Computer Science, Technical Report Series, UMCS-89-10-4Google Scholar
  3. [3]
    G. V. Bochmann “Specifications of a Simplified Transport Protocol Using Different Formal Description Techniques” in: Computer Networks and ISDN, 18, pp. 335–377, North-Holland, 1990CrossRefGoogle Scholar
  4. [4]
    H. B. Curry “Combinatory Logic”, vol. I North-Holland (Amsterdam), 1958Google Scholar
  5. [5]
    B. T. Hailpern “Verifying Concurrent Processes Using Temporal Logic” in: Lecture Notes in Computer Science, 129 Springer-Verlag Berlin Heidelberg, 1982zbMATHGoogle Scholar
  6. [6]
    J. Hooman, J. Widom “A Temporal-Logic Based Compositional Proof System for Real-Time Message Passing” in: Proceedings PARLE’ 89, Vol. II, pp. 424–441 Lecture Notes in Computer Science, 366, Springer-Verlag, 1989Google Scholar
  7. [7]
    J. Hooman “Compositional Verification of Distributed Real-Time Systems” in: Proceedings of the Workshop on “Real-Time Systems-Theory and Applications”, York (UK), September 1989Google Scholar
  8. [8]
    W. A. Howard “The Formulae-As-Types Notion of Construction” in: “To H B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism”, J. P. Seldin, J. R. Hindley (eds.), Academic Press, 1980Google Scholar
  9. [9]
    ISO “Information Technology / Vocabulary: Part 26-OSI Architecture” ISO/IEC DP 2382-26, 89-12-21, ref. no. ISO/IECJTC1/SC1 N 1178Google Scholar
  10. [10]
    W. Koole “Three-sorted RDSL” University of Nijmegen, Department of Informatics, Technical Report, 1990 (to appear)Google Scholar
  11. [11]
    R. Koymans “Specifying Message Passing and Time-Critical Systems with Temporal Logic” Ph. D. Thesis, Eindhoven University of Technology, 1989Google Scholar
  12. [12]
    L. Meertens “Constructing a calculus of programs” in: Proceedings of the International Conference on “Mathematics of program construction”, Lecture Notes in Computer Science 375, v. d. Snepscheut (ed.), Springer, 1989Google Scholar
  13. [13]
    A. S. Tanenbaum “Computer Networks” Prentice-Hall, Inc., Englewood-Cliffs, 1981Google Scholar
  14. [14]
    M. J. Wieczorek, J. Vytopil “Requirements and Design Specification Language” University of Nijmegen, Department of Informatics, Technical Report no. 90–6, June 1990Google Scholar
  15. [15]
    M. J. Wieczorek, J. Vytopil “A General Computational Model and its Application to Real-Time Systems” (in preparation)Google Scholar
  16. [16]
    M. J. Wieczorek, H. Wupper, J. Vytopil “Reliable Communication in Real-Time” University of Nijmegen, Department of Informatics, Technical Report (in preparation)Google Scholar

Copyright information

© Computational Mechanics Publications 1991

Authors and Affiliations

  • M. J. Wieczorek
    • 1
  • J. Vytopil
    • 1
  1. 1.Department of Informatics: Real-Time Systems, Faculty of Mathematics and InformaticsUniversity of NijmegenNijmegenThe Netherlands

Personalised recommendations