2nd Call for participation: ABZ 2008 Conference, London, UK, 16-18September 2008

2nd CALL FOR PARTICIPATION: ABZ 2008 CONFERENCE

The programme and the online registration form for the ABZ 2008
Conference
on the ASM, B and Z formal methods are available at
http://www.abz2008.org/

The conference is preceded by a VSR-net workshop (Verified Software
Repository), with free registration for conference participants, on
Monday
15 September (and a small charge for non-participants). This is being
organized by Jim Woodcock and speakers include Tony Hoare. The event
is
recommended and further details are below and online.

Both events are being held at the British Computer Society offices in
Covent
Garden, a lively area in central London (nearest tube stations,
Charing
Cross or Covent Garden). The conference dinner will be held at the IET
headquarters close by overlooking the River Thames.

Sponsors include the BCS, FACS, FME, Nokia and Praxis High Integrity
Systems.

--
Jonathan Bowen, co-chair
www.jpbowen.com
------------------------------------------------
ABZ2008 Programme

Monday 15 September

VSR-net (Verified Software Repository) workshop

Chair: Jim Woodcock

Invited talk: Cliff Jones (University of Newcastle). Splitting atoms
with
rely/guarantee-conditions coupled with data reification

Further speakers:

Jim Woodcock (University of York). Progress on the Verified Software
Repository

Richard Banach (University of Manchester). The Mondex Purse:
Requirements
and Retrenchments

Michael Butler (University of Southampton). Applying Event-B and Rodin
to
the filestore

John Fitzgerald (University of Newcastle). Approaches to the Pacemaker
Challenge Problem

Tony Hoare (Microsoft Research, Cambridge). Hopes and their fulfilment

Eunsuk Kang (MIT).


Tuesday 16 September

8.30-9.00 Registration

Invited talk

9.00-10.00 Wolfram Buettner (One-Spin, Munich). Complex Hardware
Modules can
now be made Free of Functional Errors without Sacrificing

Productivity

10.00-10.30 Break

Invited talks

10.30-11.30 Michael Leuschel (University of Duesseldorf). Demonstrably
Correct Compilation of Java Bytecode

11.30-12.30 Bernhard Thalheim (University of Kiel). Foundations of
Workflow
Specifications

12.30-14.00 Lunch

Invited talk

14.00-15.00 Gerhard Schellhorn (University of Augsburg). Refinement of
State-based Systems: ASMs and Big Commuting Diagrams

15.00-15.30 Break

Special presentations on ASM, B and Z

15.30-16.15 Richard Banach. Model Based Refinement and the Tools of
Tomorrow

16.15-17.00 Stefan Hallerstede. On the Purpose of Event-B Proof
Obligations

17.00-17.45 John Derrick, S. North and Anthony J.H. Simons. Z2SAL -
Building
a Model Checker for Z


Wednesday 17 September

ASM track

9:00-9:45 Gerhard Schellhorn and Richard Banach. A Concept-Driven
Construction of the Mondex Protocol using Three Refinements

9:45-10.30 Alessandro Carioni, Angelo Gargantini, Elvinia Riccobene
and
Patrizia Scandurra. A Scenario-based Validation Language for ASMs

Z/B track

9:00-9:30 Anthony Hall. Integrating Z into Large Projects: Tools and
Techniques

9:30-10:00 Jacques Julliand, Pierre-Alain Masson and Régis Tissot.
Generating Tests from B Specifications and Test Purposes

10:00-10:30 Frederic Dadeau, Adrien De Kermadec and Régis Tissot.
Combining
Scenario- and Model-based Testing to ensure POSIX Compliance

10.30-11.00 Break

Z track

11:00-11:30 Eunsuk Kang and Daniel Jackson. Formal Modeling and
Analysis of
a Flash Filesystem in Alloy

11:30-12:00 Mark Utting and Petra Malik. Unit Testing of Z
Specifications

12:00-12:30 Nuno Amalio, Fiona Polack and Jing Zhang. Autonomous
Objects and
Bottom-up Composition in ZOO Applied to a Case Study of Biological
Reactivity

B track

11:00-11:30 Richard Banach. UseCase-wise Development: Retrenchment for
Event-B

11:30-12:00 Juan Bicarregui, Alvaro Arenas, Benjamin Aziz, Philippe
Massonet
and Christophe Ponsard. Towards Modelling Obligations in Event-B

12:00-12:30 Steve Dunne and Stacey Conroy. A Practical Single
Refinement
Method for B

12.30-14.00 Lunch

ASM track

14:00-14:45 Alessandra Cavarra. Data Flow Analysis and Testing of
Abstract
State Machines

14:45-15.30 Christoph Beierle and Gabriele Kern-Isberner. A Verified
AsmL
Implementation of Belief Revision

B track

14:00-14:30 Michael Poppleton. The composition of Event-B models

14:30-14:45 Abderrahman Matoussi, Frederic Gervais and Regine Laleau.
A
First Attempt to Express KAOS Refinement Patterns with Event B

14:45-15:15 Ken Robinson. Reconciling Axiomatic and Model-Based
Specifications Reprised

15:15-15:30 Idir Ait-Sadoune and Yamine Ait Ameur. Verification and
Validation of Web Service Composition Using Event B Method

15.30-16.00 Break

ASM/Z track

16:00-16:15 Joelle Cohen and Anatol Slissenko. Stability of Real-time
Abstract State Machines

16:15-16:30 Qing Wang, Klaus-Dieter Schewe and Bernhard Thalheim. XML
Database Transformations with Tree Updates

16:30-16:45 Roozbeh Farahbod and Uwe Glaesser. Dynamic Resource
Configuration & Management for Distributed Information Fusion in
Maritime
Surveillance

16:45-17:00 Ali N. Haidar and Ali E. Abdallah. Weaving Authentication,
Authorization and Auditing Requirements into the Functional Model of a
System using Z Promotion

B track

16:00-16:15 Colin Snook and Michael Butler. UML-B: A Plug-in for the
Event-B
Tool Set

16:15-16:30 Antoine Requet. BART: A Tool for Automatic Refinement

16:30-16:45 Paulo Matos and Joao Marques-Silva. Model Checking Event-B
by
Encoding into Alloy

16:45-17:00 Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede
and
Laurent Voisin. A Roadmap for the Rodin Toolset

Thursday 18 September

ASM/Z track

9:00-9:45 Jörg Beckers, Daniel Klünder, Stefan Kowalewski and Bastian
Schlich. Direct Support for Model Checking Abstract State Machines by
Utilizing Simulation

9:45-10.00 Angelo Gargantini, Elvinia Riccobene and Patrizia
Scandurra.
Exploiting the ASM method for Validation & Verification of Embedded
Systems

10:00-10.15 Alessandro Cavalcante Gurgel, Cristiano Gurgel Castro and
Marcel
Vinicius Medeiros Oliveira Oliveira. Tool Support for the Circus
Refinement
Calculus

10:15-10.30 Ramsay Taylor. Separation of Z Operations

B track

9:00-9:30 Frederic Dadeau, Julien Lamboley, Thierry Moutet and Marie-
Laure
Potet. A verifiable Conformance Relationship between Smart Card
Applets and
B Security models

9:30-9:45 David Deharbe, Bruno Gomes and Anamaria Moreira. BSmart: A
Tool
for the Development of Java Card Applications with the B Method

9:45-10:15 Benaissa Nazim. Modelling Attacker's Knowledge for Cascade
Cryptographic Protocols

10:15-10:30 Eerke Boiten. From ABZ to Cryptography

10.30-11.00 Break

ASM/Z track

11:00-11.15 Ali Abou Dib and Ileana Ober. Using ASM to Achieve
Executability
within a Family of DSL

11:15-11.30 Margus Veanes and Ando Saabas. Using Satisfiability Modulo
Theories to Analyze Abstract State Machines

11:30-11.45 El Habib Daho Hocine and Benhamamouch Djilali. Formal
Verification of ASM Models Using TLA+

11:45-12.00 Miyoung Kang, Dea-Yon Hwang, Junkil Park, Jin-Young Choi
and
Jong-Gju Hwang. Formal Requirement Specification for Railway Signaling
Systems

12.00-12.15 Takabi Hassan and Ali E. Abdallah. Formalizing Delegation
in
Role-Based Access Control Models

B track

11:00-11:30 Stephen Wright. Using EventB to Create a Virtual Machine
Instruction Set Architecture

11:30-11:45 Christophe Metayer and Mathieu Clabaut. DIR 41 Case Study:
How
Event-B can Improve an Industrial System

11:45-12:00 Jean-Charles Chaudemar, Charles Castel and Christel
Seguin.
Model-based Safety of FDIR Architectures for Autonomous Spacecraft:
Specification and Assessment with Event-B

12:00-12:15 Helen Treharne, Edward Turner, Steve Schneider and Neil
Evans.
Object Modelling in the SystemB Industrial Project

12.15-14.00 Lunch

ASM tutorial

14.00-15.30 Roozbeh Farahbod (Simon Frazer University). Using CoreASM
for
High Level Design, Analysis and Validation of Distributed Systems
Models

15.30-16.00 Break

B tutorial

16.00-17.30 Jens Bendisposto and Daniel Plagge (University of
Duesseldorf).
Validating B, Z and CSP with ProB