Project Objectives

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:

1. An object-oriented, executable modeling language for adaptable, concurrent software components: the Abstract Behavioral Specification (ABS) language. The goal is to allow formal specification of concurrent, component-based systems on a level that abstracts away from implementation details but retains essential behavioral properties: concurrency model, component structure, execution histories, and datatypes. The ABS language has a formal operational semantics which is the basis for unambiguous usage and rigorous analysis methods. The ABS language closes gap in modeling formalisms, see Figure 1.1
2. A tool suite for analysis and development of ABS models as well as executable code (for example, in Java) derived from those:
   

   Hard methods

   typically strive for completeness or full coverage and require expert knowledge in the form of user interaction or detailed specifications. These include feature consistency, data integrity, security, property verification, and code generation.

   Soft methods

   typically are incomplete or non-exhaustive, but do not presuppose expert knowledge and are fully automatic. These include visualization, test case generation, specification mining, and type checking.

   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.

3. A methodological and technological framework that integrates the HATS tool architecture and the ABS language.

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 in the HATS Project

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.

Main Results Achieved

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:

1. The most important achievement is clearly the definition of the Full ABS language which allows to model highly adaptable, concurrent software systems. Based on the Core ABS language which was the major result of the first project year, we added the following components:
   
   1. The Micro Textual Variability Language (μTVL) is a feature description language that allows to express variability at the level of feature models.
   2. The Delta Modeling Language (DML), based on the paradigm of delta-oriented programming (see item 2 below), expresses the code-level variability required to model software product lines.
   3. The Product Line Configuration Language (CL), links a feature model and delta modules together, and forms the top level specification of an entire product line.
   4. The Product Selection Language (PSL), expresses products by providing feature and attribute selection along with initialization code for the product.

   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.

2. For the integration of features in the ABS language, we studied various formalisms and mechanisms; e.g., traits, context-oriented programming techniques, and delta modeling. We identified delta modeling as the most promising approach to bridge the gap between features and ABS code. In delta modeling one distinguishes between a core implementation, containing the code common to each product, and deltas, containing code specific to some feature configuration(s).
3. The backbone of the HATS ABS Tool Suite (consisting of a parser, type checker, enriched editor, and simulator) has been fully implemented to cover the complete Core ABS language and is fully integrated into the popular Eclipse development platform. First command line tools with support for delta modeling and therewith Full ABS have been implemented.
4. A number of analysis methods have been established for Core ABS as target language:
   
   1. A compositional program logic that makes it possible to prove functional properties of ABS models by a combination of symbolic execution and rely-guarantee reasoning.
   2. An analysis technique that detects potential deadlocks in Core ABS models.
   3. A fully automatic resource usage analyser for Core ABS programs that gives runtime estimations in the form of (asymptotic) lower and upper bounds. It is the first automatic resource analyser for concurrent programs and it has been already implemented. The technique is parametric with respect to different cost models.
5. A number of programming language-based techniques and tools have been established for Core ABS as target language:
   
   1. Code generation for Maude and Java bytecode, fully supported by the HATS ABS Tool Suite.
   2. An inlining algorithm for security monitors into concurrent Core ABS programs.
   3. An architectural component model that supports evolvability of ABS models.
   4. A novel rule-based, deductive approach for verified and optimized compilation of Core ABS into bytecode.
6. Three major case studies (Virtual Office of the Future, CoCoME Cash Desk product line, Fredhopper Access Server) have been modeled in Core ABS. Parts of the Fredhopper Access Server, a commercial server program used in web merchandising even has been modeled in Full ABS. The analysis of the case studies led to considerably refined requirements on the ABS language and influenced the design of Full ABS.

In conclusion, the second project milestone, full modeling capabilities of the ABS language, has been achieved and will be validated in the next months.

Impact

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.