Compositional Verification of Concurrent and Real-Time Systems

With the rapid growth of networking and high-computing power, the demand for large-scale and complex software systems has increased dramatically. Since many of the software systems support or supplant human control of safety-critical systems (such as those found in flight control, space shuttle control, aircraft avionics, robotics, patient monitoring devices and nuclear power plants), failure of such systems could have disastrous effects. It is essential, therefore, that software used for safety-critical systems preserves high assurance properties. This text introduces important modelling and formal verification techniques for verifying the reliability and correctness of high-assurance software systems. It focuses on the efficient analysis of large-scale systems based on the concept of "compositional verification" of modules.