HATS - a formal software product line engineering methodology

Trust in software is typically achieved via stabilization efforts over long periods of use. Adaptation to changing circumstances, however, often requires substantial changes to the software. Changing a software system using standard manufacturing processes often results in quality regressions, invalidating trust. Formal methods provide a means for guaranteeing various properties of a software system that increase its trustworthiness. The HATS methodology aims to integrate formal methods for modeling changes of software systems in terms of variability and evolution, while preserving trustworthiness properties. This paper outlines how different formal methods are extended and integrated to build an industrially viable Software Product Line Engineering method for manufacturing highly adaptable and trustworthy software.