Highly Adaptable and Trustworthy Software using Formal Methods (HATS)

This page describes the project Highly Adaptable and Trustworthy Software using Formal Methods (HATS).

Abstract

Software systems are central for the infrastructure of modern society. To justify the huge investments such systems need to live for decades. This requires software which is highly adaptable. Software systems must support a high degree of spatial variability to accommodate a range of requirements and operating conditions, and temporal evolvability to allow these parameters to change over time.

Current approaches to reusability and maintenance are inadequate to cope with the dynamics and longevity of future software applications and infrastructures, e.g. for e-commerce, e-health and e-government. At the same time, we rely increasingly on systems that provide a high degree of trustworthiness. The major challenge facing software construction in the next decades is high adaptability combined with trustworthiness.

A severe limitation of current development practices is the missing rigor of models and property specifications. Without a formal notation of distributed, component-based systems it is impossible to achieve automation for consistency checking, enforcement of security, generation of trustworthy code, etc. Furthermore, it does not suffice to simply extend current formal approaches. We propose to take an empirically successful, yet informal software development paradigm and put it on a formal basis.

Specifically, in HATS we will turn software product family (SWPF) development into a rigorous approach. The technical core of the project is an Abstract Behavioral Specification language which will allow precise description of SWPF features and components and their instances. The main project outcome is a methodological and tool framework achieving not merely far-reaching automation in maintaining dynamically evolving software, but an unprecedented level of trust while informal processes are replaced with rigorous analyses based on formal semantics.

Members

Prof. Dr. Reiner Hähnle, Chalmers Tekniska Högskola, Sweden
Wolfgang Ahrendt, Ph.D., Chalmers Tekniska Högskola, Sweden
Assoc. Prof. Dr. Einar Broch Johnsen, Universitetet i Oslo, Norway
Assoc. Prof. Dr. Martin Steffen, Universitetet i Oslo, Norway
Assoc. Prof. Mads Dam, Ph.D., Kungliga Tekniska Högskolan, Sweden
Dilian Gurov, Ph.D., Kungliga Tekniska Högskolan, Sweden
Prof. Karl Meinke, Kungliga Tekniska Högskolan, Sweden
Assoc. Prof. Dr. Germán Puebla, Universidad Politécnica de Madrid, Spain
Prof. Gilles Barthe, Ph.D., IMDEA Software, Spain
Prof. Manuel Hermenegildo, Ph.D., Universidad Politécnica de Madrid and IMDEA Software, Spain
Assoc. Prof. Elvira Albert, Ph.D., Universidad Politécnica de Madrid, Spain
Assoc. Prof. Puri Arenas, Ph.D., Universidad Politécnica de Madrid, Spain
Prof. Dr. Arnd Poetzsch-Heffter, AG Softwaretechnik, TU Kaiserslautern
Prof. Davide Sangiorgi, Ph.D., Università di Bologna, Italy
Prof. Cosimo Laneve, Ph.D., Università di Bologna, Italy
Prof. Frank de Boer, Ph.D., Centrum Wiskunde & Informatica, the Netherlands
Dr. Bjarte Østvold, Norsk Regnesentral, Norway
Dr. Anders Moen Hagalisletto, Norsk Regnesentral, Norway
Nikolay Diakov, Ph.D., Fredhopper, the Netherlands
Dirk Muthig, Ph.D., Fraunhofer-IESE
Prof. Dave Clarke, Ph.D., Katholieke Universiteit Leuven, Belgium
Prof. Dr. Frank Piessens, Katholieke Universiteit Leuven, Belgium
Prof. Tarmo Uustalu, Ph.D., Tallinna Tehnikaülikooli Küberneetika Instituut, Estonia
Dr. Peeter Laud, Tallinna Tehnikaülikooli Küberneetika Instituut, Estonia

Researchers in AG Softwaretechnik

Funding

The project is funded under the 7th Framework Programme of the European Commission within the Future and Emerging Technologies scheme.

Completion Status

The project started in March 2009 and completed in February 2013 with the predicate “excellent progress”. Yannick Welsch completed his Ph.D. defense in August 2013. Ilham Kurnia completed his Ph.D. defense in January 2015.