Abstract State Machines, Alloy, B and Z: Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010, Proceedings
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.
1114171188
Abstract State Machines, Alloy, B and Z: Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010, Proceedings
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.
54.99 In Stock
Abstract State Machines, Alloy, B and Z: Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010, Proceedings

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

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

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

Paperback(2010)

$54.99 
  • SHIP THIS ITEM
    In stock. Ships in 1-2 days.
  • PICK UP IN STORE

    Your local store may have stock of this item.

Related collections and offers


Overview

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.

Product Details

ISBN-13: 9783642118104
Publisher: Springer Berlin Heidelberg
Publication date: 04/08/2010
Series: Lecture Notes in Computer Science , #5977
Edition description: 2010
Pages: 416
Product dimensions: 5.90(w) x 9.20(h) x 0.80(d)

Table of Contents

Invited Talks

A Structure for Dependability Arguments (Abstract) Daniel Jackson Eunsuk Kang 1

Formal Probabilistic Analysis: A Higher-Order Logic Based Approach Osman Hasan Sofiéne Tahar 2

ASM Papers

Synchronous Message Passing and Semaphores: An Equivalence Proof Iain Craig Egon Börger 20

AsmL-Based Concurrency Semantic Variations for Timed Use Case Maps Jameleddine Hassine 34

Bârun: A Scripting Language for CoreASM Michael Altenhofen Roozbeh Farahbod 47

AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specifications Paolo Arcaini Angelo Gargantini Elvinia Riccobene 61

An Executable Semantics of the SystemC UML Profile Elvinia Riccobene Patrizia Scandurra 75

Alloy Papers

Specifying Self-configurable Component-Based Systems with FracToy Alban Tiberghien Philippe Merle Lionel Seinturier 91

Trace Specifications in Alloy Jeremy L. Jacob 105

An Imperative Extension to Alloy Joseph P. Near Daniel Jackson 118

Towards Formalizing Network Architectural Descriptions Joud Khoury Chaouki T. Abdallah Gregory L. Heileman 132

Lightweight Modeling of Java Virtual Machine Security Constraints Mark C. Reynolds 146

Alloy+HotCore: A Fast Approximation to Unsat Core Nicolás D'Ippolito Marcelo F. Frias Juan P. Galeotti Esteban Lamarotti Sergio Mera 160

B Papers

Supporting Reuse in Event B Development: Modularisation Approach Alexei Iliasov Elena Troubitsyna Linas Laibinis Alexander Romanovsky Kimmo Varpaaniemi Dubravka Ilic Timo Latvala 174

Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance Andrew Ireland Gudmund Grov Michael Butler 189

Applying the B Method for the Rigorous Development of Smart Card Applications Bruno Gomes David Déharbe Anamaria Moreira Katia Moraes 203

Automatic Verification for a Class of Proof Obligations with SMT-Solvers David Déharbe 217

A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking Edd Turner Michael Butler Michael Leuschel 231

Development of a Synchronous Subset of AADL Mamoun Filali-Amine Julia Lawall 245

Matelas: A Predicate Calculus Common Formal Definition for Social Networking Nestor Catano Camilo Rueda 259

Structured Event-B Models and Proofs Stefan Hallerstede 273

Refinement-Animation for Event-B — Towards a Method of Validation Stefan Hallerstede Michael Leuschel Daniel Plagge 287

Reactivising Classical B Steve Dunne Frank Zeyda 302

Event-B Decomposition for Parallel Programs Thai Son Hoang Jean-Raymond Abrial 319

Z Papers

Communication Systems in ClawZ Michael Vernon Frank Zeyda Ana Cavalcanti 334

Formalising and Validating RBAC-to-XACML Translation Using Lightweight Formal Methods Mark Slaymaker David Power Andrew Simpson 349

Towards Formally Templated Relational Database Representations in Z Nicolas Wu Andrew Simpson 363

Translating Z to Alloy Petra Malik Lindsay Groves Clare Lenihan 377

ABZ Short Papers (Abstracts)

B-ASM: Specification of ASM á la B David Michel Frédéric Gervais Pierre Valarcher 391

A Case for Using Data-Flow Analysis to Optimize Incremental Scope-Bounded Checking Danhua Shao Divya Gopinath Sarfraz Khurshid Dewayne E. Perry 392

On the Modelling and Analysis of Amazon Web Services Access Policies David Power Mark Slaymaker Andrew Simpson 394

Architecture as an Independent Variable for Aspect-Oriented Application Descriptions Hamid Bagheri Kevin Sullivan 395

ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy Models Nicolás Rosner Juan P. Galeotti Carlos G. Lopez Pombo Marcelo F. Frias 396

Introducing Specification-Based Data Structure Repair Using Alloy Razieh Nokhbeh Zaeem Sarfraz Khurshid 398

Secrecy UML Method for Model Transformations Waël Hassan Nadera Slimani Kamel Adi Luigi Logrippo 400

Improving Traceability between KAOS Requirements Models and B Specifications Abderrahman Matoussi Dorian Petit 401

Code Synthesis for Timed Automata: A Comparison Using Case Study Anaheed Ayoub Ayman Wahba Ashraf Salem Mohamed Sheirah 403

Towards Validation of Requirements Models Atif Mashkoor Abderrahman Matoussi 404

A Proof Based Approach for Formal Verification of Transactional BPEL Web Services Idir Aït Sadoune Yamine Aït Ameur 405

On an Extensible Rule-Based Prover for Event-B Issam Maamria Michael Butler Andrew Edmunds Abdolbaghi Rezazadeh 407

B Model Abstraction Combining Syntactic and Semantic Methods Jacques Julliand Nicolas Stouls Pierre-Christope Bué Pierre-Alain Masson 408

A Basis for Feature-Oriented Modelling in Event-B Jennifer Sorge Michael Poppleton Michael Butler 409

Using Event-B to Verify the Kmelia Components and Their Assemblies Pascal André Gilles Ardourel Christian Attiogbé Arnaud Lanoix 410

Starting B Specifications from Use Cases Thiago C. de Sousa Aryldo G. Russo Jr 411

Integrating SMT-Solvers in Z and B Tools Alessandro Cavalcante Gurgel Valério Gutemberg de Medeiros Jr Marcel Vinicius Medeiros Oliveira David Boris Paul Déharbe 412

Formal Analysis in Model Management: Exploiting the Power of CZT James R. Williams Fiona A.C. Polack Richard F. Paige 414

Author Index 415

From the B&N Reads Blog

Customer Reviews