Abstract We present an approach to transform SysML structural diagrams, BDD and IBD with constraints, into a B Method project skeleton. This project can then be directly used for implementation development through usual B refinement mechanism.
Abstract Starting from Gurevich’s thesis for sequential algorithms (the so-called “sequential ASM thesis”), we propose a characterization of the behaviour of sequential algorithms enriched with reflection. That is, we present a set of postulates which we conjecture capture the fundamental properties of reflective sequential algorithms (RSAs).
Abstract Use cases are a popular but informal technique used to define and analyse system behaviour. We introduce UC-B a plug-in for the Rodin platform (Event-B tool) that supports the authoring and management of use case specifications with both informal and formal components.
Abstract The paper presents our efforts in defining UASM, a unified syntax for Abstract State Machines (ASMs), based on the syntaxes of two of the main ASM frameworks, CoreASM and ASMETA, which have been adapted to accept UASM as input syntax of all their validation and verification tools.
Abstract Constraint satisfaction and data validation problems can be expressed very elegantly in state-based formal methods such as B. However, is B suited for developing larger applications and are there existing tools that scale for these projects?
This documents presents a description of a case study concerning the control of a hemodialysis (HD) machine. It provides an overview of the requirements and the design of an HD machine including a sketch of the machine’s functionality, related safety conditions, and a top-level system architectural description.