Paradigms for the specification, design, and verification of real-time distributed systems
Rudrapatna K. Shyamasundar, Leo Yuhsiang Liu · 1989
Due to the catastrophic consequences of failures in real-time systems, the issues of safety and reliability are extremely important for the design of such systems. However, typical real-time systems are large and complex; hence, they are difficult--if not impossible--for a programmer or a team to mentally comprehend. Thus, to facilitate the specification and verification of large real-time systems, it is essential to employ compositional methodologies using realistic models for real-time concurrency. Despite the proliferation of real-time systems surrounding us, the programming abstractions provided by existing languages do not cope with the increase in complexity and sophistication of these systems. In this thesis, we propose several paradigms for the specification, design, and verification of real-time distributed systems. Our goal is to provide tools to bridge the gap between specification and realization of programs. We employ communication histories to capture the behavior of real-time programs using the maximal parallelism model. We first show how to characterize and analyze programs in synchronous real-time languages through static analysis. The analysis allow us to study many interesting safety, liveness, and timing properties. We also give algorithms to detect deadlock, distributed termination, and various timing errors. The analysis has made an emphasis on compositionality as well as on practicability. The approach can be automated and applied to other languages. We then propose a real-time design language, RT-CDL, for the design of reliable reactive systems. The language is formally defined by an operational semantics. It is expressive enough for users to specify various timing constraints and to write responsive programs. Furthermore, the language features can be adapted easily for various exception handling purposes. Our investigation reveals that the features provided by RT-CDL are indeed suitable for a spectrum of real-time applications. The approach is compositional and hence provides a firm base for modular/hierarchical development of real-time programs.