Abstract State Machines, Alloy, B and Z (Paperback)

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.- AsmL-Based Concurrency Semantic Variations for Timed Use Case Maps.- Barun: A Scripting Language for CoreASM.- AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specifications.- An Executable Semantics of the SystemC UML Profile.- Alloy Papers.- Specifying Self-configurable Component-Based Systems with FracToy.- Trace Specifications in Alloy.- An Imperative Extension to Alloy.- Towards Formalizing Network Architectural Descriptions.- Lightweight Modeling of Java Virtual Machine Security Constraints.- Alloy+HotCore: 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 ClawZ.- 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 a 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.- ParAlloy: 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.