+612 9045 4394
Abstract State Machines, Alloy, B and Z : Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010, Proceedings - Marc Frappier

Abstract State Machines, Alloy, B and Z

Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010, Proceedings

By: Marc Frappier (Editor), Uwe Glasser (Editor), Sarfraz Khurshid (Editor), Regine Laleau (Editor), Steve Reeves (Editor)

Paperback Published: 2nd March 2010
ISBN: 9783642118104
Number Of Pages: 416

Share This Book:


or 4 easy payments of $39.60 with Learn more
Ships in 7 to 10 business days

ABZ 2010 was held in the beautiful natural setting of Orford in the Eastern Townships of Qu ebec, during February22-25,2010, midwaythroughthe Ca- dian winter and the 21st Winter Olympics, bringing participants from all over the world to brave this rigorous climate. ABZcoversrecentadvancesinfourequallyrigorousmethodsforsoftwareand hardware development: Abstract State Machines (ASM), Alloy, B and Z. They shareacommonconceptualframework, centeredaroundthe notionsofstateand operation, andpromotemathematicalprecisioninthemodeling, veri?cation, and construction of highly dependable systems. These methods have continuously matured over the past decade, reaching a stage where they have been successfully integrated into industrial practice in various areas like trains, automobiles, aerospace, smart cards, virtual machines, and business processes. Their development is in?uenced by both research and practice, which mutually nurture each other. ABZ has both a long and a short history. With the aim of stimulating cro- fertilization between these four methods, it has merged their individual conf- ence and workshopseries which started in 1986 for Z, 1994 for ASM, 1996 for B, and 2006 for Alloy. The ?rst ABZ conference was held in London in 2008; ABZ 2010 is the second edition. The conference remains organized as four separate Program Committees.

Invited Talks
A Structure for Dependability Arguments (Abstract)p. 1
Formal Probabilistic Analysis: A Higher-Order Logic Based Approachp. 2
ASM Papers
Synchronous Message Passing and Semaphores: An Equivalence Proofp. 20
AsmL-Based Concurrency Semantic Variations for Timed Use Case Mapsp. 34
Bârun: A Scripting Language for CoreASMp. 47
AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specificationsp. 61
An Executable Semantics of the SystemC UML Profilep. 75
Alloy Papers
Specifying Self-configurable Component-Based Systems with FracToyp. 91
Trace Specifications in Alloyp. 105
An Imperative Extension to Alloyp. 118
Towards Formalizing Network Architectural Descriptionsp. 132
Lightweight Modeling of Java Virtual Machine Security Constraintsp. 146
Alloy+HotCore: A Fast Approximation to Unsat Corep. 160
B Papers
Supporting Reuse in Event B Development: Modularisation Approachp. 174
Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidancep. 189
Applying the B Method for the Rigorous Development of Smart Card Applicationsp. 203
Automatic Verification for a Class of Proof Obligations with SMT-Solversp. 217
A Refinement-Based Correctness Proof of Symmetry Reduced Model Checkingp. 231
Development of a Synchronous Subset of AADLp. 245
Matelas: A Predicate Calculus Common Formal Definition for Social Networkingp. 259
Structured Event-B Models and Proofsp. 273
Refinement-Animation for Event-B — Towards a Method of Validationp. 287
Reactivising Classical Bp. 302
Event-B Decomposition for Parallel Programsp. 319
Z Papers
Communication Systems in ClawZp. 334
Formalising and Validating RBAC-to-XACML Translation Using Lightweight Formal Methodsp. 349
Towards Formally Templated Relational Database Representations in Zp. 363
Translating Z to Alloyp. 377
ABZ Short Papers (Abstracts)
B-ASM: Specification of ASM á la Bp. 391
A Case for Using Data-Flow Analysis to Optimize Incremental Scope-Bounded Checkingp. 392
On the Modelling and Analysis of Amazon Web Services Access Policiesp. 394
Architecture as an Independent Variable for Aspect-Oriented Application Descriptionsp. 395
ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy Modelsp. 396
Introducing Specification-Based Data Structure Repair Using Alloyp. 398
Secrecy UML Method for Model Transformationsp. 400
Improving Traceability between KAOS Requirements Models and B Specificationsp. 401
Code Synthesis for Timed Automata: A Comparison Using Case Studyp. 403
Towards Validation of Requirements Modelsp. 404
A Proof Based Approach for Formal Verification of Transactional BPEL Web Servicesp. 405
On an Extensible Rule-Based Prover for Event-Bp. 407
B Model Abstraction Combining Syntactic and Semantic Methodsp. 408
A Basis for Feature-Oriented Modelling in Event-Bp. 409
Using Event-B to Verify the Kmelia Components and Their Assembliesp. 410
Starting B Specifications from Use Casesp. 411
Integrating SMT-Solvers in Z and B Toolsp. 412
Formal Analysis in Model Management: Exploiting the Power of CZTp. 414
Author Indexp. 415
Table of Contents provided by Ingram. All Rights Reserved.

ISBN: 9783642118104
ISBN-10: 3642118100
Series: Lecture Notes in Computer Science
Audience: General
Format: Paperback
Language: English
Number Of Pages: 416
Published: 2nd March 2010
Publisher: Springer-Verlag Berlin and Heidelberg Gmbh & Co. Kg
Country of Publication: DE
Dimensions (cm): 23.11 x 15.24  x 2.29
Weight (kg): 0.66