23,478 research outputs found
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
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
Language and tool support for class and state machine refinement in UML-B
No full textUML-B is a ’UML-like’ graphical front end for Event-B that provides support for object-oriented modelling concepts. In particular, UML-B supports class diagrams and state machines, concepts that are not explicitly supported in plain Event-B. In Event-B, refinement is used to relate system models at different abstraction levels. The same abstraction-refinement concepts can also be applied in UML-B. This paper introduces the notions of refined classes and refined state machines to enable refinement of classes and state machines in UML-B. Together with these notions, a technique for moving an event between classes to facilitate abstraction is also introduced. Our work makes explicit the structures of class and state machine refinement in UML-B. The UML-B drawing tool and Event-B translator are extended to support the new refinement concepts. A case study of an auto teller machine (ATM) is presented to demonstrate application and effectiveness of refined classes and refined state machines
The Guy Butler Collection Inventories
No full textThe Guy Butler Collection Inventories consists of the following: Section A: Material concerning Butler’s academic and broader interests. Section B: Family material. Section C: Newspaper clippings. Section D: Miscellaneous. Section E: Guy Butler writing. Section F: Photographs of the different Butler families, including Biggs, Butler, Collett, Friends, Satchwell, Stringer and Trollip. Section G: Photographs (Prophetic Nun). Section H: Photographs (Miscellaneous)
ProB: A Model Checker for B
No full textWe present ProB, an animation and model checking tool for the B method. ProB's animation facilities allow users to gain confidence in their specifications, and unlike the animator provided by the B-Toolkit, the user does not have to guess the right values for the operation arguments or choice variables. ProB contains a model checker and a constraint-based checker, both of which can be used to detect various errors in B specifications. We present our first experiences in using ProB on several case studies, highlighting that ProB enables users to uncover errors that are not easily discovered by existing tools
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
- …
