Integrated formal methods

Meer over het boek

This collection explores various aspects of verifying temporal properties and formal specifications in system designs. It covers customer-friendly foundations for precise scenarios, automated verification of security policies in mobile code, and the slicing of concurrent real-time system specifications. The text delves into methodologies like Slotted-Circus and addresses challenges such as bug hunting with false negatives. It discusses deriving behavioral specifications from class models and the inheritance of laws for processes with states. Additionally, it presents probabilistic timed behavior trees and guides the correction of parameterized specifications. The work includes proving linearizability via non-atomic refinement and the verification of CSP-OZ-DC specifications with complex data types and timing parameters. It also models and verifies protocols like LMAC for wireless sensor networks and explores qualitative probabilistic modeling in Event-B. Other topics include smart card application verification using ASM, the verification of probabilistic properties in HOL, and the semantics of web services. The collection emphasizes integrated approaches, such as static analysis for Linux device driver verification and the unification of theories of objects, while also addressing the co-simulation of distributed embedded real-time control systems.