Scientific Deliverables
The list of published scientific deliverables:
Deliverable 5.1 – Requirement Elicitation: elicits requirements representative to the theoretical and practical challenges that the envisioned method has to solve. We describe the selected requirements in form of detailed scenarios. Furthermore, the collected scenarios already may sketch the results of the envisioned solutions.
Deliverable 1.1.a – Report on the Core ABS Language and Methodology: Part A: contains the definition of the core ABS language, an abstract executable modeling language intended to form the basis for extensions later that will support evolvability, features, and further concepts relevant for the modeling and analysis of software families.
Deliverable 1.1.b – Report on the Core ABS Language and Methodology: Part B: reports the development of the HATS methodology as part of Task 1.1. Specifically this report describes a high level view of the HATS methodology, identifies relevant work tasks to each phase in the method and shows how work tasks’ contributions are related to the phases.
Deliverable 2.2.a – First Report on Feature Selection and Integration: consists of an investigation of possible techniques that may help bring the abstract notion of features down to the concrete level of program code. These include context oriented programming, multiple dispatch, trait-based programming and delta modeling. We summarize these techniques and refer to publications investigating them more thoroughly.
Deliverable 3.1.a – First Report On Evolvable Systems: reports on the investigations pursued in the setting of Task 3.1. The goal of this task is to analyze and model fundamental aspects of system and component evolution, formally pin down and compare the concepts, construct scenarios, and build formal execution models that can be subjected to evaluation, theoretical examination, comparison, and simulation.
Period 2
Deliverable 5.2 – Evaluation of Core Framework (supplementary models): tests the expressive power of the ABS language and HATS methodology in the case studies. The activities include extensive requirement analysis of the scenarios defined in Task 5.1. This task closely cooperates with the activities of Task 1.1, so that the requirement analysis drives the design of the innovative software development method developed in Task 1.1. It forms the basis for verification of Milestone M1.
Deliverable 4.2 – Resource Guarantees: reports on the basic framework for resource usage analysis (a.k.a. cost analysis) of ABS programs as well as a series of advanced issues which aim at improving the efficiency, the accuracy and the applicability of the proposed framework. Besides, we have studied the verification of the resource bounds obtained the resource usage analyzer using the KeY system.
Deliverable 1.2 – Full ABS Modelling Framework (supplementary code): reports on the definition of the full ABS language, an abstract executable modeling language intended for modeling and analysis of software product families.
Deliverable 2.2.b – Final report on Feature Selection and Integration: reports an investigation of possible techniques that may help bring the abstract notion of features down to the concrete level of program code. These include platform modeling, feature model- ing, views, feature Petri nets, context-oriented programming, multiple dispatch, trait-based programming and delta modeling. As a main contribution of this deliverable, we propose a generalization of delta modeling. The approach is influenced earlier delta modeling publications, the AHEAD methodology and trait-based pro- gramming. The published delta modeling formalism gives rise to a new design methodology, which is to become part of the HATS methodology.
Deliverable 2.5 – Verification of Behavioral Properties: reports on a program logic for the HATS modeling language ABS. The program logic is based on symbolic execution and used to reason about functional behavior of ABS programs. We present further work on possible optimization concerning compositionality and full abstraction which promise a significantly better automation. We report further on our results concerning incremental verification and introduce a variety of techniques suitable to reduce redundancy and minimize the need for redoing analyses when an ABS program is changed locally. Also an analysis to detect and prove absence of dead-locks is presented.
Deliverable 3.1.b – Final report on Evolvable Systems: reports on the investigations pursued in the setting of Task 3.1. The goal of this task is to analyze and model fundamental aspects of system and component evolution, formally pin down and compare the concepts, construct scenarios, and build formal execution models that can be subjected to evaluation, theoretical examination, comparison, and simulation.
Deliverable 3.4 – Evolvability at Bytecode Level: This deliverable reports on the development of runtime code evolution at the bytecode level through the use of software transformation techniques in the style of monitor inlining. The deliverable also reports on an experiment showing how deductive techniques can be used to automatically refine ABS models into bytecode.
Period 3
Deliverable 2.1 – Configuration Deployment (Paper Appendix): The report develops the lowest levels of a flexible architecture upon which to base models in ABS, an abstract executable modeling language intended for modeling and analysis of software product families. This lowest level of ABS models captures deployment concerns, such as the underlying concurrency and interaction models as well as an abstract failure model for the language, are considered.
Deliverable 2.3 – Testing, Debugging and Visualization (Paper Appendix): we present the unit testing framework ABSUnit for the Abstract Behavioural Language (ABS). ABSUnit can be used to write and execute test cases easily. Failed tests can be used to guide the debugging process. We investigate further how to generate test suites of significant quality and size. Therefore we follow two different approaches: glassbox test generation and blackbox test generation. For the first approach we present also an implemented tool aPET which generates tests for an ABS model in the ABSUnit framework.
Deliverable 2.4 – Types for Variability (Paper Appendix): The task addresses the objective of achieving lightweight verification mechanisms means of type systems. The challenge here is to take into account the novel features of the ABS language, notably features related to variability, dynamicity, and use of components.
Deliverable 3.2 – Model Mining (Paper Appendix): This deliverable investigates various algorithms and techniques to build abstract models from concrete inputs in a (partly) automated fashion. Our common name for these techniques is model mining. The motivation for model mining is to assist developers in writing models of their code or models describing the domain in which the developers are working. Mined models may then be used for analysis, understanding or reorganising a product line. Our work on model mining builds on and extends results from machine learning, formal specification, and program analysis.
Deliverable 4.1 – Security (Paper Appendix, Case Study): This deliverable reports on mechanisms which ensure confidentiality policies for long-lived and complex software. It consists of two parts: The first part of the deliverable reports on the development, and on the evaluation on a common case study in ABS, of three complementary language-based methods (type systems, logics, and dynamic methods) for enforcing confidentiality policies for ABS applications, both at the ABS level and at the bytecode level. The second part of this deliverable reports on the automatic generation of protocol implementations in ABS. The prototype has been successfully evaluated on a large set of protocols.
Deliverable 5.3 – Evaluation of Modeling (Paper Appendix, supplementary models): This deliverable evaluates developed modeling techniques using various case-studies. It is also a followup of Deliverable 5.2.
Period 4
Deliverable 1.3 – Analysis (Paper Appendix) reports on the results achieved in Task 1.3 “Analysis” which was concerned with the development and documentation of a workflow driven, coherent user interface as well as the design of parametrizable analyzes. The document is composed of the user interface guideline documentation which is designed as a living document to be updated regularly and the presentation of a pluggable type checking extension that introduces location types and features an innovative user interface solution to present inferred types. Finally, we present a framework that provides a common fundament for the development of ABS language extensions, analyses and compilers. The framework allows in particular rapid prototyping of tools.
Deliverable 2.6 – Refinement and Abstraction (Paper Appendix) describes various forms of refinement and abstraction in the context of the ABS modeling framework. As main result, the deliverable presents: (i) an approach to show behavior-preserving refinements at the level of class libraries, (ii) a deductive compilation approach that refines an ABS model to Java bytecode while provably preserving the ABS model’s properties, and (iii) a compositional notion of refinement for timed I/O automata with deadlines applied to the ABS setting.
Deliverable 1.4 – ABS System Derivation and Code Generation (Paper Appendix) presents an update on the Java backend of the ABS compiler first described in Deliverable D1.2, emphasizing the new foreign function interface. We report on a new Scala backend that is based on the Akka actor library of Scala and the continuations facility and maps the ABS concurrency model in an elegant way to high-level concurrency mechanisms of Scala. This backend supports distributed execution of ABS code. On subsets of ABS and Scala (core ABS and a small functional language with delimited continuations) we demonstrate that the compilation scheme of this backend is correct in a mathematically precise sense and also report on results of formalizing this proof in the proof assistant Agda. We give an update on the support of delta modelling in ABS for software product lines, describing the changes and additions that we have introduced into the syntax and semantics of ABS deltas wrt. the initial description in Deliverable D1.2 We describe a product configurator helping the user to select a product (i.e., produce a PSL specification) that satisfies the given customer requirements while conforming to the feature model of the product line
Deliverable 2.7 – Analysis Final Report: In this deliverable we provide a concise overview on selected formal
analysis methods for the ABS language. The different analyses cover testing, automated test generation, runtime assertion checking, functional verification and contract based deadlock analysis.
Deliverable 3.3 – Hybrid Analysis for Evolvability (Version with Papers in Appendix, Paper Appendix) reports on mechanisms for expressing the evolution of systems in the language ABS and for the analysis of such systems. As the full details of evolving systems are not known at compile time or because the configuration is based on runtime decisions, the analysis consists of a combination of static and dynamic techniques. This delivery also describes MetaABS, a meta-programming facility for ABS, and the new dynamic back end upon which it is based. MetaABS provides a framework for adapting the ABS runtime from within the language itself, allowing many ABS extensions and checking mechanisms to be implemented without having to change the compiler or the backend.
Deliverable 4.4 – Auto Configuration and Quality Variability (Appendix with generated code) reports on (i) a visualizer for the text-based feature specification language muTVL. We specify quality variability modeling approach in HATS and present a configurator that provides functional auto configuration. In addition to that we present how in the presence of desired quality analyzers for different quality metrics, quality aware configuration can be achieved; (ii) performance-aware configuration which provides awareness of the performance throughout the configuration process. The results obtained and extended version of the resource analyzer COSTABS can be used the ABS product configurator. Last, but not least we report (iii) on modeling and analysing the security variability of computer systems using security features.
Deliverable 1.5 – ABS Tool Platform and Methodology has two key contributions: First, an integrated tool architecture, that is, an architecture for the set of tools developed in the HATS project, and second, the HATS methodology, which describes how to use these tools to build product line software. The HATS methodology presented here is an update of the previous version from Deliverable D1.1b.
Deliverable 3.5 – Autonomous Evolving Systems (D3.5 with paper appendix, Paper Appendix) eports on several lines of work that explore the use of the ABS language and framework to support software evolvability, software adaptation, and auto-configuration at runtime, with the goal of producing software systems that evolve in a goal-driven and, as far as possible, autonomous manner.
Deliverable 3.6 – Evolvability Final Report (D3.6 with paper appendix, Paper Appendix) presents three new work items that in various ways address the problem of dynamically evolvable software, we report on a journal special issue in progress on the topic of evolvable software, and we briefly summarize and discuss the achievements of HATS WP 3 more broadly.
Deliverable 4.3 – Correctness (Paper Appendix) reports on analysis of correctness of systems modeled and realized with the HATS methodology. Several different kind of analyses are presented that cover a wide range of techniques like functional verification, deadlock analysis, verification on the family level and more.
Deliverable 5.4 – Evaluation of Tools and Techniques (Paper Appendix) presents the evaluation of tools and techniques developed in the HATS project via case studies. The selection of tools and techniques has been made specifically to address a wide range of static and run-time analysis techniques, and to address both functional and non-functional properties.
Dissemination and Project Management
Deliverable 6.4 – Dissemination Plan: This document is the current version of the dissemination plan. It is meant to be a living document that is updated regulary during the whole project duration but at least once in each reporting period. Over time, experiences in disseminating the HATS project results and new dissemination opportunities in general will require changes to the dissemination plan.
Deliverable 7.2.a – Biannual Management Report (t6, t12, t18, t24, t30, t36, t42): The biannual management report is given the project coordinator as presentation synchronized with the annual meeting and project review.
Deliverable 7.3 – Project Quality Plan: This document is the current version of the project quality plan detailing the measurements taken to ensure high scientific quality. It is meant to be a living document that is updated regularly during the whole project duration but at least once in each reporting period. Over time, experiences in conducting the HATS project will prompt changes to the project quality plan.
Period 2
Deliverable 6.2 – Exploitation strategy: presents the partial result of Task 6.2 (Exploitable Strategy), which is concerned with the preparation of a technology usage plan for the HATS project. The goal of this task is to maximize the opportunities for market adoption of the project results
Period 4
Deliverable 6.2.b – HATS Technology Usage Plan presents the results of Task 6.2 (Exploitable Strategy), which is concerned with the preparation of a technology usage plan for the HATS project. The goal of this task was to maximise the opportunities for market adoption of the project results.
Deliverable 6.3 – Training Material (requires login) consists of two parts: (i) The LNCS book with a series of tutorials that have been held at the HATS International Summer School 2012; and (ii) a website linking the most relevant training material produced in the HATS project. The internal website is at the moment non-public and requires a log in as the draft versions of the LNCS book are linked for the moment. The public website of the summer school is accessible.
