305,513 research outputs found
A Basis for feature-oriented modelling in Event-B
No full textFeature-oriented modelling is a well-known approach for Software Product Line (SPL) development. It is a widely used method when developing groups of related software. Due to reuse methods, the development of the software product is quicker, less expensive and of higher quality. However, this approach is not common in formal methods development, which is generally high cost and time consuming, yet crucial in the development of critical systems. We present a method to integrate feature-oriented development with the formal specification language Event-B. Our approach allows the user to map a feature from the feature model to an Event-B component, which contains a formal specification of that feature. We also present some patterns, which assist the user in the modelling of Event-B components. We describe a composition process which consists of the user selecting an instance in the feature model and then constructing this instance in Event-B. While composing, the user may also discharge new composition proof obligations in order to ensure the model is consistent. The model is then constructed using a number of composition rules.<br/
ERTMS Hybrid Level 3 - model using iUML-B/Event-B
No full textiUML-B based model of the ERTMS Hybrid Level 3 specification. Developed to support ABZ2018 case study track paper:
Diagram-led formal modelling using iUMLB for Hybrid ERTMS Level 3,
Dana Dghaym, Michael Poppleton, Colin Snook</span
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
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
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
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
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)
Retrenchment and the Mondex Electronic Purse (Extended Abstract)
No full textSome of the success stories of model based refinement are recalled, as well as some of the annoyances that arise when refinement is deployed in the engineering of large systems. The way that retrenchment attempts to alleviate such inconveniences is reviewed. The Mondex Electronic Purse formal development provides a highly credible testbed for examining how real world refinement difficulties can be treated via retrenchment. The contributions of retrenchment to integrating the real implementation with the formal development are surveyed, and the extraction of commonly occurring ‘retrenchment patterns’ is suggested
Towards an integrated formal method for verification of liveness properties in distributed systems: with application to population protocols
No full textState-based formal methods [e.g. Event-B/RODIN (Abrial in Modeling in Event-B—system and software engineering. Cambridge University Press, Cambridge, 2010; Abrial et al. in Int J Softw Tools Technol Transf (STTT) 12(6):447–466, 2010)] for critical system development and verification are now well established, with track records including tool support and industrial applications. The focus of proof-based verification, in particular, is on safety properties. Liveness properties, which guarantee eventual, or converging computations of some requirements, are less well dealt with. Inductive reasoning about liveness is not explicitly supported. Liveness proofs are often complex and expensive, requiring high-skill levels on the part of the verification engineer. Fairness-based temporal logic approaches have been proposed to address this, e.g. TLA Lamport (ACM Trans Program Lang Syst 16(3):872–923, 1994) and that of Manna and Pnueli (Temporal verification of reactive systems—safety. Springer, New York, 1995). We contribute to this technology need by proposing a fairness-based method integrating temporal and first-order logic, proof and tools for modelling and verification of safety and liveness properties. The method is based on an integration of Event-B and TLA. Building on our previous work (Méry and Poppleton in Integrated formal methods, 10th international conference, IFM 2013, Turku, Finland, pp 208–222, 2013. doi:10.?1007/?978-3-642-38613-8_?15), we present the method via three example population protocols Angluin et al. (Distrib Comput 18(4):235–253, 2006). These were proposed as a theoretical framework for computability reasoning about Wireless Sensor Network and Mobile Ad-Hoc Network algorithms. Our examples present typical liveness and convergence requirements. We prove convergence results for the examples by integrated modelling and proof with Event-B/RODIN and TLA. We exploit existing proof rules, define and apply three new proof rules; soundness proofs are also provided. During the process we observe certain repeating patterns in the proofs. These are easily identified and reused because of the explicit nature of the reasoning
Feature composition - towards product lines of event-B models
No full textEvent-B is a formal language for modelling reactive systems, based on set theory and first-order logic. The RODIN toolkit provides comprehensive tool support for modelling and refinement in Event-B, analysis and verification using animator/model-checkers and theorem provers. We consider the need to support reuse, in particular product line reuse, in such a formal development method. Feature modelling is an established technique for reuse in product lines. We introduce concepts of feature modelling and composition in Event-B to support the reuse of formal models and developments. A prototype feature composition tool has been developed (as a RODIN plug-in) for Event-B, based on the Eclipse Modelling Framework (EMF). Using an MDD philosophy, the tool extends the Event-B language meta-model to a composition meta model, and implements prototype composition patterns for Event-B features. Thus, a required composite model can be constructed by selecting, specializing, and composing input features in a defined way. The tool is the first step towards full feature modelling for product line model reuse for Event-B. We describe future work required to meet this goal
- …
