Formal methods

Más información sobre el libro

This book covers a range of topics in embedded systems design and formal verification. It includes discussions on interactive verification techniques, such as machine-checked proofs for electronic payment systems and the validation of medical guidelines. The text explores the certification of airport security regulations and the safety properties of aircraft landing protocols using theorem proving. It also addresses the validation of hypervisors and formal modeling of systems, including properties of behavioral model merging and the automatic translation of Circus to Java. The book delves into real-time systems, focusing on the modeling and validation of distributed embedded systems and modularized verification approaches. It shares industrial experiences in adopting formal methods, including case studies from railway signaling manufacturers and object-oriented development. Additionally, the text discusses specification refinement, programming languages, and formal reasoning about Java methods. It presents concepts like dynamic frames, type-safe data transformation, and feature algebra. The educational aspect emphasizes using domain-independent problems to introduce formal methods and formal modeling of communication protocols. Lastly, it covers model checking techniques, including strategies for symmetry reduction and monitoring distributed controllers, alongside insights into formal methods for security and their applicat