ASTEC Final Report 1995-2005

Appendix 3

Projects, their acronyms, names, leaders, goals, time period, volume and publication rate.

A total of 21 projects were carried out by 17 project leaders, the cost were 144 MSEK, 266 publications were produced. Results from the projects is presented in the section Technical and scientific results

Analysing ERLANG/OTP systems

Bengt Jonsson lead the project that were active the years 2001-2002 it had a volume of 1,2 MSEK, which corresponds to 1% of the total project volume, 4 publications were produced of which one was a PhD thesis.

Goal: To support the analysis of the ability of ERLANG systems to tolerate and recover crashes of individual processes.

ARENA (ASTEC Requirement Engineering Approach)

Roland Bol lead the project that were active the years 1995-1998 it had a volume of 4,7 MSEK, which corresponds to 3% of the total project volume, 4 publications were produced one was a MSc thesis.

Goal: To improve the usefulness of the resulting requirements specification to design, formal verification and testing.

Auto

Wang Yi lead the project that were active the years 1998-2000 it had a volume of 3,4 MSEK, which corresponds to 2% of the total project volume, 19 publications were produced of which one was a PhD thesis.

Goal: A design methodology for embedded real-time systems. Development of a design method for Automotive Real-Time Applications.

BOOM (Formal Specification of Object-Oriented Modeling Concepts)

Joachim Parrow lead the project that were active the years 1995-1998 it had a volume of 3,7 MSEK, which corresponds to 3% of the total project volume, 3 publications were produced of which one was a PhD thesis.

Goal: The major goal was to develop a meta-language, named ODAL, in which the semantics of object-oriented specification notations can be given.

BUS

Wang Yi lead the project that were active the years 1999-2000 it had a volume of 1,8 MSEK, which corresponds to 1% of the total project volume, 2 publications were produced.

Goal: This project was a case study. It aimed at modeling and analyzing a bus protocol, developed and implemented by ABB Automation Products, using state-of-the-art model checking tools, primarily UPPAAL.

Erl Ver (Erlang Verification)

Mads Dam lead the project that were active the years 1997-2001 it had a volume of 9,2 MSEK, which corresponds to 6% of the total project volume, 22 publications were produced of which one was a PhD thesis and 2 MSc theses.

Goal: A Verification Method for Erlang, developing a general verification tool for the Erlang programming language based on a combination of model checking, compositional and symbolic techniques.

HIPE (High Performance Erlang)

Kostis Sagonas, Mikael Pettersson lead the project that were active the years 1996-2005 it had a volume of 28,1 MSEK, which corresponds to 20% of the total project volume, 49 publications were produced of which one was a PhD thesis, 2 Licentiate theses and 5 MSc theses.

Goal: To develop techniques for efficient compilation of concurrent functional programming languages.

PLEX

Björn Lisper lead the project that were active the years 2004-2005 it had a volume of 2,4 MSEK, which corresponds to 2% of the total project volume, 4 publications were produced of which one was a Licentiate thesis.

Goal: Methods to parallelize PLEX programs.

REMODEL

Christer Norström, Wang Yi lead the project that were active the years 2003-2005 it had a volume of 7,3 MSEK, which corresponds to 5% of the total project volume, 17 publications were produced of which one was a Licentiate thesis and 2 MSc theses.

Goal: To provide methods and tools for introducing timing analysis in existing industrial software systems.

SA (Static Analysis)

Sven-Olof Nyström lead the project that were active the years 1999-2001 it had a volume of 1,6 MSEK, which corresponds to 1% of the total project volume, 0 publications were produced.

Goal: Analysis of types and process topology for static debugging.

SAAPP (Simulator-Aided Analysis of Parallel Processes)

Björn Victor lead the project that were active the years 2002-2005 it had a volume of 4,3 MSEK, which corresponds to 3% of the total project volume, 3 publications were produced.

Goal: To monitor and analyse the execution of parallel programs at runtime, in a predictable and reproducible way, in order to find race conditions and other dependencies between processes.

SMC, FTA (Symbolic model Checking, Fault Tree Analysis)

Parosh Abdulla, Johann Deneux lead the project that were active the years 1999-2005 it had a volume of 11,4 MSEK, which corresponds to 8% of the total project volume, 12 publications were produced of which one was a Licentiate thesis and 4 MSc theses.

Goal: To develop tools to perform Fault Tree Analysis on time-dependent safety-critical systems.

Software Synthesis

Wang Yi lead the project that were active the years 2001-2003 it had a volume of 4,4 MSEK, which corresponds to 3% of the total project volume, 12 publications were produced of which one was a Licentiate thesis.

Goal: To develop (1) a tool for schedulability analysis of timed systems based on their design models and resource constraints. (2) a compiler to transform design models to executable code including a run-time scheduler (run time system) preserving the correctness and schedulability of the models.

Testning

Bengt Jonsson lead the project that were active the years 1999-2003 it had a volume of 6,9 MSEK, which corresponds to 5% of the total project volume, 25 publications were produced of which one was a Licentiate thesis and 6 MSc theses.

Three subprojects formed 2003 the testing cluster at ASTEC with the goals: Techniques for automated testing of computer systems. Central problems were: 1) - Symbolic techniques for generation of test suites from abstract models of system under test. 2) - Generation of test oracles from requirements of systems under test.

1. AutoWay (Automatic Testing of a WAP Gateway)
   Paul Pettersson lead the project that were active the years 2004-2005 it had a volume of 3,1 MSEK, which corresponds to 2% of the total project volume. Goal: A method for model based tesing of Real-Time systems using UPPAAL and TIMES.
2. DeTrack (Tracking Dependencies in Software Modules)
   Bengt Jonsson lead the project that were active the years 2004-2004 it had a volume of 1,7 MSEK, which corresponds to 1% of the total project volume. Goal: Developing a technique for detecting dependencies.
3. STEP (Specification Testing environment for Erlang Protocol software)
   Bengt Jonsson lead the project that were active the years 2003-2005 it had a volume of 3,7 MSEK, which corresponds to 3% of the total project volume. Goal: Developing a tool for test case generation.

VASSCO (Verification of Asynchronous Systems of Synchronous Components)

Roland Bol lead the project that were active the years 1997-1998 it had a volume of 0,9 MSEK, which corresponds to 1% of the total project volume, 0 publications were produced.

Goal: UU was supposed to assist Prover in the Esprit project CRISYS: Critical Instrumentation and Control Systems, and to dig deeper scientifically in areas covered shallowly by the project.

WCET, RT (Worst Case Execution Time Analysis, Rela Time)

Hans Hansson, Jakob Engblom, Björn Lisper lead the project that were active the years 1995-2005 it had a volume of 29,1 MSEK, which corresponds to 20% of the total project volume, 73 publications were produced of which 4 was PhD theses, 2 Licentiate theses and 10 MSc theses.

Goal: A WCET prototype tool, containing all parts (flow analysis, pipeline analysis, cache analysis, WCET calculation).

VOCAL (Verification and Optimization with Constraints And Logic)

Mats Carlsson lead the project that were active the years 1995-1997 it had a volume of 3,0 MSEK, which corresponds to 2% of the total project volume, 7 publications were produced of which one was a MSc thesis.

Goal: The project developed a package for constraint programming over finite domains for such applications, as well as for general use.

WPO (Whole Programme Optimization)

Sven-Olof Nyström lead the project that were active the years 1997-2004 it had a volume of 12,2 MSEK, which corresponds to 8% of the total project volume, 10 publications were produced of which two was MSc theses.

Goal: To explore optimization techniques that become feasible when the entire program is available to the compiler. We focused on optimizations that reduce memory use.