68,510 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
No.579 Helen Julene Butler
No full textTranscript (52 pages) of interview by Becky B. Lloyd with Helen Julene Butler on March 27, 2010Butler (b. 1948) was born in Price, Utah. Her family moved to Dragerton (East Carbon) in 1950. She contracted polio at age three and a half years of age in August 1951. She was transported to the Salt Lake County Hospital, where she remained in isolation for three weeks. She was transferred to Holy Cross Hospital in Salt Lake City and was treated there from September to December of that year. She entered Shriners Hospital in Salt Lake City in early 1952 and stayed there for therapy for eighteen months. She thereafter periodically returned to Shriners for lengthy stays, receiving various surgical procedures-thirteen in all-until she was sixteen years old. Ms. Butler recalls time spent in the hospital, details of her surgeries, and various treatments and therapies received. Butler was paralyzed in all four limbs at the time of her illness. She recovered some use of her left side. She was outfitted with full-length leg braces and crutches and has used a wheelchair in public since 1954. Around her home she used crutches and eventually shed first the left leg brace, then later the right. Ms. Butler discusses post-polio syndrome effects, difficulties and necessary adjustments. She has exclusively used a wheelchair since 2002. Butler received both a master\u27s degree and a PhD in Library Science and currently serves as the Director of the Brigham Young University Library. This interview is part of the Polio Oral History Project. Interviewed by Becky B. Lloyd
Evidence for the decay B0→J/ψω and measurement of the relative branching fractions of meson decays to J/ψη and J/ψη′
No full textFirst evidence of the B 0 → J / ψ ω decay is found and the B s 0 → J / ψ η and B s 0 → J / ψ η ′ decays are studied using a dataset corresponding to an integrated luminosity of 1.0 fb -1 collected by the LHCb experiment in proton-proton collisions at a centre-of-mass energy of sqrt(s) = 7 TeV. The branching fractions of these decays are measured relative to that of the B 0 → J / ψ ρ 0 decay:frac(B (B 0 → J / ψ ω), B (B 0 → J / ψ ρ 0)) = 0.89 ± 0.19 (stat) - 0.13 + 0.07 (syst),frac(B (B s 0 → J / ψ η), B (B 0 → J / ψ ρ 0)) = 14.0 ± 1.2 (stat) - 1.5 + 1.1 (syst) - 1.0 + 1.1 (frac(f d, f s)),frac(B (B s 0 → J / ψ η ′), B (B 0 → J / ψ ρ 0)) = 12.7 ± 1.1 (stat) - 1.3 + 0.5 (syst) - 0.9 + 1.0 (frac(f d, f s)), where the last uncertainty is due to the knowledge of f d / f s, the ratio of b-quark hadronization factors that accounts for the different production rate of B 0 and B s 0 mesons. The ratio of the branching fractions of B s 0 → J / ψ η ′ and B s 0 → J / ψ η decays is measured to befrac(B (B s 0 → J / ψ η ′), B (B s 0 → J / ψ η)) = 0.90 ± 0.09 (stat) - 0.02 + 0.06 (syst)
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
- …
