In my series of presentations of new projects at the Department of informatics time has come for HATS (Highly Adaptable and Trustworthy Software using Formal Methods).

HATS is a 4-year Integrated Project funded by the EU’s FP7 programme for future and emerging technologies (FET) called «Forever Yours». The objective of HATS is to develop a new method for designing highly adaptable software systems, focusing on system reliability and trustworthiness. Our project leader is Einar Broch Johnsen at the PMA-group.

Software families

The starting point for HATS is the development of software families, which are families of related software products. Members of software families share certain common features, but also differ in other features. For example, all the mobile phones of a manufacturer may share the software for telephony and have a common user interface, but the phones have different additional features such as MMS support, cameras, etc. These differences are often referred to as the variability of the software family.

Software evolution – in space and time

Another example of highly varying software is operating systems, which are designed to be configured and deployed on a wide range of architectures, from single machines to multi-core machines and distributed platforms. Current methods for the rigorous analysis of software mostly address single designs. In HATS, we address multiple designs by means of adaptability. In HATS, adaptability covers this variability in the design of software product, but in addition the evolution of a software product while it is in use; i.e., the reprogramming of features in a product at runtime.  Hence, adaptability in HATS addresses evolvability in both space and time.

Methods and models

The design method developed in HATS adds rigor to existing methods for the development of software families by developing formal models and analysis techniques for behavioral aspects of software systems: concurrency, modularity, integrity, security, and resource consumption. The modeling techniques developed in HATS lie in between structural models, expressed in languages such as UML and FDL, and implementation-oriented models, expressed in languages such as Spec# and Java+JML.

Models in HATS can be understood as abstract behavioral specifications: they are object-oriented and executable, yet abstract from many implementation details. This abstraction has two consequences. First, it makes the models easier to validate with respect to user requirements. Second, it means that the models can be adapted to different implementation scenarios, so family members may vary in deployment features such as security policies, resource requirements, concurrency and distribution, scheduling policies, etc. Inspired by variability in software families, the analysis techniques developed in HATS should also support variability in analysis; i.e., they should allow the modular and incremental analysis of software families.

Novel languages and correctness of software

Abstract behavioral specifications in HATS are expressed in the novel ABS language, which is based on the Creol language developed by the PMA group in Oslo. Creol has been shown to have advantages for verifying the correctness of software, compared to other object-oriented models. Furthermore, Creol supports the runtime reprogramming of software. With the extension to ABS, the HATS consortium extend our work on Creol to a large European effort, including the development of a range of analysis techniques for ABS models. In HATS, we want to demonstrate that this approach to software development is particularly suited for modular analysis and adaptable software, evolving in space as well as in time.

Partners

The HATS project is a collaboration between the following institutions: Chalmers Technical University (Gothenburg, Sweden), University of Oslo (Norway), Kungliga Tekniska Høgskolan (Stockholm, Sweden), Polytechnic University of Madrid (Spain), IMDEA Software (Madrid, Spain), University of Kaiserslautern (Germany), University of Bologna (Italy), Centruum voor Wiskunde en Informatica (Amsterdam, the Netherlands), Norsk Regnesentral (Oslo, Norway), Fredhopper (Amsterdam, the Netherlands), Fraunhofer Institute for Experimental Software Engineering (Kaiserslautern, Germany), Catholic University of Leuven (Belgium).