Temporal verification of reactive systems

This book focuses on the verification of reactive systems, which continuously interact with their environment rather than compute a final value upon termination. Such systems include concurrent programs, embedded and process control programs, and operating systems, all of which present unique challenges for reliable construction. Examples include air traffic control systems, train control programs, and processes like nuclear reactors. As computers are increasingly used in safety-critical applications where failures can have severe consequences, ensuring correctness becomes essential. This necessity has led to the development of formal verification techniques that enhance user and designer confidence in meeting specifications. The approach outlined in this book utilizes temporal logic to specify the properties of reactive systems and establishes a comprehensive verification methodology for demonstrating that a system adheres to its temporal specifications. Reactive programs must be defined by their ongoing behavior, and temporal logic serves as an expressive language for this purpose. The framework for specifying and verifying the temporal properties of reactive systems comprises four components, with the chosen computational model being a Fair Transition System (FTS) to effectively describe the behavior of these systems.