7,879 research outputs found
The composition of Event-B models
No full textThe transition from classical B [2] to the Event-B language and method [3] has seen the removal of some forms of model structuring and composition, with the intention of reinventing them in future. This work contributes to thatreinvention. Inspired by a proposed method for state-based decomposition and refinement [5] of an Event-B model, we propose a familiar parallel event composition (over disjoint state variable lists), and the less familiar event fusion (over intersecting state variable lists). A brief motivation is provided for these and other forms of composition of models, in terms of feature-based modelling. We show that model consistency is preserved under such compositions. More significantly we show that model composition preserves refinement
Java implementation platform for the integrated state- and event-based specification in PROB
No full textPROB is an animation and model checking tool, which supports integrated event- and state-based specifications combining B and CSP. We present an initial strategy for implementing the combined specification model as a concurrent Java program. Our Java implementation for the combined B and CSP model uses a similar approach to that of JCSP. The restricted operational semantics for the integrated B and CSP model in PROB is defined. Then a new Java package, JCSProB, is developed for implementing the semantics. The new package supports external choice with multi-way synchronization, and introduces an improved multi-threading implementation from JCSP
Timing diagrams add Requirements Engineering capability to Event-B Formal Development
No full textEvent-B is a language for the formal development of reactive systems. At present the RODIN toolkit [15] for Event-B is used for modeling requirements, specifying refinements and doing verification. In order to extend graphical requirements modeling capability into the real-time domain, where timing constraints are essential, we propose a Timing diagram (TD) [13] notation for Event-B. The UML 2.0 based notation provides an intuitive graphical specification capability for timing constraints and causal dependencies between system events. A translation scheme to Event-B is proposed and presented. Support for model refinement is provided. A partial case study is used to demonstrate the translation in practice
Towards Feature-Oriented Specification and Development with Event-B
No full textA proposal is made for the development of a feature-oriented reuse capability for safety-critical software construction using rigorous methods. We pr´ecis the Event-B language - the evolution of the B-Method of J.-R. Abrial [1] - a leading formal method for safety-critical software development. Current and new infrastructure for scalable development with Event-B is outlined, and contrasted with support required for feature-oriented development. The proposal is illustrated by a small example of feature-oriented construction and refinement with Event-B
Retrenching partial requirements into system definitions: A simple feature interaction case study
No full textIn conventional model-oriented formal refinement, the abstract model is supposed to capture all the properties of interest in the system, in an as-clutter-free-as-possible manner. Subsequently, the refinement process guides development inexorably towards a faithful implementation. However refinement says nothing about how to obtain the abstract model in the first place. In reality, developers experiment with prototype models and their refinements until a workable arrangement is discovered. Retrenchment is a formal technique intended to capture some of the informal approach to a refinable abstract model in a formal manner that will integrate with refinement. This is in order that the benefits of a formal approach can migrate further up the development hierarchy. The basic ideas of retrenchment are presented, and a simple telephone system feature interaction case study is elaborated. This illustrates not only how retrenchment can relate incompatible and partial models to a more definitive consolidated model during the development of the contracted specification, but also that the same formalism is applicable in a reengineering context, where the subsequent evolution of a system may be partly incompatible with earlier design decisions. The case study illustrates how the natural method of composing retrenchments can give results that are too liberal in certain cases, and stronger laws of composition are derived for systems possessing suitable properties. It is shown that the methodology can encompass more ad hoc and custom built techniques such as Zave’s layered feature engineering approach to applications exhibiting a feature oriented architecture (such as telephony)
Engineering and theoretical underpinnings of retrenchment
No full textRefinement is reviewed, highlighting in particular the distinction between its use as a specification constructor at a high level, and its use as an implementation mechanism at a low level. Some of its shortcomings as a specification constructor at high levels of abstraction are pointed out, and these are used to motivate the adoption of retrenchment for certain high level development steps. Basic properties of retrenchment are described, including a justification of the operation proof obligation, simple examples, its use in requirements engineering and model evolution, and simulation properties. The interaction of retrenchment with refinement notions of correctness is overviewed, as is a range of other technical issues. Two case study scenarios are presented. One is a simple digital redesign control theory problem, and the other is an overview of the application of retrenchment to the Mondex Purse development
Composing Event-B Specifications - Case-Study Experience
No full textEvent-B is a formal method, based on set theory and first-order logic, for specification and verification of reactive systems supported by the Rodin tool kit. Feature modelling is a well-known technique for managing variability and configuring products within software product lines (SPLs). Our objective is to explore whether we can use existing Event-B composition techniques and tooling for feature-based product line development. If case-study experiments reveal these mechanisms to be inadequate, then they also should suggest further research directions. The main objective is to maximise the amount of reuse. This includes avoiding as far as possible having to reprove a composed specification when the models being composed have already been proven. We have modelled two case-studies in Event-B using both horizontal and vertical refinements. This work contributes by analysing existing tools and techniques in Event-B for feature-based development, exploring composition related issues by modelling example case-studies and suggesting further tooling requirements
Retrenching the Purse: Finite Exception Logs, and Validating the Small
No full textThe Mondex Electronic Purse is an outstanding example of industrial scale formal refinement, and was the first verification to achieve ITSEC level E6 certification. A formal abstract model and a formal concrete model were developed, and a formal refinement was hand-proved between them. Nevertheless, certain requirements issues were set beyond the scope of the formal development, or handled in an unnatural manner. The retrenchment Tower Pattern is used to address one such issue in detail: the finiteness of the purse log (which records unsuccessful transactions). A retrenchment is constructed from the lowest level model of the purse system to a model in which logs are finite, and is then lifted to create two refinement developments of the purse, working at different levels of detail, and connected via retrenchments, forming the tower. The tower development is appropriately validated, vindicating the design used
JCSProB: Implementing Integrated Formal Specifications in Concurrent Java
No full textThe ProB model checker provides tool support for an integrated formal specification approach, which combines the classical state-based B language with the event-based process algebra CSP. In this paper, we present a developing strategy for implementing such a combined ProB specification as a concurrent Java program. A Java implementation of the combined B and CSP model has been developed using a similar approach to JCSP. A set of translation rules relates the formal model to its Java implementation, and we also provide a translation tool JCSProB to automatically generate a Java program from a ProB specification. To demonstrate and exercise the tool, several B/CSP models, varying both in syntactic structure and behavioural/concurrency properties, are translated by the tool. The models manifest the presence and absence of various safety, deadlock, and bounded fairness properties; the generated Java code is shown to faithfully reproduce them. Run-time safety and bounded fairness checking is also demonstrated. The Java programs are discussed to demonstrate our implementation of the abstract B/CSP concurrency model in Java. In conclusion we consider the effectiveness and generality of the implementation strategy
Structuring Retrenchments in B by Decomposition
No full textSimple retrenchment is briefly reviewed in the B language of J.-R. Abrial [ref] as a liberalization of classical refinement, for the formal description of application developments too demanding for refinement. This work initiates the study of the structuring of retrenchment-based developments in B by decomposition. A given coarse-grained retrenchment relation between specifications is decomposed into a family of more fine-grained retrenchments. The resulting family may distinguish more incisively between refining, approximately refining, and non-refining behaviours. Two decomposition results are given, each sharpening a coarse-grained retrenchment within a particular syntactic structure for operations at concrete and abstract levels. A third result decomposes a retrenchment exploiting structure latent in both levels. The theory is illustrated by a simple example based on an abstract model of distributed computing, and methodological aspects are considered
- …
