156,213 research outputs found
Tasking Event-B: An Extension to Event-B for Generating Concurrent Code
No full textThe Event-B method is a formal approach for modelling systems in safety-, and business-critical, domains. Initially, system specification takes place at a high level of abstraction; detail is added in refinement steps as the development proceeds toward implementation. Our aim has been to develop a novel approach for generating code, for concurrent programs, from Event-B. We formulated the approach so that it integrates well with the existing Event-B methodology and tools. In this paper we introduce a tasking extension for Event-B, with Tasking and Shared Machines. We make use of refinement, decomposition, and the extension, to structure projects for code generation for multitasking implementations. During the modelling phase decomposition is performed; decomposition reduces modelling complexity and makes proof more tractable. The decomposed models are then extended with sufficient information to enable generation of code. A task body describes a task’s behaviour, mainly using imperative, programming-like constructs. Task priority and life-cycle (periodic, triggered, etc.) are also specified, but timing aspects are not modelled formally. We provide tool support in order to validate the practical aspects of the approach
Applying Atomicity and Model Decomposition to a Space Craft System in Event-B
No full textEvent-B is a formal method for modeling and verifying consistency of systems. In formal methods such as Event-B, refinement is the process of enriching or modifying an abstract model in a step-wise manner in order to manage the development of complex and large systems. To further alleviate the complexity of developing large systems, Event-B refinement can be augmented with two techniques, namely atomicity decomposition and model decomposition. Our main objective in this paper is to investigate and evaluate the application of these techniques when used in a refinement based development. These techniques have been applied to the formal development of a space craft system. The outcomes of this experimental work are presented as assessment results. The experience and assessment can form the basis for some guidelines in applying these techniques in future cases
Automatic Refinement Checking for B
No full textRefinement is a key concept in the B-Method. While refinement is at the heart of the B Method, so far no automatic refinement checker has been developed for it. In this paper we present a refinement checking algorithm and implementation for B. It is based on using an operational semantics of B, obtained in practice by the ProB animator. The refinement checker has been integrated into ProB toolset and we present various case studies and empirical results in the paper, showing the algorithm to be surprisingly effective. The algorithm checks that a refinement preserves the trace properties of a specification. We also compare our tool against the refinement checker FDR for CSP and discuss an extension for singleton failure refinement
Decomposition Structures for Event-B
No full textAbstract. Event-B provides a flexible approach to modelling and re-finement of systems. In this paper we outline two important ways in which Event-B refinement can be augmented with additional structuring to support further the management of complex refinements. Firstly we show how event refinement diagrams can be used to structure refinement steps involving decomposition of atomicity. Secondly we outline a tech-nique for decomposing models into sub-models to allow for independent refinement. We show how these two structuring techniques can be used together.
Shared Event Composition/Decomposition in Event-B
No full textThe construction of specifications is often a combination of smaller sub-components. Composition and decomposition are techniques that support reuse and allow us to formally combine sub-components through refinement steps while reusing their properties. Sub-components can result from a design or architectural goal and a refinement framework should allow further parallel development over the sub-components. We propose the definition of composition and decomposition in the Event-B formalism following a shared event approach where sub-components interact via synchronisation over shared events and shared states are not allow. We define the necessary proof obligations to ensure a valid composition or decomposition. We also show that shared event composition preserves refinement proofs for sub-components, that is, in order to maintain refinement of compositions, it is sufficient to prove refinement between corresponding subcomponents. A case study applying these two techniques is illustrated using Rodin, the Event-B toolset
Supporting reuse of Event-B developments through generic instantiation
No full textIt is believed that reusability in formal development should reduce the time and cost of formal modelling within a production environment. Along with the ability to reuse formal models, it is desirable to avoid unnecessary re-proof when reusing models. Event-B is a formal method that allows modelling and refinement of systems. Event-B supports generic developments through the context construct. Nevertheless Event-B lacks the ability to instantiate and reuse generic developments in other formal developments. We propose a way of instantiating generic models and extending the instantiation to a chain of refinements. We define sufficient proof obligations to ensure that the proofs associated to a generic development remain valid in an instantiated development thus avoiding re-proofs
Supporting reuse mechanisms for developments in event-b: composition
No full textThe development of specifications often is a combination of smaller sub-components. Focusing on reuse, an interesting perspective is to formally define the combination of sub-components through refinement steps, reusing their properties and generating larger systems. The previous situation suggests the application of a reuse mechanism: composition. Event-B is a formal method that allows modelling and refinement of systems. The combination and reuse of existing sub-components is not currently supported in Event-B. We propose the development of composition by extending the Event-B formalism as an option for developing larger models, focusing in distributed systems. A tool is developed to support the shared event composition in the Rodin platform. Properties and proof obligations of sub-components are reused and sufficient proof obligations are generated to ensure valid composed models
UML-B: Formal modelling and design aided by UML
No full textThe emergence of the UML as a de-facto standard for object-oriented modelling has been mirrored by the success of the B method as a practically useful formal modelling technique. The two notations have much to offer each other. The UML provides an accessible visualisation of models facilitating communication of ideas but lacks formal precise semantics. B, on the other hand, has the precision to support animation and rigorous verification but requires significant effort in training to overcome the mathematical barrier that many practitioners perceive. We utilise a derivation of the B notation as an action and constraint language for the UML and define the semantics of UML entities via a translation into B. Through the UML-B profile we provide specialisations of UML entities to support model refinement. The result is a formally precise variant of UML that can be used for refinement based, object-oriented behavioural modelling. The design of UML-B has been guided by industrial applications
Specification and refinement of discrete timing properties in Event-B
No full textEvent-B is a formal language for systems modeling, based on set theory and predicate logic. It has the advantage of mechanized proof, and it is possible to model a system in several levels of abstraction by using refinement. Discrete timing properties are important in many critical systems. However, modeling of timing properties is not directly supported in Event-B. In this paper we identify three main categories of discrete timing properties for trigger-response pattern, deadline, delay and expiry. We introduce language constructs for each of these timing properties that augment the Event-B language. We describe how these constructs can be mapped to standard Event-B constructs. To ease the process of using the timing constructs in a refinement-based development, we introduce patterns for refining the timing constructs that allow timing properties on abstract models to be replaced by timing properties on refined models. The language constructs and refinement patterns are illustrated through some generic examples. Event-B refinement allows atomic events at the abstract level to be broken down into sub-steps at the refined level. The goal of our refinement patterns is to provide an easy way to represent and correctly refine timing constraints on abstract atomic events with more elaborate timing constraints on the refined events. This paper presents an initial set of patterns
- …
