Formal Analysis and Verification of Safety Interlock Systems

The ever-increasing reliance of society on computer systems has led to a need for highly reliable systems. There are a number of areas where computer systems perform critical functions and the development of such systems requires a higher level of attention than any other type of system. The appropriate approach in this situation is known as formal methods. Formal methods refer to the use of mathematical techniques for the specification, development and verification of software and hardware systems. The two main goals of this book are: (1) the design of mathematical models as a basis for the implementation of error-free software for the safety interlock system at iThemba LABS and (2) the comparison of formal method techniques that addresses the lack of much-needed empirical studies in the field of formal methods. This book is suitable for both undergraduate and postgraduate students who have already some experience with elementary discrete mathematics, logic, and finite state machines. A running example is provided to make this book ideal for students who want to learn about this important new field.