Highly Adaptable and Trustworthy Software using Formal Models

George Fox Lt2
Wed, 27/07/2011

Many software development projects make strong demands on the adaptability and trustworthiness of the developed software, while the contradictory goal of ever faster time-to-market is a constant drum beat. Adaptability includes two aspects: anticipated variability as well as evolvability, i.e., unanticipated change. The first is addressed, to a certain extent, in development methods such as software product line engineering. However, increasing product complexity, e.g., coming from a large number of possible product features or different deployment options, is starting to impose serious limitations. Evolvability over time is an even more difficult problem that is far from any satisfying solution, in particular in the context of system diversity.

Current development practices do not make it possible to produce highly adaptable and trustworthy software in a large-scale and cost-efficient manner. Adaptability and trustworthiness are not easily reconciled: unanticipated change, in particular, requires freedom to add and replace components, subsystems, communication media, and functionality with as few constraints regarding behavioral preservation as possible. Trustworthiness, on the other hand, requires that behavior is carefully constrained, preferably through rigorous models and property specifications since informal or semi-formal notations lack the means to describe precisely the behavioral aspects of software systems: concurrency, modularity, integrity, security, resource consumption, etc.

Existing notations for system specification at the modeling level, such as architectural languages, visual design languages, or feature description languages, are mainly structural and lack adequate means to specify detailed behavior including datatypes, compositionality, or concurrency. But without a formal notation for the behavior of distributed, component-based systems, it is impossible to automate behavioral verification, enforcement of security, trusted code generation, resource analysis, 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 even for commercial languages such as Java, C, or C#, and reasonably well supported by tools. The size and complexity of these languages, however, makes specification and verification extremely expensive. In addition, re-use of specification and verification efforts is very hard to realize. In conclusion, there is a gap between highly abstract modelling formalisms and implementation-level tools.

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. The core of the method is an object-oriented, executable modeling language for adaptable, concurrent software components: the Abstract Behavioral Specification (ABS) language. Its design goal is to permit formal specification of concurrent, component-based systems on a level that abstracts away from implementation details, but retains essential behavioral properties, thus, closing the mentioned gap.

HATS Research Project Symposium Session (Part 1) at ECOOP 2011 from Phil Greenwood on Vimeo.

HATS Research Project Symposium Session (Part 2) at ECOOP 2011. from Phil Greenwood on Vimeo.

Target Audience: 

The target audience comprises anyone with a professional interest in model-centric development of large-scale distributed, object-oriented systems. Both, academic and industrial participants, are equally in the focus of the presentation which will be accessible to a wide audience:

  1. Academic researchers working in concurrent programming, modeling languages, formal specification/verification, and software evolution.
  2. Industrial researchers and practitioners dealing with highly configurable software that must be adapted to varying scenarios, specifically, people who are working in software product line engineering and people from industries where high trustworthiness of software is an issue. The ABS language and tool set will also be interesting for developers and users of tools for model-centric development.
  3. Academic instructors who wish to teach a modern, OO concurrent programming language that is more abstract and less complex than, e.g., Java or C++. ABS has a uniform formal semantics and comes with a compiler, code generators, simulators, and a debugger, which are all usable either as standalone tools or as Eclipse plugins.
Outline of Sessions: 
  • Morning (11am -- 12.30pm): ABS Tutorial and Demo
  • Afternoon (2pm -- 3pm): Presentations (20 min each):
    • From Features to Product Lines
    • Compositional Verification of Product Lines
    • Evolution and Monitoring
  • 3pm -- 3.30pm: Discussions and Networking
HATS.pdf213.36 KB