This book presents the application of formal methods in the development and verification of industrial software, particularly for safety-critical systems in the railway sector. It begins by discussing the transition from traditional development languages ​​and methods to formal methods, followed by an analysis of the practical application of the B-Method in the SAET-METEOR railway system. The book introduces model-based design using Simulink—covering modeling, code generation, verification, and validation—as well as the use of Simulink Design Verifier to prove global model properties. Additionally, it covers SCADE and its applications in safety-critical software development, the GATeL platform for SCADE model verification and validation, and ControlBuild, a control system development framework. Through industrial case studies, the book provides practical insights into the verification, validation, and deployment of formal methods for safety-critical software development.

Ngôn ngữ:	eng
Tác giả:	Boulanger, Jean-Louis
Thông tin nhan đề:	Formal methods: Industrial use from model to the code
Nhà xuất bản:	ISTE Ltd and John Wiley & Sons, Inc.
Loại hình:	Giáo trình sách, tham khảo / Bộ sưu tập: Công nghệ thông tin
Mô tả vật lý:	357p.
Năm xuất bản:	2012