Recently, parallel and distributed systems are emerging as a highly promising candidate for implementing the next generation of high-performance embedded real-time systems which are adaptive to the rapidly changing environment. However, "fast" does not necessarily mean "real-time". Therefore, parallel and distributed systems must be fine-tuned before they can be trusted to monitor and control critical real.-time processes. These real-time monitoring and control systems must be able to compute correct results on time. Examples of these embedded system include the new generation of airplane avionics, the planned Space Station control software, high-performance network and telephone switching systems, medical monitoring instruments, multimedia tools, virtual reality systems, and robotic controllers.
More precisely, these real-time systems must respond to events in the rapidly changing external environment so that the results of the system's computation in each monitor-respond cycle are valid in safely operating the real-time system. In addition to functional correctness requirements, these systems must satisfy stringent performance requirements. Based on input sensor values, the real-time system must make decisions within bounded time to respond to the changing external environment, the results of missing a deadline may inflict serious damage to the real-time system, and may be harmful to human operators and users. The formal verification of real-time systems to ensure that they satisfy the specified integrity and timing requirements is thus essential if such systems are to be sued in safety-critical environments.
This tutorial introduces a formal framework and powerful techniques for the design and development of this class of systems, including the aspects of specification, design, analysis, implementation, verification, and validation. Programming in real-time/rule-based languages such as Ada, EQL, MRL, and OPS5 is described. Specification and verification tools such as Statechart, Modechart, and Estella are used to help design experimental parallel and distributed real-time systems.