Abstract State Machines, Alloy, B and Z: Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010, Proceedings

Front Matter....Pages -
A Structure for Dependability Arguments....Pages 1-1
Formal Probabilistic Analysis: A Higher-Order Logic Based Approach....Pages 2-19
Synchronous Message Passing and Semaphores: An Equivalence Proof....Pages 20-33
AsmL-Based Concurrency Semantic Variations for Timed Use Case Maps....Pages 34-46
Bârun: A Scripting Language for CoreASM ....Pages 47-60
AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specifications....Pages 61-74
An Executable Semantics of the SystemC UML Profile....Pages 75-90
Specifying Self-configurable Component-Based Systems with FracToy....Pages 91-104
Trace Specifications in Alloy....Pages 105-117
An Imperative Extension to Alloy....Pages 118-131
Towards Formalizing Network Architectural Descriptions....Pages 132-145
Lightweight Modeling of Java Virtual Machine Security Constraints....Pages 146-159
Alloy+HotCore: A Fast Approximation to Unsat Core....Pages 160-173
Supporting Reuse in Event B Development: Modularisation Approach....Pages 174-188
Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance....Pages 189-202
Applying the B Method for the Rigorous Development of Smart Card Applications....Pages 203-216
Automatic Verification for a Class of Proof Obligations with SMT-Solvers....Pages 217-230
A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking....Pages 231-244
Development of a Synchronous Subset of AADL....Pages 245-258
Matelas: A Predicate Calculus Common Formal Definition for Social Networking....Pages 259-272
Structured Event-B Models and Proofs....Pages 273-286
Refinement-Animation for Event-B — Towards a Method of Validation....Pages 287-301
Reactivising Classical B....Pages 302-318
Event-B Decomposition for Parallel Programs....Pages 319-333
Communication Systems in ClawZ....Pages 334-348
Formalising and Validating RBAC-to-XACML Translation Using Lightweight Formal Methods....Pages 349-362
Towards Formally Templated Relational Database Representations in Z....Pages 363-376
Translating Z to Alloy....Pages 377-390
B-ASM: Specification of ASM à la B....Pages 391-391
A Case for Using Data-Flow Analysis to Optimize Incremental Scope-Bounded Checking....Pages 392-393
On the Modelling and Analysis of Amazon Web Services Access Policies....Pages 394-394
Architecture as an Independent Variable for Aspect-Oriented Application Descriptions....Pages 395-395
ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy Models....Pages 396-397
Introducing Specification-Based Data Structure Repair Using Alloy....Pages 398-399
Secrecy UML Method for Model Transformations....Pages 400-400
Improving Traceability between KAOS Requirements Models and B Specifications....Pages 401-402
Code Synthesis for Timed Automata: A Comparison Using Case Study....Pages 403-403
Towards Validation of Requirements Models....Pages 404-404
A Proof Based Approach for Formal Verification of Transactional BPEL Web Services....Pages 405-406
On an Extensible Rule-Based Prover for Event-B....Pages 407-407
B Model Abstraction Combining Syntactic and Semantic Methods....Pages 408-408
A Basis for Feature-Oriented Modelling in Event-B....Pages 409-409
Using Event-B to Verify the Kmelia Components and Their Assemblies....Pages 410-410
Starting B Specifications from Use Cases....Pages 411-411
Integrating SMT-Solvers in Z and B Tools....Pages 412-413
Formal Analysis in Model Management: Exploiting the Power of CZT....Pages 414-414
Back Matter....Pages -