HATS: Highly Adaptable and Trustworthy Software using Formal
Models
===> New! Information
on Kick-Off Meeting in Bologna 9-11 March 2009
<===
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.
|