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. This approach thus integrates formal methods into existing industrial processes.
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. MSOS can be adapted by using “syntactic” labels that allow local variables and aliasing to be defined without augmenting the semantics with environments and locations. The syntactic labels allow both state-based constructs of imperative languages and event-based constructs of process algebras to the specified in an integrated manner. To illustrate the integrated approach we compare its rules with Plotkin’s original rules for both small-step and big-step operational semantics. One issue that arises is that defining concurrency requires the use of a small-step approach to handle interleaving, while defining a specification command requires a big-step approach. The integrated approach can be generalised to use a sequence of (small) steps as a label; we call this a multi-step operational semantics. This approach allows both concurrency and non-atomic specification commands to be defined.
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. In order to complement these techniques with test generation and state model inference from Event-B models, we developed a new feature as a Rodin plugin. Our plugin implements a model-learning approach to iteratively construct an approximate automaton model together with an associated test suite. Test suite optimization is further applied according to different optimization criteria.
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. This approach may be too costly when the main goal is to explore a theory, understand by simulation its underlying concepts and computation procedures, and conduct experiments by applying them to small problems. Based on previous work with Alloy on the synthesis of observers and nonblocking supervisors of a system organized hierarchically with a flat state space estimated to 1031 states, this paper investigates more deeply issues raised with its use in the modeling and prototyping of the supervisory control theory, including the application of models to practical problems. This study was conducted in a broader context than just hierarchical control since it embraces various variants of this theory.
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. This paper describes a new approach, implemented in the latest version of the Alloy Analyzer, in which instances that would involve overflow are suppressed, and consequently, spurious counterexamples are eliminated. The key idea is to interpret quantifiers so that bound variables range only over values that do not cause overflow.
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. This highly iterative process builds on stepwise refinement of ground models that evolve with progressing understanding of functional system requirements. Usually, as complexity increases, reorganization of a model’s internal structure helps enhance its flexibility and robustness. While this approach is common practice, the underlying principles are usually left implicit. In this paper, we propose refactoring patterns to restructure abstract machine models with the goal of improving their intelligibility and maintainability.
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. Our first contribution hence is a proposal for a new construct called interface that encapsulates the external variables, along with a mechanism for interface instantiation. Using the new construct and mechanism, external variables can be refined consistently. Our second contribution is an approach for verifying the correctness of Event-B extensions using the supporting Rodin tool. We illustrate our approach by proving the correctness of interface instantiation.
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. We take an integrated approach – combining the complementary strengths of top-down planning and bottom-up theory formation. In this paper we focus mainly on the planning perspective. Specifically, we propose a new technique called refinement plans which combines both modelling and reasoning perspectives. When a refinement step fails, refinement plans provide a basis for automatically generating modelling guidance by abstracting away from the details of low-level proof failures. The refinement plans described here are currently being implemented for the Event-B modelling formalism, and have been assessed on paper using case studies drawn from the literature. Longer-term, our aim is to identify refinement plans that are applicable to a range of modelling formalisms.