This book presents real-world examples of formal techniques in an industrial context. It covers formal methods such as SCADE, the B-Method, ControlBuild and Matelo, in various fields such as railways, aeronautics, and the automotive industry. The purpose of this book is to present a summary of experience on the use of “formal methods” (such as […]
This book presents real-world examples of formal techniques in an industrial context. It covers formal methods such as SCADE, the B-Method, ControlBuild and Matelo, in various fields such as railways, aeronautics, and the automotive industry. The purpose of this book is to present a summary of experience on the use of “formal methods” (such as proof and model-checking) in industrial examples of complex systems, based on the experience of people currently involved in the creation and evaluation of safety critical system software. The involvement of people from within the industry allows the authors to avoid the usual confidentiality problems which can arise and thus enables them to supply new useful information (photos, architecture plans, real examples, etc.).
The authors cover the following topics: the use of SCADE, constraint solving in B, validation of Petri Nets-based automated rail safety, Mitsubichi, Clearsy, the B-method, B extended to flight, which is sufficient to prove avionics software, data validation with ProB, proof with new GNATprove tools.