1,721,028 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
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
Java implementation platform for the integrated state- and event-based specification in PROB
Full text linkPROB 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
Formal modelling and verification of population protocols
No full textThe population protocols of Angluin, Aspnes et al provide a theoretical framework for computability reasoning about algorithms for Mobile Ad-Hoc Networks (MANETs) and Wireless Sensor Networks (WSNs). By developing two example protocols and proving convergence and reachability results using the Event-B/RODIN and TLA frameworks, we explore the potential for formal analysis of these protocols
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
Modelling the pacemaker in event-B: towards methodology for reuse
No full textThe cardiac pacemaker is one of the system modelling problems posed to the Formal Methods community by the Grand Challenge for Dependable Systems Evolution. The pacemaker is an intricate safety-critical system that supports and moderates the dysfunctional heart's intrinsic electrical control system. This paper focusses on (i) the problem (requirements) domain specification and its mapping to solution (implementation) domain models, (ii) the significant commonality of behaviour between its many operating modes, emphasising the potential for reuse, and (iii) development and verification of models.We introduce the problem and model three of the operating modes in the problem domain using a state machine notation. We then map each of these models into a solution domain state machine notation, designed as shorthand for a refinement-based solution domain development in the Event-B formal language and its RODIN toolkit
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
Model Based Engineering of Specifications by Retrenching Partial Requirements
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 a 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. After a presentation of the basic ideas of retrenchment, a simple telephone system feature interaction case study is given to illustrate how retrenchment can relate incompatible partial models to a more definitive consolidated model during the development of the contracted specification
Software Evolution with Refinement and Retrenchment
No full textGiven a record of the derivation of a component from its specification, and a new, changed specification, we can compare the two specifications and use the differences between them as a basis for revising the derivation of the component and attempt to discharge the resulting proof obligations. This is essentially the way that program refinements are modified by hand, and could be supported by a refinement tool. Alternatively, we might describe the new specification by combining the original specification and a description of the new behaviour required using combinators similar to schema conjunction and disjunction in Z. This approach has been explored in the context of the refinement calculus, and also in a relational setting. Independently of this revision-based and constructive work, another potential formal approach to the evolution of specifications has recently emerged. Retrenchment is a generalisation of classical refinement which was proposed to extend the reach of formal verification to applications too demanding to be described, computationally, in terms of refinement. Recent work has proposed the integration of these constructive and retrenchment approaches. This paper reports on initial work investigating the construction of evolutions using these constructive and retrenchment approaches. In special cases the evolution transformation may be a refinement. More widely applicable will be certain specification combinators and constructors. Finally, as the most general relation between specifications, retrenchment will be applicable to any evolution; the work will be in establishing how to use it to preserve structure in a useful way
- …
