TopIntroduction
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.