Formal Methods and Software Engineering: 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007. Proceedings

J. -R. Abrial (auth.), Michael Butler, Michael G. Hinchey, María M. Larrondo-Petrie (eds.)3540766480, 9783540766483

This book constitutes the refereed proceedings of the 9th International Conference on Formal Engineering Methods, ICFEM 2007, held in Boca Raton, Florida, USA, November 14-15, 2007.

The 19 revised full papers together with two invited talks presented were carefully reviewed and selected from 38 submissions. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on security and knowledge, embedded systems, testing, automated analysis, hardware and concurrency.

---

Table of contents :
Front Matter….Pages –
A System Development Process with Event-B and the Rodin Platform….Pages 1-3
Challenges in Software Certification….Pages 4-18
Integrating Formal Methods with System Management….Pages 19-36
Formal Engineering of XACML Access Control Policies in VDM++….Pages 37-56
A Verification Framework for Agent Knowledge….Pages 57-75
From Model-Based Design to Formal Verification of Adaptive Embedded Systems….Pages 76-95
Machine-Assisted Proof Support for Validation Beyond Simulink….Pages 96-115
VeSTA: A Tool to Verify the Correct Integration of a Component in a Composite Timed System….Pages 116-135
Integrating Specification-Based Review and Testing for Detecting Errors in Programs….Pages 136-150
Testing for Refinement in CSP….Pages 151-170
Reducing Test Sequence Length Using Invertible Sequences….Pages 171-190
Model Checking with SAT-Based Characterization of ACTL Formulas….Pages 191-211
Automating Refinement Checking in Probabilistic System Design….Pages 212-231
Model Checking in Practice: Analysis of Generic Bootloader Using SPIN….Pages 232-245
Model Checking Propositional Projection Temporal Logic Based on SPIN….Pages 246-265
A Denotational Semantics for Handel-C Hardware Compilation….Pages 266-285
Automatic Generation of Verified Concurrent Hardware….Pages 286-306
Modeling and Verification of Master/Slave Clock Synchronization Using Hybrid Automata and Model-Checking….Pages 307-326
Efficient Symbolic Execution of Large Quantifications in a Process Algebra….Pages 327-344
Formalizing SANE Virtual Processor in Thread Algebra….Pages 345-365
Calculating and Composing Progress Properties in Terms of the Leads-to Relation….Pages 366-386
Erratum to: Challenges in Software Certification….Pages E1-E1
Back Matter….Pages –