Call for participation: ABZ 2008 Conference, London, 16-18 September 2008
Jonathan Bowen
The programme and the online registration form for the ABZ 2008
Conference
on the ASM, B and Z formal methods are now available at
http://www.abz2008.org/
The conference is preceded by a VSR-net workshop (Verified Software
Repository), with free registration, on Monday 15 September.
Both events are being held at the British Computer Society offices in
central London. There is limited space due to fire regulations, so
please
book early to avoid disappointment!
--
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