Specification and Verification of Distributed Real-Time Systems
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.
Unable to display preview. Download preview PDF.
- S. Aggarwal, C. Courcoubetis, P. Wolper “Adding liveness properties to coupled finite state machines” in: ACMTOPLAS, 1990Google Scholar
- 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
- H. B. Curry “Combinatory Logic”, vol. I North-Holland (Amsterdam), 1958Google Scholar
- 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
- 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
- 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
- ISO “Information Technology / Vocabulary: Part 26-OSI Architecture” ISO/IEC DP 2382-26, 89-12-21, ref. no. ISO/IECJTC1/SC1 N 1178Google Scholar
- W. Koole “Three-sorted RDSL” University of Nijmegen, Department of Informatics, Technical Report, 1990 (to appear)Google Scholar
- R. Koymans “Specifying Message Passing and Time-Critical Systems with Temporal Logic” Ph. D. Thesis, Eindhoven University of Technology, 1989Google Scholar
- 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
- A. S. Tanenbaum “Computer Networks” Prentice-Hall, Inc., Englewood-Cliffs, 1981Google Scholar
- M. J. Wieczorek, J. Vytopil “Requirements and Design Specification Language” University of Nijmegen, Department of Informatics, Technical Report no. 90–6, June 1990Google Scholar
- M. J. Wieczorek, J. Vytopil “A General Computational Model and its Application to Real-Time Systems” (in preparation)Google Scholar
- M. J. Wieczorek, H. Wupper, J. Vytopil “Reliable Communication in Real-Time” University of Nijmegen, Department of Informatics, Technical Report (in preparation)Google Scholar