2,682 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/
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
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
Feature-Oriented Modelling Using Event-B
No full textEvent-B is a formal method for specification and verification of reactive systems. Its Rodin toolkit provides comprehensive support for modelling, refinement and analysis using theorem proving, animation and model checking. There has always been a need to reuse existing models and their associated proofs when modelling related systems to save time and effort. Software product lines (SPLs) focus on the problem of reuse by providing ways to build software products having commonalities and managing variations within products of the same family. Feature modelling is a well know technique to manage variability and configure products within the SPLs. We have combined the two approaches to formally specify SPLs using Event-B. This will contribute the concept of formalism to SPLs and re-usability to Event-B. Existing feature modelling notations were adapted and extended to include refinement mechanism of Event-B. An Eclipse-based graphical feature modelling tool has been developed as a plug-in to the Rodin platform. We have modelled the "production cell" case-study in Event-B, an industrial metal processing plant, which has previously been specified in a number of formalisms. We have also highlighted future directions based on our experience with this framework so far
Transforming timing diagrams into knowledge acquisition in automated specification
No full textRequirements engineering is an important part of developing programs. It is an essential stage of the software development process that defines what a product or system should to achieve. The UML Timing diagram and Knowledge Acquisition in Automated Specification (KAOS) model are requirements engineering techniques. KAOS is a goal-oriented requirements approach while the Timing diagram is a graphical notation used for explaining software timing requirements. KAOS uses linear temporal logic (LTL) to describe time constraints in goal and operation models. Similarly, the Timing diagram can describe some temporal operators such as X (next), U (until) and R (release) over some period of time. Thus, our aim is to use the Timing diagram to generate parts of a KAOS model. In this paper we demonstrate techniques for creating a KAOS goal model from a Timing diagram. The Timing diagram which is used in this paper is adapted from the UML 2.0 Timing diagram and includes features to support translation into KAOS. We use a case study of a Lift system as an example to explain the translation processes described here
Timing diagrams requirements modeling using Event-B formal methods
No full textTiming diagrams provide an intuitive graphical specification for time constraints and causal dependencies between a system’s objects. Such a view can provide useful insight during Requirements Engineering (RE). Formal Modeling techniques allow abstract system level models to be explored in revealing detail and provide feedback via verification and validation methods such as proofs of consistency, model checking and animation. Here, we bring these two modelling approaches together. In particular we present techniques to extend a graphical modeling capability for formal modeling into the real-time domain by developing a Timing diagram view for the Event-B formal method and its graphical front-end, UML-B. Translation schemes to Event-B and UML-B are proposed and presented. A case study of a lift system is used to demonstrate the translation in practice
Mike Olszewski Interview, 2009
No full textMike Olszewski is a newscaster for WKSU-FM and a professor of communications at Kent State University and the University of Akron, as well as the author of several books. He was born in Cleveland in 1953. The interview discusses his childhood, racial issues, music, and the media
Mike Olszewski Interview, 2009
No full textMike Olszewski is a newscaster for WKSU-FM and a professor of communications at Kent State University and the University of Akron, as well as the author of several books. He was born in Cleveland in 1953. The interview discusses his childhood, racial issues, music, and the media
Dr. Mike Davison – Faculty Author Interview
No full textDr. Mike Davison, Professor of Music, discusses his documentary film, Cuba: Rhythm in Motion. This dynamic film captures the joy of making music in Cuba, an island that Dr. Davison has visited numerous times with his students. The contrasting yet intertwined histories of Cuban and American music are traced and illustrated with extensive performance footage. A DVD of Cuba: Rhythm in Motion is available in Parsons Music Library
Mike Nichols Oral History
No full textOral histories created by University of Kansas students, staff and faculty as part of the Religion in Kansas Project are archived at http://hdl.handle.net/1808/12524 in KU ScholarWorks, the digital repository of the University of Kansas.Oral history interview with Mike Nichols conducted by Diana Brown at the Latte Land coffee shop in Kansas City, Kansas, on July 6, 2014. Mike is the author of The Witches’ Sabbats, taught classes on Paganism for decades, and owned The Magic Lantern occult book shop in Kansas City in the 1980s; this interview discusses those experiences. This interview was conducted for the Religion in Kansas Project as part of a summer fieldwork internship funded by the Friends of the Department of Religious Studies.Friends of the Department of Religious Studie
- …
