Appendix 4
05-Apr-2001 17:14

ASTEC Projects

Auto: A design methodology for embedded real-time systems
This project takes a broad view on the development of embedded real-time systems. The main focus is on

techniques for describing functional modules of a design and their relationships,
methods for mapping a network of connected functional modules onto a distributed target architecture. Important aspects are resource sharing, resource allocation and scheduling.

A starting point is the software development method BASEMENT proposed in the VIA project, which includes an outline of a signal-flow based design language.
Participating industries: Mecel AB.

SMC: Symbolic Model Checking Using Stålmarck's Method
The goal of the project is to extend the applicability and efficiency of model checking algorithms. The main approach is to consider an alternative approach for symbolic verification by using SAT-solvers such as Stålmarck's method, instead of BDDs as a search engine in model checking.
The main issues are

to design methods that scale for large and complex system models, in particular for control systems, signalling systems, hardware circuits, etc.
to make analysis as complete and powerful as possible in the case that complete coverage of the system model is impossible.

The work will be based on Stålmarck's method for proving large formulas in propositional logic and in restricted fragments of first-order logic.
Participating industries: Prover Technology AB.

BUS: Modelling and analysis of a bus protocol
This project is primarily a case study. It aims at modeling and analyzing a bus protocol, developed and implemented by ABB Automation Products, using state-of-the-art model checking tools, primarily UPPAAL. The purpose is

to construct an abstract model of the protocol, and finding sources of potential execution problems.
using the experiences gained in the case study, to develop further the general methodology for modeling bus protocols, and the tool support for analysis.

Participating industries: ABB Automation Products AB, UPAAL Sweden AB.

Automated Testing
This project aims at further development of techniques for automated testing of software systems. Issues to be addressed include:

Automated generation of test suites from requirements on software.
Selection and Assessment of test suites.
Investigation into the relationship between requirements and test suites.

The project will make a number of studies on how testing can be automated in collaboration with different industrial partners.
Participating industries: Telelogic AB, Telia Validation AB and Volvo Teknisk Utveckling AB.

ErlVer: A Verification Method for Erlang
This project develops a methodology which consists of the following.

On the theoretical side, of an operational semantics, property specification language based on temporal logic, and a proof system for Erlang.
On the practical side, of a tool set that supports verification of properties by means of a proof assistant, extended with a graphical user inteface, and with considerable support for proof automation.
Evaluation of the approach using a range of case studies in telecommunications systems, kindly submitted by Erlang software developers.

Participating industries: Ericsson Utvecklings AB.

SA: Analysis of types and process topology for static debugging
This project develops a method and an implementation for analysis of the Erlang programming language. The analysis is intended to give information similar to that of a static typing system, helping the programmer to validate and debug a program while it is being constructed. The approach is specifically aimed at handling features that are characteristic of Erlang and telecommunications programs, such as processes and communication. The analysis is also intended to provide information to an Erlang compiler, which can be used for compilation.
Participating industries: Ericsson Utvecklings AB.

HIPE: High Performance Erlang
The project aims at developing techniques for efficient compilation of concurrent functional programming languages. The project focuses on the Erlang language. Within the project, the following issues are addressed.

Techniques for efficient compilation of programming language features and abstractions that are prominent in communication software, such as process communication, process creation and code replacement. Efforts should be guided by the characteristics of realistic industrial applications.
Methods for measuring usage characteristics and execution properties of software, which is useful for guiding optimization efforts
Evaluation on industrial-size programs found in telecommunications systems, such as ATM switches and WWW servers.

The project is based on the current development of a compiler for Erlang, currently being developed at Uppsala University. This compiler is a platform for experimenting with optimizations, and for application to industrial-size programs, which exist today.
Participating industries: Ericsson Utvecklings AB.

WPO: Whole-Program Optimization in Compilers for Embedded Systems
This project addresses

Methods for automated and efficient compilation of code to meet stringent constraints on memory, power, timing, and irregular hardware architectures.
The target applications are taken from small embedded programs.
The approach to solve this problem is to develop static analysis methods that consider the entire program. The entire application is analyzed and optimizations are performed based on the information obtained. In the embedded market, the normal applications are small enough for this approach.

The goal should be "keyword-free programming", in which the compiler relieves the programmer from the burden to optimize for particular features of the platform. Techniques for automatically generating efficient optimized code for a variety of hardware platforms shall be developed.
Participating industries: IAR Systems AB.

WCET: Calculation of Worst-Case Execution Times
The project addresses static analysis of programming languages and hardware in industrial use, in order to extract information about the execution time of code fragments. This information is of vital importance for the development of predictable embedded and real-time systems.
This project addresses three main areas:
- Static and automatic analysis of program flow, in order to determine the worst possible program executions without manual intervention. Examples of problems that are attacked is recursion, loops, and inheritance in object-oriented languages.
- Analysis of hardware features like pipelines, caches, and external memory, to provide timing estimates on the level of single clock cycles.
- The combination of flow information and hardware information to calculate final execution time estimates, including how to account for compiler optimizations that makes the relation between source code and object code complex.
Participating industries: IAR Systems AB and Volcano Communications Technologies AB.
Updated 05-Apr-2001 17:14 by Roland Grönroos
e-mail: info -at- astec.uu.se Location: http://www.astec.uu.se/etapp3/evaluations/eval2000/material/appendices/projects.shtml
- Uppsala University