Abstract

Abstract

Abstract
Software Product Lines (SPLs) are families of systems that share a high number of common assets while differing in others. In component-based systems, components themselves can be SPLs, i.e., each component can be seen as a family of variations, with different interfaces and functionalities, typically parameterized by a set of features and a feature model that specifies the valid combinations of features. This paper explores how to safely replace such families of components with more refined ones. We propose a notion of refinement for Interface Featured Timed Automata (IFTA), a formalism to model families of timed automata with support for multi-action transitions. We separate the notion of IFTA refinement into behavioral and variability refinement, i.e., the refinement of the underlying timed automata and feature model. Furthermore, we define behavioral refinement for the semantic level, i.e., transition systems, as an alternating simulation between systems, and lift this definition to IFTA refinement. We illustrate this notion with examples throughout the text and show that refinement is a pre-order and compositional. © Springer International Publishing AG 2017.

Abstract
Featured Timed Automata (FTA) is a formalism that enables the verification of an entire Software Product Line (SPL), by capturing its behavior in a single model instead of product-by-product. However, it disregards compositional aspects inherent to SPL development. This paper introduces Interface FTA (IFTA), which extends FTA with variable interfaces that restrict the way automata can be composed, and with support for transitions with atomic multiple actions, simplifying the design. To support modular composition, a set of Reo connectors are modelled as IFTA. This separation of concerns increases reusability of functionality across products, and simplifies modelling, maintainability, and extension of SPLs. We show how IFTA can be easily translated into FTA and into networks of Timed Automata supported by UPPAAL. We illustrate this with a case study from the electronic government domain. © 2017, IFIP International Federation for Information Processing.

Abstract
Software Product Lines (SPLs) enable the development of families of software systems by taking advantage of the commonalities and variabilities of the members of the family. Despite its many advantages, it is an unexplored area in the electronic government domain, an area with evident families of services, and with high demands to develop faster and better services to citizens and businesses while reducing costs. This paper discusses the need of formal methods to model SPLs for such domain. It presents a case study of a family of public licensing services modeled in UPPAAL and based on Featured Timed Automata, an extension of Timed Automata to model real-time SPLs. It analyzes the suitability of FTA to model distributed families of services, while provides hints on a possible enrichment of FTA to better support modularization and compositionality of services. © 2017 IEEE.