Marc Frappier & Uwe Glässer 
Abstract State Machines, Alloy, B and Z [PDF ebook] 
Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010, Proceedings

Invited Talks.- A Structure for Dependability Arguments.- Formal Probabilistic Analysis: A Higher-Order Logic Based Approach.- ASM Papers.- Synchronous Message Passing and Semaphores: An Equivalence Proof.- Asm L-Based Concurrency Semantic Variations for Timed Use Case Maps.- Bârun: A Scripting Language for Core ASM.- Asmeta SMV: A Way to Link High-Level ASM Models to Low-Level Nu SMV Specifications.- An Executable Semantics of the System C UML Profile.- Alloy Papers.- Specifying Self-configurable Component-Based Systems with Frac Toy.- Trace Specifications in Alloy.- An Imperative Extension to Alloy.- Towards Formalizing Network Architectural Descriptions.- Lightweight Modeling of Java Virtual Machine Security Constraints.- Alloy+Hot Core: A Fast Approximation to Unsat Core.- B Papers.- Supporting Reuse in Event B Development: Modularisation Approach.- Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance.- Applying the B Method for the Rigorous Development of Smart Card Applications.- Automatic Verification for a Class of Proof Obligations with SMT-Solvers.- A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking.- Development of a Synchronous Subset of AADL.- Matelas: A Predicate Calculus Common Formal Definition for Social Networking.- Structured Event-B Models and Proofs.- Refinement-Animation for Event-B — Towards a Method of Validation.- Reactivising Classical B.- Event-B Decomposition for Parallel Programs.- Z Papers.- Communication Systems in Claw Z.- Formalising and Validating RBAC-to-XACML Translation Using Lightweight Formal Methods.- Towards Formally Templated Relational Database Representations in Z.- Translating Z to Alloy.- ABZ Short Papers (Abstracts).- B-ASM: Specification of ASM à la B.- A Case for Using Data-Flow Analysis to Optimize Incremental Scope-Bounded Checking.- On the Modelling and Analysis of Amazon Web Services Access Policies.- Architecture as an Independent Variable for Aspect-Oriented Application Descriptions.- Par Alloy: Towards a Framework for Efficient Parallel Analysis of Alloy Models.- Introducing Specification-Based Data Structure Repair Using Alloy.- Secrecy UML Method for Model Transformations.- Improving Traceability between KAOS Requirements Models and B Specifications.- Code Synthesis for Timed Automata: A Comparison Using Case Study.- Towards Validation of Requirements Models.- A Proof Based Approach for Formal Verification of Transactional BPEL Web Services.- On an Extensible Rule-Based Prover for Event-B.- B Model Abstraction Combining Syntactic and Semantic Methods.- A Basis for Feature-Oriented Modelling in Event-B.- Using Event-B to Verify the Kmelia Components and Their Assemblies.- Starting B Specifications from Use Cases.- Integrating SMT-Solvers in Z and B Tools.- Formal Analysis in Model Management: Exploiting the Power of CZT.