The HATS project develops a formal method for the design, analysis, and implementation of highly adaptable software systems that are at the same time characterized by a high demand on trustworthiness.
Adaptability includes two aspects: anticipated variability and evolvability, i.e., unanticipated change. The first is, to a certain extent, addressed in modern software architectures such as software product families. However, increasing product complexity (features, deployment) is starting to impose serious limitations. Evolvability over time is an even more difficult problem.
Current development practices do not make it possible to produce highly adaptable and trustworthy software in a large-scale and cost-efficient manner. The crucial limitation is the missing rigor of models and property specifications: informal or semi-formal notations lack the means to describe precisely the behavioral aspects of software systems: concurrency, modularity, integrity, security, and resource consumption.
Existing formal notations for specification of systems at the architectural or design level are mainly structural and lack the possibility to specify detailed behavior including datatypes, compositionality, concurrency. However, without a formal notation for the behavior of distributed, component-based systems it is impossible to achieve automation for consistency checking, enforcement of security, generation of trustworthy code, test case generation, specification mining, etc.
At the same time, formal specification and reasoning about executable programs on the implementation level is by now well understood for the sequential fragments of commercial languages such as Java or C and it is supported by tools (KeY, VCC, Krakatoa). The size and complexity of implementation languages, however, makes specification and verification extremely expensive. Even more difficult is formal specification of the functionality of parallel programs at the thread-level. Here, no scalable solution is in sight. In addition, re-use of formal specifications is very hard to achieve at the implementation level.
In conclusion, there is a gap between highly abstract modeling formalisms and implementation-level tools, which is visualized in Figure 1.1.
The HATS project addresses this modeling gap by providing these three ingredients:
One decisive aspect of the HATS project is to develop the analysis methods hand in hand with the ABS language to ensure feasibility of the resulting analyses.
As a main challenge in the development of the ABS language and HATS tool suite we identified (in addition to the technical difficulties) the need to make it relevant for industrial practice. Therefore, to keep the project firmly grounded, we orient the design of the ABS language and the HATS methodology along an empirically highly successful informal software development paradigm. In software product family-based development one separates Family Engineering, which includes feature modeling and library development, from Application Engineering, where code is derived via selection, instantiation and composition.
In HATS we turn software product family-based (SWPF) development into a rigorous approach based on formal specification.
Constructing a software family requires architecting both the commonality, that is, features, properties, and resources that are common to all products in the family, as well as the adaptability, that is, the varying aspects across the software family, in order to exploit them during the customization and system derivation process. As explained above, adaptability encompasses both anticipated differences among products in the family (variability), as well as the different products which appear over time due to evolving requirements (evolvability).
Ultimately, a model-centric development process for software product lines based on a uniform formal modeling framework such as HATS ABS can evolve into a single-source technology for engineering software product lines, see Figure 1.2. The integration of different modeling formalisms on the basis of a common formal semantics allows to analyze the consistency of different modeling concerns. Language concepts for artifact reuse provide a formal semantics for reuse such that consistency and correctness can be ensured by formal analysis techniques. Executable models of the product line as well as of individual products enable simulation and visualization techniques during all phases of family and application engineering. This helps to discover and correct defects early and permits rapid prototyping of products for communication with stakeholders.
Formal models allow automatic generation of test cases on the family level as well as on the product level. This is essential for reusability and maintainability. On the product level, test cases can be reused between different products that share common components. It is even possible to perform formal verification of critical system requirements already at early development stages. Evidence for the certifiability of derived products can be immediately provided. The modular and hierarchic structure of the product line model allows efficient validation and verification based on incremental and compositional reasoning. Code generation from formal models means to decrease time-to-market without sacrificing quality. Code generators can be verified and certified. The model-centric development approach supports product line maintenance and evolution.
The work package structure of HATS (see Figure 1.3) reflects the preceding discussion: the ABS language and methodology development, as well as the infrastructure and tool architecture are the platform for all other work and collected in Work Package 1. Work Packages 2 and 3 contain modeling/analysis work on variability and evolvability, respectively. Work Package 4 takes their input while investigating overarching aspects of systems trustworthiness. Work Package 5 validates the achievement of each milestone and injects the results of requirements analysis into ongoing theoretical efforts. The capability to model and analyze variability and evolvability of systems serves the underlying general goal to ensure the comprehensive and cross-cutting quality of trustworthiness (Work Package 4), including the aspects: security, resource guarantees, correctness, and auto-configuration.
During the second reporting period, from 1 March 2010 until 28 February 2011, the HATS project obtained a number of crucial and novel results that prove the viability of the overall approach. We highlight the most important ones:
These language extensions combine to describe an entire product line, where the behavior is written using Core ABS. A specific product selection results in a Core ABS program corresponding to the selected product. This approach makes it possible to use already now all the technologies available for Core ABS (see items 4 and 5 below) to analyse and derive actual products. The Full ABS language has a mathematically rigorous and unambiguous syntax and semantics.
In conclusion, the second project milestone, full modeling capabilities of the ABS language, has been achieved and will be validated in the next months.
Software systems provide important services and central parts of the infrastructure for modern economies and societies. The size and cost of these systems forbid to create them ``de novo'' again and again. To justify the huge investments, such systems need to live for decades, if not centuries. Already today and more so in the future, this requires to develop software systems that can cope with changes in the environment as well as with modified and new requirements. As it is impossible to anticipate all changes, software systems must be adaptable.
Major IT-trends under way pose new challenges: a prerequisite for cloud computing is the ability to abstract away from physical resource allocation, load distribution, the architecture of the execution platform, etc. This implies the need to specify intended behavior without referring to concrete resources. Likewise, the emergence of cyber-physical systems and the internet of things emphasize the need for abstract behavioral description of highly configurable and diverse systems.
The HATS ABS language and an accompanying tool suite facilitates to model and analyse precisely the behavior and functionality of highly configurable, distributed systems in an ``end-to-end'' manner. This means that not only the (concurrent) implementation of features is captured, but also the feature space and the dependencies among them. Furthermore, ABS includes language concepts to represent model evolution, e.g., due to changing requirements. In addition, it is possible to formally specify properties of systems modeled with ABS in form of behavioral contracts. The ABS modeling language aims to fill the gap between structural high-level modeling languages, such as UML, and implementation-close formalisms, including programming languages. It has the potential to become single-source technology in a suitable development process.
At this mid stage of the project we kept the promise to provide a new modeling language that has already been applied to a first, industrial case study and comes with a working tool set. A range of novel analysis and development techniques have been produced, several of which have been made to work in a distributed setting for the very first time.
The remaining stages of HATS will see the exploration of further techniques, including test case generation, model mining, various type systems, visualization, etc. Existing techniques will be matured and integrated, some of them will be scaled up to the family engineering level. After having consolidated the capability for modeling and analyzing variability, we will focus now more on evolvability. We will also start to evaluate the HATS Tool Suite in various industrial settings, for example, within the companies of the HATS end user panel.