Formal methods and software engineering

Más información sobre el libro

The book covers a wide range of topics related to system development, verification, and testing in software and hardware engineering. It discusses a system development process using Event-B and the Rodin platform, addressing challenges in software certification and the integration of formal methods with system management. Key topics include the formal engineering of access control policies, a verification framework for agent knowledge, and the transition from model-based design to formal verification of adaptive embedded systems. The text also explores machine-assisted proof support, tools for verifying component integration in composite timed systems, and approaches for integrating specification-based review with testing to detect program errors. Additionally, it examines methods for reducing test sequence lengths, model checking with SAT-based characterization, and automating refinement checking in probabilistic system design. Practical applications of model checking, including analysis of bootloaders, are also highlighted. In hardware, the book presents denotational semantics for hardware compilation, automatic generation of verified concurrent hardware, and modeling of clock synchronization using hybrid automata. Finally, it addresses concurrency through symbolic execution in process algebra and formalization of virtual processors in thread algebra. An erratum is included regarding software certification challenges.