ABZ'08

ABZ 2008 (London, UK)

1st International Conference on ASM, B, and Z

A Concept-Driven Construction of the Mondex Protocol Using Three Refinements

Abstract The Mondex case study concerns the formal development and verification of an electronic purse protocol. Several groups have worked on its specification and mechanical verification, their solutions being (as were ours previously), either one big step or several steps motivated by the task’s complexity.

A First Attempt to Express KAOS Refinement Patterns with Event B

Abstract It is now recognised that goals play an important role in requirements engineering process, and consequently in systems development process.Whereas specifications allow us to answer the question”WHAT the system does”, goals allow us to address the ”WHY, WHO, WHEN” questions [1].

A Practical Single Refinement Method for B

Abstract We propose a single refinement method for B, inspired directly by Gardiner and Morgan’s longstanding single complete rule for data refinement, and rendered practical by application of the current first author’s recent first-order characterisation of refinement between monotonic computations.

A Roadmap for the Rodin Toolset

Abstract Event-B is a formal method for system-level modelling and analysis. Key features of Event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels.

A Scenario-Based Validation Language for ASMs

Abstract This paper presents the AValLa language, a domain-specific modelling language for scenario-based validation of ASM models, and its supporting tool, the AsmetaV validator. They have been developed according to the model-driven development principles as part of the asmeta (ASM mETAmodelling) toolset, a set of tools around ASMs.

A Verifiable Conformance Relationship between Smart Card Applets and B Security Models

Abstract We propose a formal framework based on the B method, that supports the development of secured smart card applications. Accordingly to the Common Criteria methodology, we start from a formal definition and modelling of security policies, as access control policies.

A Verified AsmL Implementation of Belief Revision

Abstract Belief revision is a key functionality for any intelligent agent being able to perceive pieces of knowledge from its environment and to give back sentences she believes to be true with a certain degree of belief.

ABZ2008 VSR-Net Workshop

Abstract In 2004, the UK Computing Research Committee initiated a number of Grand Challenges aimed at stimulating long term research in key areas of computing science. One of the challenges (GC6) focuses on Dependable Systems Evolution.

Autonomous Objects and Bottom-Up Composition in ZOO Applied to a Case Study of Biological Reactivity

Abstract As part of our work on the formal analysis of object-oriented models, we turn to systems where many autonomous individuals interact to give rise to complex collective behaviour. We adapt our ZOO [1,2] structuring and apply it to a case study based on a published model of part of the immune system [3].

BART: A Tool for Automatic Refinement

Abstract Refining a B specification into an implementation can be a complex and time consuming process. This process can usually be separated in two distinct parts: the specification part, where the refinement is used to introduce new properties and specification details, and the implementation, where refinement is used to convert a detailed B specification into a B0 implementation.

BSmart: A Tool for the Development of Java Card Applications with the B Method

Abstract A smart card is a portable computer device able to store data and execute commands. Java Card [1] is a specialization of Java, providing vendor inter-operability for smart cards, and has now reached a de facto standard status in this industry.

Combining Scenario- and Model-Based Testing to Ensure POSIX Compliance

Abstract We present in this paper a way to produce test suites for the POSIX mini-challenge, based on a formal model of a file system manager, written using a B machine.

Complex Hardware Modules Can Now be Made Free of Functional Errors without Sacrificing Productivity

Abstract Complementary to the systems and software focus of the conference, this presentation will be about chips and the progress that has been made in their functional verification. Common ground will be high-level, still cycleaccurate, state-based models of hardware functionalities called Abstract RT.

Data Flow Analysis and Testing of Abstract State Machines

Abstract This paper introduces an approach to apply data flow testing techniques to Abstract State Machines specifications. Since traditional data flow coverage criteria are strictly based on the mapping between a program and its flow graph, they cannot be directly applied to ASMs.

DIR 41 Case Study

Abstract Some RATP units are responsible for evolution and maintenance of an automated interlocking specification document. In order to improve their paper and pencil process, RATP asked Systerel if Event-B could be useful to them.

Direct Support for Model Checking Abstract State Machines by Utilizing Simulation

Abstract This paper presents an approach to model checking abstract state machines (ASMs) without the need for translation of the ASM specification into the modeling language of an existing model checker.

Dynamic Resource Configuration & Management for Distributed Information Fusion in Maritime Surveillance

Abstract We propose a highly adaptive and auto-configurable, multi-layer network architecture for distributed information fusion to address large volume surveillance challenges, assuming a multitude of different sensor types on multiple mobile platforms for intelligence, surveillance and reconnaissance.

Exploiting the ASM Method for Validation & Verification of Embedded Systems

Abstract SystemC (built upon C++) [2] is an IEEE industry-standard language for system-level models, specifically targeted at architectural, algorithmic, transaction-level modelling. Recently, a further improvement has been achieved by trying to combine SystemC with lightweight software modelling languages like UML to describe system specifications.

FDIR Architectures for Autonomous Spacecraft: Specification and Assessment with Event-B

Abstract On-board Fault Detection, Isolation and Recovery (FDIR) systems are considered to ensure the safety and to increase the autonomy of spacecrafts. They shall be carefully designed and validated. Their implementation involves a relevant knowledge of items like functions and architectures of the system, and a fault model in relation with these items.

Formal Modeling and Analysis of a Flash Filesystem in Alloy

Abstract This paper describes the formal modeling and analysis of a design for a flash-based filesystem in Alloy. We model the basic operations of a filesystem as well as features that are crucial to NAND flash hardware, such as wear-leveling and erase-unit reclamation.

Formal Verification of ASM Models Using TLA+

Abstract The notion of Abstract State Machines(ASMs) handles a practical new approach for modeling and analysing various kinds of discrete dynamic systems. In the context of the verification problem of ASM models, formal verification techniques based on variants of restricted first-order temporal logic have been used to verify correctness of restricted forms of ASM specifications.

From ABZ to Cryptography

Abstract Three Steps from the Ideal Ideally correctness is by construction; post-hoc verification is second choice; verification of proofs is the next step down. In the application area of modern cryptographic protocol verification, the latter would be viewed as serious progress.

Generating Tests from B Specifications and Test Purposes

Abstract This paper is about generating tests from test purposes, in addition to structural tests. We present a method that re-uses a behavioural model and an abstract test concretization layer developed for structural testing, and relies on additional test purposes.

Integrating Z into Large Projects Tools and Techniques

Abstract If we want to use Z to write an overall system specification, we need to integrate it into a rich set of documents written in natural language and domain-specific notations.

Model Based Refinement and the Tools of Tomorrow

Abstract The ingredients of typical model based development via refinement are re-examined, and some well known frameworks are reviewed in that light, drawing out commonalities and differences. It is observed that alterations in semantics take place de facto due to applications pressures and for other reasons.

Model Checking Event-B by Encoding into Alloy

Abstract Current day systems are ever more detailed and complex leading to the necessity of developing models that abstract unimportant implementation details while emphasizing their structure. Until recently it was only possible to perform temporal model checking in an Event-B model by converting the model to B-METHOD and then using ProB [1].

Modeling Workflows, Interaction Patterns, Web Services and Business Processes: The ASM-Based Approach

Abstract We survey the use of the Abstract State Machines (ASM) method for a rigorous foundation of modeling and validating web services, workflows, interaction patterns and business processes. We show in particular that one can tailor business process definitions in application-domain yet rigorous terms in such a way that the resulting ASM models can be used as basis for binding contracts between domain experts and IT technologists.

Modelling Attacker's Knowledge for Cascade Cryptographic Protocols

Abstract We address the proof-based development of cryptographic protocols satisfying security properties. Communication channels are supposed to be unsafe. Analysing cryptographic protocols requires precise modelling of the attacker’s knowledge. In this paper we use the event B modelling language to model the knowledge of the attacker for a class of cryptographic protocols called cascade protocols.

Object Modelling in the SystemB Industrial Project

Abstract The SystemB project is a two year project at the University of Surrey, funded by AWE plc, and is concerned with bridging the areas of formal methods and object modelling.