Abstract Formal methods are used for the specification and verification of software and hardware systems. One class of systems interacts with the outside world through sensors and actuators, and may include nondeterminism from hardware faults or environmental inputs, making modelling more complex.
Abstract Event-B is a formal method that allows flexible modelling and refinement of systems. However, it is hard to convince developers to adopt it because they are not used to mathematical models and it doesn’t provide any practical refinement method.
Abstract According to the vision of Design for Reliability, software reliability has to be considered in all the activities within the software development life cycle. In particular, writing formal specifications, like other activities in software development, is error-prone, especially for large-scale systems.
Abstract Specifications of programs frequently involve operators and functions that are not defined over all of their (syntactic) domains. Proofs about specifications –and those to discharge proof obligations that arise in justifying steps of design– must be based on formal rules.
Abstract We present an idea how to simplify Gurevich’s parallel ASM thesis. The key idea is to modify only the bounded exploration postulate from the sequential ASM thesis by allowing also non-ground comprehension terms.
Abstract Previous work described how to translate Simulink control law diagrams into Circus specifications to facilitate verification by refinement. This is not a trivial task; several tools have been developed to automate parts of the translation.
Abstract For safety critical embedded systems the correctness of the processor, toolchain and compiler is an important issue. Translation validation is one approach for compiler verification. A common semantic framework to represent source and target language is needed and Abstract State Machines (ASMs) are a well suited and established method.
Abstract In this paper, we use Alloy Analyzer, a fully automatic checker, to detect vulnerabilities in the multicast key management protocol proposed by Tanaka and Sato, and discover some previously unknown attacks.
Abstract We define an abstract standards-compliant web browser model. The model focuses on those parts of the browser behaviour which are most relevant for the deployment and execution of web applications, such as interaction with a scripting language (here, ECMAScript), cookies, and asynchronous behaviour of the network layer, while hiding other aspects, such as page navigation and presentational issues.
Abstract While many systems are naturally viewed as the interaction between a controller subsystem and a controlled, or plant subsystem, they are often most easily understood and designed monolithically. A practical implementation needs to separate controller from plant.
Abstract Formal methods have been used and successfully applied to a wide range of industrial applications for many years. However formal methods can be difficult to comprehend for outsiders and the link of formal models and external subsystems which are not modelled can be unclear.
Abstract The ASM framework is extended to include continuously varying quantities as well as conventional discretely changing ones. This opens the door to the more faithful modeling of many scenarios where digital systems have to interact with the continuously varying physical world.
Abstract Including provision for continuously varying behaviour as well as discrete state change is considered for Event-B. An extension of Event-B is sketched that accommodates continuous events (called pliant events) in between familiar discrete events (called mode events).
Abstract We suggest an approach for accurate modeling and analysis of web application frameworks.
Document If you cannot see the document below, the PDF document is most likely not freely accessible.
Abstract We present a method to discharge proof obligations from Atelier B using multiple SMT solvers. It is based on a faithful modeling of B’s set theory into polymorphic first-order logic.
Abstract The Event-B method is a formal modelling approach; our interest is the final step, of generating code for concurrent programs, from Event-B. Our Tasking Event-B tool integrates Event-B to facilitate code generation.
Abstract Kodkod, the backend of Alloy4, incorporates new features for solving models where part of the solution, that is, a partial instance, is already known. Although Kodkod has had this functionality for some time, it is not explicitly available to the modeller through the Alloy language syntax.
Abstract The Test Template Framework (TTF) is a method for model-based testing (MBT) from Z specifications. Although the TTF covers many features of the Z notation, it does not explain how to deal with axiomatic descriptions, quantifiers and set comprehensions.
Abstract The New York City Transit Authority has included formal proofs at system level as part of the safety assessment for its New York subway Line 7 modernization project, based on the CBTC from Thales Toronto.
Abstract In this paper we propose an approach to verify PLC programs, a common platform to control systems in the industry. Programs written in the languages of the IEC 61131-3 standard are automatically translated to B machines and are then amenable to formal analysis of safety constraints and general structural properties of the application.
Abstract This paper contains the development of hybrid systems in Event-B and the Rodin Platform. It follows the seminal approach introduced at the turn of the century in Action Systems. Many examples illustrate our approach.
Abstract Plotkin’s structural operational semantics provides a tried and tested method for defining the semantics of a programming language via sets of rules that define valid transitions between program configurations. Mosses’ modular structural operational semantics (MSOS) recasts the approach by making use of rules consisting of labelled transitions, allowing a more modular approach to defining language semantics.
Abstract The Event-B method is a formal approach for reliable systems specification and verification, being supported by the Rodin platform, which includes mature plugins for theorem-proving, model-checking, or model (de)composition features.
Abstract This paper proposes the use of the Abstract State Machine method for a rigorous foundation in modeling and validating Vision-Based Robot Control applications. We show how to tailor control tasks definitions and associated synchronization/communication patterns in rigorous and abstract terms by using control state ASMs and an extension of the classical flowchart notation to allow the definition/instantiation of recurring design solutions and to improve model traceability.
Abstract Scientific literature reveals that symbolic representation techniques behind some formal methods are attractive to synthesize parts or verify properties of large discrete event systems. They involve, however, complex encoding schemata and fine tuning heuristic parameters in order to translate specific problems into efficient BDD or SAT-based representations.
Abstract In a bounded analysis, arithmetic operators become partial, and a different semantics becomes necessary. One approach, mimicking programming languages, is for overflow to result in wrap-around. Although easy to implement, wrap-around produces unexpected counterexamples that do not correspond to cases that would arise in the unbounded setting.
Abstract The Abstract State Machine (ASM) method proposes the concept of ground models for analyzing a target system based on pseudo-code-like descriptions for reasoning about system properties in terms of state machine runs over abstract data structures.
Abstract Decomposition is a technique to separate the design of a complex system into smaller sub-models, which improves scalability and team development. In the shared-variable decomposition approach for Event-B sub-models share external variables and communicate through external events which cannot be easily refined.
Abstract Refinement is a powerful technique for tackling the complexities that arise when formally modelling systems. Here we focus on a posit-and-prove style of refinement, and specifically where a user requires guidance in order to overcome a failed refinement step.