Enhancing Formal Methods with Feature Models in MDD

Enhancing Formal Methods with Feature Models in MDD

Felice Laura (Universidad Nacional del Centro de la Provinicia de Buenos Aires, Argentina), Ridao Marcela (Universidad Nacional del Centro de la Provinicia de Buenos Aires, Argentina), Mauco María Virginia (Universidad Nacional del Centro de la Provinicia de Buenos Aires, Argentina) and Leonardi María Carmen (Universidad Nacional del Centro de la Provinicia de Buenos Aires, Argentina)
Copyright: © 2015 |Pages: 16
DOI: 10.4018/978-1-4666-5888-2.ch700
OnDemand PDF Download:
List Price: $37.50

Chapter Preview



As formal methods offer a wide spectrum of possible paths towards designing high-quality software, they are receiving increasing attention in the academia and the industry, especially where safety or security is important (Streitferdt; Riebisch & Philippow, 2003). By using formal methods early in the software development process, ambiguities, incompleteness, inconsistencies, errors, or misunderstandings can be detected, avoiding their discovery during costly testing and debugging phases.

A well-known formal method is the RAISE Method (George, Haxthausen, Hughes, Milne, Prehn, & Pedersen, 1995), which has been used on real developments (Dang Van, George, Janowski, & Moore, 2002). This method includes a large number of techniques and strategies for doing formal development and proofs, as well as a formal specification language, the RAISE Specification Language (RSL) (George, Haff, Havelund, Haxthausen, Milne, Nielsen, Prehn, & Wagner, 1992), and a set of tools to help writing, checking, printing, storing, transforming, and reasoning about specifications (George, 2001). However, formal specifications are unfamiliar to stakeholders, whose active participation is crucial in the first stages of software development process to understand and communicate the problem. This also holds in Domain Analysis (DA) (Kang, Kim, Lee, & Kim, 1998), because its first stage is to capture the knowledge of a particular domain, making necessary to have a model that is comprehensible by software engineers and domain experts.

A way to contribute to bridge this gap is to work in the integration of a DA phase into the RAISE Method, in order to specify a family of systems to produce qualitative and reliable applications in a domain, promoting early reuse and reducing development costs.

The use of Feature Models (FM) (Eisenecker & Czarnecki, 2000) to represent the DA facilitates the customization of software requirements. In DA, features and relationships between features (called Domain Feature Model) are used to organize the requirements of a set of similar applications in a software domain.

In this article, an informal strategy which starts by defining this feature model following one of the several proposals that facilitate the construction of FM: Feature-Oriented Reuse Method (FORM) (Kang, Kim, Lee, & Kim, 1998), is presented. Then, this model is transformed, by means of a set of manual heuristics, into a RSL specification that can be later developed into a more concrete one to automatically obtain a prototype to validate the specification by using the RAISE Tools. The use of FM is motivated by the fact that stakeholders often speak about product characteristics in terms of “features the product has and/or delivers,” using them to communicate their ideas, needs, and problems.

In order to fit the main proposal of enhancement of formal developments with the RAISE Method into Model Driven Development (MDD) paradigm (Mellor, Clark, & Futagami, 2003), an ATL (Atlas Transformation Language) (ATL, 2012) transformation which allows the automatic derivation of a first abstract RSL specification of a domain starting from a Feature Model has been developed. The ATL rules define how features and relationships between them (the source model) are matched and navigated to produce the RSL specification (the target model) (Felice, Ridao, Mauco, & Leonardi, 2011). The rules follow closely the principles proposed in the RAISE Method, so this first and still incomplete specification may be later developed into a more concrete one following the RAISE Method steps. With a concrete specification, the RAISE tools can be used to automatically obtain a quick prototype and get a feeling of what the specification really does.

Key Terms in this Chapter

Domain Analysis (DA): A process that affects the maintainability, usability, and reusability of a system and includes: domain definition; domain analysis; the development of a domain architecture; the construction of components (specifications, design, documentation).

Feature Modeling: The process where it is documented only functional features but also implementation features, various optimizations, alternative implementation techniques, and so on.

RSL Specification: A collection of modules. A module is basically a named collection of declarations; it can be a scheme or an object. Each module should have only one type of interest, defining the appropriate functions to create, modify, and observe values of the type.

Feature: Anything users or client programs might want to control about a concept. a coherent and identifiable bundle of system functionality that helps characterize the system from the user perspective. a prominent or distinctive user-visible aspect, quality, or characteristic of a software system or systems.

MDD: A new software development paradigm that stresses the use of models in the software development life cycle and argues automation via model execution, model transformation and code generation techniques.

RAISE Method: A formal method. It is an acronym for “Rigorous Approach to Industrial Software Engineering.” It provides facilities for the industrial use of Formal Methods in the development of software systems. RAISE consists of the RAISE Specification Language (RSL) which is a powerful specification and design language and a comprehensive development method.

Atlas Transformation Language: ( ATL): A model transformation language and toolkit. It provides ways to produce a set of target models from a set of source models.

Complete Chapter List

Search this Book: