ASTEC

ASTEC Final Report 1995-2005

Uppsala_University
line

This document including cover and appendices as pdf file.

Contents

Tables and figures

Summary

ASTEC (Advanced Software Technology) was a competence centre, which focused on advanced tools and techniques for software development. Development of software accounts for a significant part of the costs in the construction of a number of important products, such as communication systems, transportation and process control systems, of Swedish industry. ASTEC's vision were that software should be developed using high-level specification and programming languages, supported by powerful automated tools that assist in specification, analysis, validation, simulation, and compilation. ASTEC has conducted pre-competitive and industrially applicable research that contributed to fulfil this vision, built up a concentrated research environment, and been a forum for contacts and exchange of ideas between academia and industry. Four primary examples of ASTEC results are:

  1. The High Performance Erlang compiler system: this tools is now widely used in the telecommunication industry, and its importance will grow in the future.
  2. The UPPAAL and TIMES Toolsets for modeling, analysis, and implementation of embedded systems have spawned a startup company, and are world-leading in their domains
  3. The Worst Case Execution Time Analysis tools chain, which takes a C program as input and automatically generates a WCET estimate for the program, has been evaluated on a range of examples from the embedded software industry
  4. Tools and results on symbolic model checking, including the tool FixIT, which was the first application of SAT-solving technology to complete automated verification, and a tool to automatically perform fault tree analysis incorporated into Prover Technology's plug-in in Scade.

The scientific results of ASTEC have been widely recognised, with several award winning papers and tools. The amount of publications has been large: 266 publications whereof 51 theses (PhD, Lic and MSc). The network effects have been great with 170 persons directly involved in writing. A number of undergraduate courses have been directly involved in projects, stretching over up to 6 months. Furthermore, expertise emanating from the research teams and activities has been incorporated in the gradual update of the course programmes given at the universities involved. A close co-operation between Uppsala University and Mälardalen University and the industry has been developed through staff mobility during ASTEC's lifetime.

Sammanfattning

ASTEC (Advanced Software Technology) var ett kompetenscentrum för utveckling av avancerade tekniker och verktyg för programvaruutveckling. Utveckling av programvara utgör en betydande del av konstruktionskostnaden för viktiga produkter som kommunikationssystem, transport och processtyrningssystem i svensk industri. ASTEC's vision var att programmvara ska utvecklas med hjälp av högnivåprogramspråk som stöds av kraftfulla automatiska verktyg för specificering, analys, simulering och kompilering. För att uppnå visionen utförde ASTEC prekompetitiv forskning av hög industriell relevans. ASTEC byggde upp en forskningsmiljö som blev ett forum där kontakter och idéer flödade mellan universitet och industri. Fyra exempel på konkreta resultat av samarbete är:

  1. "High Performance Erlang" kompilator systemet. Detta verktyg används nu allmänt (även internationellt) inom telekomindustrin. Vi ser att dess betydelse kommer att öka med tiden.
  2. UPPAAL och TIMES verktygen för modellering, analys, och konstruktion av inbyggda system är världsledande inom sitt område. De har även gett upphov till ett nystartat företag.
  3. "Worst Case Execution Time Analysis tool chain" (analys av maximal körtid för ett program) kan för ett program skrivet i C automatiskt ge den längsta tid detta program kan tänkas ta på sig att utföra sin uppgift. Detta verktyg har utvärderats på en mängd inbyggda program från industrin.
  4. Två verktyg för "symbolic model checking". FixIT var den första första analysprogrammet som använde SAT-lösare för automatisk verifiering. Ett automatiskt verktyg för felanalys har byggts in i Prover Technology's plug-in i Scade.

ASTEC's vetenskapliga produktion (266 publicationer varav 51 avhandlingar (doktor, licenciat and examensarbeten)) har fått ett brett internationellt erkännande, bland annat vann flera uppsatser och verktyg priser. Nätverket som byggdes upp omfattade bland annat 170 personer som författare till publikationerna. Några universitetskurser blev direkt inblandade i vetenskapliga projekt som kunde vara upp till 6 månader. Innehållet i flera kurser upppdaterades med forskningsresultat från ASTEC som utgångspunkt. Ett nära samarbete utvecklades mellan Uppsala universitet och Mälardalens högskola genom att personal flyttade mellan arbetsplatserna.

Facts about partners, finances and organisation

Table Years in astec vs partners
Table A. The industrial participation in ASTEC during 1995-2005. Company names within the same row represent essentially the same partner whose name or internal organisation has changed during the years.


Partners

The expansion of ASTEC together with industrial changes in infrastructure and has led to a total of 34 involved partners in ASTEC (Table A). Three industrial partners have been involved in ASTEC from the start in 1995 until the end in 2005, Ericsson, IAR and Validation. From the personal point of view we have had contact with the same persons in many companies throughout the changes in industry. Three academic partners has helped Uppsala university to carry out the research, KTH (1995-1998), SICS (1996-2001) and Mälardalen university (2001-2005). At the initial years were NUTEK (Närings- och teknikutvecklingsverket) the organising partner, after a reorganisation in 2001 were research and development tasks moved to the new Verket för innovationssystem, (VINNOVA).

Finances

The contributions to ASTEC from all partners each phase (Table B). The total contributions after 10 years were 156 MSEK.

Organisation

The consortium

ASTEC was formed as a consortium of academic and industrial partners. Research groups at Uppsala University, the Swedish Institute of Computer Science (SICS), Mälardalen University and the first years also KTH, studied mainly formal methods, functional, logic and constraint programming languages, compilation, and on embedded, distributed, and real-time systems, together with companies with a substantial software production and thus a large interest in software development, and companies that produce tools for software development. Further details about accounting and economy are given in Appendix 2. A notable figure is that the number of companies grew with about one company per year.



ASTEC Partners vs contributions each phase Table B. Each partners contribution to ASTEC divided into the four phases. Note that year 3 became a separate phase. The phases had different length Phase 1, 2 years; Year 3, 1 year; Phase 2, 2 years; Phase 3, 3 years and Phase 4, 2 years. Company names within the same row represent essentially the same partner whose name or internal organisation has changed during the years.

Management

The management of ASTEC were structured as follows: Within Uppsala University, ASTEC is a separate financial unit, hosted by the Department of Information Technology. The participating institutions and companies employed all personnel involved in ASTEC.

ASTEC Activities were controlled by a board (Table C). Daily management was performed by the director, Bengt Jonsson (1995-2004) Konstantinos Sagonas (2004-2005), the assisting director, Konstantinos Sagonas (2002-2004), the administrative research coordinator Roland Grönroos (1998-2005), and the respective project leaders (Appendix 3). The directors and project leaders had regular monthly meetings.

Area coordinators for each technical area were responsible for strategic project planning and for planning seminars together with the coordinator. Longer-term project planning and progress was supervised by the Scientific Advisory board (Table D), which also carried out internal reviews. All funding decisions are taken by the board. The board followed activities through project reports, and contributed to ensure the industrial relevance of ASTEC work.

The scientific work in ASTEC was carried out in cooperation between the participating research groups, both in industry and academia. There were (and still are) many informal links, discussions, and technical links between projects within ASTEC. Formal components in this cooperation were the ASTEC seminar series, which typically meets twice a month, and regularly organized program area seminars. Two-day workshops for the entire ASTEC were conducted annually.



Table C. Board members during 1995-2005
Name Affiliation Period
Ewert Bengtsson Uppsala University 990101 – 991231
Bjarne Däcker Pensioner (former Ericsson AB) 990101 – 051231
Martin Eriksson Validation AB 000101 – 031231
Peter Eriksson ABB Automation Technologies AB 040101 – 051231
Erik Hagersten Uppsala University 000101 – 051231
Catrin Hansson-Granbom Ericsson Utvecklings AB 020101 – 031231
Seif Haridi SICS/KTH 990101 – 991231
Sten Hellström Mecel AB 990101 – 001208
Olle Landström IAR AB 990101 – 051231
Jan Lindblad ENEA OSE Systems AB 020101 – 051231
Björn Lisper Mälardalen University 000101 – 051231
Lena Nyberg WM data AB 040101 – 051231
Åke Sandberg Telia Validation AB 990101 – 991231
Mike Williams Ericsson AB 040101 – 051231


Table D. Scientific advisory board
Name Affiliation Period
Prof. Alan Burns University of York 1998
Prof. Neil Jones University of Copenhagen 1998 – 2005
Prof. Bernhard Steffen University of Dortmund 1998 – 2005
Prof. Neeraj Suri TU Darmstadt 1998 – 2005



The Centre Development over 10 years

History and Evaluations of ASTEC

During the first two years (Phase 1), ASTEC activities focussed on establishing collaboration links between academia and industry by conducting projects where techniques from academia were applied to problems in industry, thereby creating a network of contacts.

To address recommendations of the first ASTEC evaluation, in Phase 2, a strategic research plan, which structures challenges for the long-term development of ASTEC, was developed. Based on this plan, more research competence has been recruited and strengthened to build up key areas of ASTEC such as compilation, and the administrative support was strengthened by appointing a research coordinator (Roland Grönroos, 40%). Also in Phase 2, an international scientific advisory board was appointed Table D.. The scientific advisory board conducted several self-imposed internal reviews in Phase 2, 3 and 4. These reviews have pointed out strengths and weaknesses in the technical work of ASTEC, provided guidance, and resulted in shifts of focus of some projects.

The second, mid-term NUTEK evaluation in year 2000 generally expressed its satisfaction with the work of ASTEC and with the measures taken since the first review. Specific recommendations for individual projects and for the structure of ASTEC in general were made and most of them have been followed. In particular, we mention:

  • The recommendation that the ASTEC board be enriched with influential leaders from industry partners. Catrin Hansson-Granbom (from Ericsson AB) and Jan Lindblad (from OSE Systems AB) joined the ASTEC board, and an assisting director was appointed.
  • That procedures and mechanisms be developed that ensure that all researchers and participants are well informed about projects, technology transfer plans, and the interrelationships between projects. In response to this recommendation, ASTEC created the CODER project cluster, organized half-day long seminars where work from the three technical areas of ASTEC was presented in a concentrated form, and has kept the frequency of meetings between project leaders high.

The Research Programme of ASTEC

The research program of ASTEC has steadily focussed on advanced tools and techniques for software development. Development of software accounts for a significant part of the costs in the construction of a number of important products, such as communication systems, transportation and process control systems, of Swedish industry. It is thus a vital interest to be able to produce better software at lower cost. One of the means to achieve this is to improve the tools and techniques used for software development. ASTECs vision has been that, wherever possible, software should be developed using high-level specification and programming languages, supported by powerful automated tools that assist in specification, analysis, validation, simulation, and compilation. The purpose of ASTEC has been to conduct pre-competitive and industrially applicable research that contributes to this vision, to build up and offer a concentrated research environment in the software technology area, and to be a forum for contacts and exchange of ideas between academia and industry.

Initially, in 1995, the ASTEC research program defined as the union of 4 program areas: Requirements engineering, programming paradigms, implementation techniques, and analysis techniques. The focus of ASTEC was to establish collaboration links academia with industry by conducting projects where techniques from academia were applied to problems in industry. 4 projects were initiated in 1995, each focusing on a specific application domain.

The first international evaluation criticized ASTEC on several points, one of which was that ASTEC did not systematically identify and pursue relevant longer-term research problems. As a reaction to this criticism, in phase two, a strategic perspective for the long-term development of ASTEC was added. A Strategic Research Plan was developed, which structures longer-term challenges addressed by ASTEC.

In the A Strategic Research Plan, the research activities of ASTEC are structured into program areas, which focus the efforts from several projects and are responsible for a wider dissemination of the conclusions, conducting seminars or specialised courses as deemed necessary. The areas are interrelated in that progress in one area is dependent on the state of the art in the others.

Each program area is either an application area, which provides problems to drive the research, or a technical program area, which serve to develop techniques, tools, and methods. A particular project can very well span over several of these areas, typically at least one technical area and one application area.

The application areas are

  • Software for Automotive and Vehicle Applications, including embedded and safety-critical software, often deployed on a distributed network, and
  • Data- and telecommunication systems, with requirements on mobility, high distribution, massive concurrency, and code replacement without disruption of the continuous operation of the system.
The technical areas are
  • Validation and verification is concerned with high-level notations for expressing requirements and design specifications, together with tools and (formal) methods for analysis of specifications for the purposes of verification, validation, test generation, and tracing of requirements.
  • Programming language implementation and compilation is concerned with the implementation and use of high-level (concurrent) programming languages, together with the development of compilation technology for (time- or space-) efficient program execution and code generation for different architectures.
  • Real-time, embedded, and distributed systems is concerned with features specific to software development for real-time, embedded, or distributed systems, such as predictability, timeliness, scheduling, and distribution.

The strategic research plan formulates longer-term research goals which require basic research and address important industrial problems. Based on the plan, research competence has been recruited and strengthened to build up key areas, and long-term Ph.D. thesis projects have been formulated. As example, the area of compilation was included within ASTEC, where competence was recruited and strengthened.

Also in phase two, an international Scientific Advisory Board was appointed, consisting of profs. Alan Burns (York), Neil Jones (Copenhagen), and Bernhard Steffen (Dortmund), later also prof. Neeraj Suri (Gothenburgh). The Scientific Advisory Board conducted annual internal reviews. The reviews of the Scientific Advisors have pointed out strengths and weaknesses in the technical work, and resulted in some shifts of projects. As an example, the work on requirements, started in Phase 1, was phased out in Phase 2, and later replaced by work on testing.

After the restructuring in Phase 2, ASTEC developed into a focussed research unit with a critical mass within its key areas. ASTEC has since then performed research on the highest international level. Impressive recognized research results have been produced, of both theoretical and practical nature, and are published in leading conferences. ASTEC collaborates with other national research initiatives, and has strong international collaboration links. A sign of recognition is that centre groups participate in an increasing number of European collaboration projects.

The number of industrial partners of ASTEC has been steadily increasing. Results from ASTEC work have been transferred and are used in industry. Some of the technology development in ASTEC has been transferred into industrial products, which are currently supported by ASTEC groups. The academic-industrial collaboration has given ASTEC research very valuable access to industrial software for experimentation, evaluation, and code development, as well as a rich source of interesting research problems.

The production of Ph.D., Lic., and M.Sc. graduates has continued. The centre contributes courses to national and local graduate and undergraduate education. Several tools produced in ASTEC work are used in graduate and undergraduate education, both locally, nationally, and internationally. ASTEC has been a catalytic force in the creation of new academic positions, including chairs, within its area.

Two notable characteristics of software development within many of the ASTEC projects facilitate industrial implementation and technology transfer:

  1. The existence of software, concurrently with a commercial version, in an open-source version which is not significantly different than the commercial one. Such is for example nowadays the case for the Erlang/OTP system from Ericsson. Existence of an open-source version, not only allows distribution of code without getting hang up into legal issues, but also provides a whole new community of users which is significant in number. Perhaps not surprisingly (since they have access to the code), some of the open-source users are quite knowledgeable and are often more committed to improving the software than its paying users. Moreover, they are not afraid to try new, unsupported features and seem to have more time to provide valuable feedback than commercial users. All these, have e.g. allowed the HiPE compiler to be first released as an unsupported component of Erlang/OTP, get feedback and an ``informal approval'' from the open-source user community, thereby making the decision to also include HiPE in the commercial version of Erlang/OTP (which is the one typically used in telecom applications) easier to take.
  2. Because of the close industrial collaboration, it is quite often the case that state-of-the-art academic research projects carried out under the aegis of ASTEC have access to production-size, industrial-quality software. This software is given as source code, which can be used to conduct experiments and serve as a ``real-life'' benchmark. This has given the research on compilation, execution-time analysis, and on formal verification, a unique opportunity to evaluate the applicability and effectiveness of new techniques in realistic settings rather than on synthetic (and often toy) benchmarks.

Organization and Collaboration

Initially, in 1995, the research groups of ASTEC were located at Uppsala University (UU), the Royal Institute of Technology (KTH), the Swedish Institute of Computer Science (SICS), with Uppsala University as the main site for the center. After 2000, the involvement of KTH and SICS gradually declined, and was replaced by activities at Mälardalen University in Västerås.

ASTEC was formed as a consortium of academic partners with strong research programs in different areas of software technologies, and of companies which either have a substantial software production or produce tools for software development. During phase 1, i.e., the first two years, the focus of ASTEC was to establish collaboration links academia with industry by conducting projects where techniques from academia were applied to problems in industry. This phase created a network of contacts between academia and industry.

The First NUTEK Evaluation was not fully satisfied with ASTECs functioning. Its recommendations were addressed by several measures, including the following.

  • Working out a strategic research plan pointing out strategic research areas, and plans for promoting them. During several years around 2000, ASTEC promoted national workshops in each strategic research area, as well as industrial seminars.
  • ASTEC standardized a model for industrial Ph.D. students, in which a student was half-time employed by a university and a company, while still devoting most of his/her time to research in ASTEC.
  • The administrative support was reinforced by appointing Roland Grönroos as half-time research coordinator shared with ARTES.

The organization of ASTEC Management stabilized to the following points

  • Within Uppsala University, ASTEC is a separate financial unit, hosted by the Department of Information Technology. The participating institutions and companies employed all personnel involved in ASTEC.
  • ASTEC Activities are controlled by a board of 7 member, chaired by Bjarne Däcker.
  • The director, the assisting director, the administrative research coordinator, and the respective project coordinators performed daily management. The directors and project coordinators had regular monthly meetings.
  • Area coordinators for each technical area were responsible for strategic project planning and for planning seminars. The Scientific Advisory board, consisting of Neil Jones, Bernhard Steffen, and Neeraj Suri, which conducted yearly internal reviews, supervised longer-term project planning and progress.
  • The board took all funding decisions. The board followed activities through project reports every 6 months, and contributed to ensuring the industrial relevance of ASTEC work.

The scientific work in ASTEC was carried out in cooperation between the participating research groups, both in industry and academia. There were many informal links, discussions, and technical links between projects within ASTEC. Formal components in this cooperation were the ASTEC seminar series, which typically meet twice a month, and regularly organized program area seminars. Two-day workshops for the entire ASTEC were conducted annually, in conjunction with reviews by the Scientific Advisory Board.

An important improvement in the organizational foundation for ASTEC has been the formation of strong University Departments at its research nodes.

In January 1999 the various small departments at Uppsala University dealing with different aspects of IT were joined to two large departments, and the Virtual IT-faculty was created to coordinate and promote the role of IT within the university in different ways. These reforms created the very strong Department of Information Technology. Generally speaking, ASTEC was been part of this increased focus on the IT area within the university both in the sense that the program had advantages from it and that the activities within ASTEC have been seen as part of the focus on IT at Uppsala University.

Mälardalen University has over the last several years developed MRTC (the Mälardalen Real-Time REsearch Centre) into a strong environment for Real-Time research, now with around 100 researchers.

Many ASTEC projects have involved only one industrial partners, especially in the earlier phases of ASTEC. ASTEC has strived to make projects involve several industrial partners, thereby also promoting contacts between them. After year 2000, this has resulted in the formation of several project clusters, such as

  • The Erlang Cluster containing projects involving Erlang, including HiPE (at UU) and Erlang/OTP (at Ericsson) development teams, the Failure analysis project, and the testing project at Mobile Arts AB.
  • Another example of close coordination between different activities in ASTEC is the formation of the CODER (Cluster on Distributed and Embedded Real-Time systems) cluster, which originated from integration of the WCET group with the WPO group, and which also includes the projects TAS and Remodeling. The rationale for forming the CODER cluster is that there are obvious synergies between research on compilation techniques for embedded systems and research on execution-time analysis of code for such systems. In practice, this has worked out very well. There is a research compiler infrastructure shared by the two groups, and there have been several joint graduate seminars on program analysis techniques.
  • The work in the CODER cluster is geographically and organizationally dispersed, with nodes at Uppsala University, IAR Systems, CC-Systems, ABB, OSE Systems AB, and Mälardalen University. There is also a steady cooperation with C-Lab in Paderborn, Germany. This has worked well, thanks to using email, instant messaging programs, and the use of CVS (Concurrent Versions System) to share text and code.
  • The Testing project clusters has involved work at Validation AB, Ericsson AB, and Mobile Arts AB, and previously Volvo Technical Development Corp.

Technical and scientific results

Appendix 1, ASTEC Publications 1995-2007 list the 266 publications produced. Appendix 3 shows ASTEC Projects, their acronyms, names, leaders, goals, time period, volume and publication rate.

Application Areas

A.2.1. Software for Data- and Telecommunication Systems

ASTEC has been guided by the ficion that development of communications software should be conducted, not by large organisations employing heavy and often old-fashioned software development processes, but by small, well-qualified teams working with powerful development tools that enable them to quickly turn an innovative idea into a products. This means that the tools should preferably embody solutions to typical requirements for these systems, including reliability, massive concurrency, ability to update systems with new functionality while in operation, etc. Therefore, ASTEC has been actively involved in the development of the Erlang programming language, and several projects have centered around applications written in Erlang. Erlang is a concurrent functional programming language designed by Ericsson to ease the development of large-scale, distributed, soft real-time applications. Erlang has thus far been used quite successfully in the telecommunication industry, both within Ericsson Telecom, where it was designed and developed, and by other companies (both within Sweden and internationally). Examples of product whose software is written in Erlang are scalable ATM switching systems, ADSL delivery systems, next-generation call centers, scalable internet servers, mail robustifiers etc. ASTEC's involvement in the context of Erlang has spanned various aspects of Erlang's design, implementation, and use:

  • at the level of programming language design, two significant extensions of the Erlang language (a package system and a parameterized module system) have been designed and implemented in the context of the HiPE (High Performance Erlang) project;
  • at the level of the efficient implementation of the language, the HiPE native code compiler and a shared heap runtime system architecture have been developed and fully incorporated within the Erlang/OTP (Open Telecom Platform) system;
  • at the level of enhancing the robustness and safety of applications, tools that aid the verification and testing of applications written in Erlang have been developed in the context of the ASTEC projects ErlVer (Erlang Verification), Failure Analysis, and Testing.

We describe these software tools below.

The major goal of the HiPE project has been to improve the performance characteristics of Erlang applications through better implementations of the language. The project started by developing a native code compiler for Erlang. A native code compiler with a SPARC back-end was developed and open-source released as an autonomous system, called the HiPE system in March 2000. Aiming to achieve more impact on the Erlang community, the HiPE project thereafter incorporated and integrated the HiPE native code compiler in the Erlang/OTP system from Ericsson (which is the most commonly used implementation Erlang, and certainly the only system used in commercial applications). The HiPE compiler then became a fully integrated and supported component in Erlang/OTP started from release R9B in 2002.

In addition to compiler development, a sub-project within the HiPE project developed an alternative runtime system architecture for the Erlang/OTP system. Its main characteristic is the use of a shared heap space for all Erlang processes, which enables inter-process communication to occur with significantly less costs. This work is nowadays also fully integrated within the Erlang/OTP system (starting with R9B). More information can be found at Erlang/OTP's homepage.

The HiPE compiler improves the performance of Erlang applications from a few percent up to an order of magnitude. Furthermore, significant space improvements (e.g. an order of magnitude reduction) from uses of the shared heap runtime system architecture can often be observed in large, highly concurrent Erlang applications (e.g. in the NETSim product from Ericsson). Feedback from users of features of Erlang/OTP developed in the context of the HiPE project is quite positive. As a concrete example, in 2003, another company, T-Mobile, joined ASTEC as a new industrial partner and became the second industrial partner of the HiPE project (the first being Ericsson).

Software for telecommunication systems often possesses certain characteristics, such as massive and dynamic concurrency and on-line updating of software, that prohibit the use of fully automatic verification techniques. To permit verification of such software programmed in Erlang a major effort has been undertaken in the ErlVer project. A significant part of the work is described in the Ph.D. Thesis of Lars-åke Fredlund (Sept. 2001). An operational semantics for Erlang has been developed, with a property specification language and a novel proof system for compositional and inductive reasoning. To support verification, a proof assistant with a state-of-the-art graphical user interface and considerable support for proof automation is available: the Erlang Verification Tool (EVT). The feasibility of the method has been illustrated in case studies such as, e.g., the verification of a core part of the Mnesia distributed database system which is part of the standard Erlang distribution. As a side effect of the Erlang verification effort, two patent applications at Ericsson's Computer Science Laboratory were indirectly stimulated.

The EVT tool is rather ambitious, in that it allows to verify arbitrary properties of the behavior of an Erlang program, which could be expressed in a general property language. As a consequence, it is difficult to obtain automatic proofs for properties of programs of significant size. Motivated by this, two smaller projects were carried out have aiming at the automated validation and testing of certain characteristics of typical applications written Erlang.

  1. More specifically, the Failure analysis project has developed a tool which focuses on analyzing only the failure behavior of a telecom application, but which in return is able to do so fully automatically on applications of significant size. The techniques developed in the context of this project analyze what is the effect of a process failure on the overall system and how the system can recover from such a failure. These techniques crucially assume (and also check) that the programmer has used the built-in support for failure recovery that is provided by the Erlang/OTP platform. The tool has been evaluated on several parts of the software in the AXD 301 switch.
  2. Another automated tool for analyzing the behaviour of telecom applications written in Erlang has being developed in the Testing project in collaboration with the company Mobile Arts AB. The tool allows the automatic generation of test sequences for telecom protocols. The generation considers both control and data aspects of the protocol; data parameters are handled symbolically. The tool assumes that the protocol to be tested is specified as a state machine, and generates a test suite. The tool has been applied to a product developed by MobileArts, for which it is possible to achieve a very high degree of coverage.

A.2.2. Software for Embedded Applications

A lot of effort is currently devoted to developing and formalizing a complete methodology for building software in embedded systems, for instance within the automotive industry. Such a methodology should cover the entire chain from requirements to running code on a specific target platform. Systems are often assembled from parts delivered by subcontractors, and requirements on resource consumption are often very stringent. Challenging research problems include development of notations for requirements, techniques for system modeling and for analyzing whether a component or a collection of components conforms to requirements, techniques for mapping a design onto a distributed target architecture, and for generating code which satisfies requirements on memory, power and timing consumption.

ASTEC has addressed the development of tools that address larger chunks in the development chain by combining solutions to several related problems. Two major efforts in this area are the TIMES tool, which combines modeling, schedulability analysis, schedule synthesis, and code synthesis, and the development of an integrated tool for calculating the WCET (Worst-Case Execution Time) of embedded programs.

TIMES is a tool for Modeling and Implementation of Embedded Systems, which supports modelling, simulation, verification, schedulability analysis, synthesis of (optimal) schedules and executable code. It is appropriate for systems that can be described as a set of tasks which are triggered periodically or sporadically by time or external events. Currently TIMES supports code generation for the LegoOS platform. A system model consists of three parts: a control part represented as a network of timed automata extended with tasks, parameters of the triggered tasks, and a scheduling policy. The unique feature of TIMES is that it supports a more general process model (timed automata) than usual in classic scheduling theory, where processes are usually assumed to be periodic. The schedulability analysis then avoids overly pessimistic results, made possible by exploiting recent advances in verification of timed systems, as embodied in UPPAAL. in Section A.2.3. The TIMES tool received the Best tool award at the ETAPS conferences in April 2002.

The WCET project has produced an end-to-end prototype tool that takes a C program as input and automatically generates a WCET estimate for the program. The aim is to make the WCET calculation (almost) fully automatic, thus relieving the programmer from the burden of current practice to annotate the program with flow information, and to measure (by testing or simulation) the execution time of individual code segments.

The prototype tool integrates solutions to all parts of the WCET problem puzzle: it compiles the program and generates a representation of its structure, it makes a semantic analysis of the program code and generates flow information that states how many times each part may be executed, it analyzes the effects of low-level processor features, such as caches and pipelines, and finally it combines all the information to calculate the actual WCET of the program. The tool is built on the modular tool architecture developed within the WCET project for combining modules that solve each particular subproblem into an end-to-end tool.

The quality of the results generated by the WCET tool are very competitive. For the classes of processor addressed by the pipeline analysis, very tight results have been demonstrated. The flow analysis gives good flow information for simple programs, and is continually being extended to handle greater parts of the C language. Thanks to working within a compiler, very powerful analyses are possible which are much harder for an approach that starts from the object code.

The ASTEC WCET group has been active throughout the entire lifetime of ASTEC (1995 - 2005). The group was initially situated at Uppsala University, then activities started at Mälardalen University under the leadership of Prof. Björn Lisper, and towards the end of ASTEC the group was fully migrated to Mälardalen University.

The first activities of the group were initial studies like the industry enquiry 1997. Later, Jan Gustafsson and Andreas Ermedahl published seminal papers on automatic flow analysis for WCET analysis 1997 and 1998. Another research direction was pursued by Jakob Engblom and Andreas Ermedahl, who developed advanced low-level analysis and calculation methods.

From the end of the 90ies, the group has developed to become one of the world's leading groups in static WCET analysis. The group has very good relations with the WCET international research community, and is active in European research networks such as ARTIST2 and the forthcoming ARTIST-DESIGN.

Leading members of the group delivered PhD theses in the WCET area during the forthcoming years (Gustafsson 2000, Engblom 2002, Ermedahl 2003).

During the final years of ASTEC, the group published results at most of the real-time workshops, conferences and symposiums world-wide, as well as in leading journals on real-time and computer systems. The group also developed a well-known WCET analysis prototype tool, SWEET (SWEdish Execution Time analysis tool).

The work has been performed with good contacts with the industry, like Volvo and Enea. For example, a series of industrial case studies have been performed from 1998 and onwards. These results of these case studies have been published at several scientific conferences.

In cooperation with CC Systems, the TAS (Time-Accurate Simulation) project has (in a series of M.Sc. theses) developed techniques to simulate distributed real-time systems in real time, in order to allow efficient testing and debugging on a regular PC. They have been proven by use in industrial pilot studies together with customers of CC-Systems, and are being used today at CC-Systems to develop new embedded control systems. TAS is a good example of how the university world can help small companies adopt and develop simple but powerful ideas into techniques that confer concrete competitive advantages.

Timing properties are also central for the Remodeling project, conducted in cooperation with ABB Robotics, but this project has a different goal, namely to develop techniques to recover the structure of old, complex, real-time software, in order to allow easier maintenance and addition of new functionality, also by third parties. The project uses measurements to generate a model of an existing system that covers resource usage of programs, such as timing properties, memory consumption, and performance properties.

There is an increasing industrial interests in using UML as a standard modeling language, for the development of embedded systems. Most software tools for UML support only editing, modeling and simulation, and no analysis. Gunnar Övergaards Ph.D. thesis (2000) lays a foundation for such tools by providing a formal semantics for a significant portion of UML.

Technical Areas

A.2.3. Validation and Verification Technology

The area considers methods and tools for specifying and analysing properties of the behavior of systems and system components. The emphasis is on formal approaches to requirement and design specification, and on methods and tools for establishing adherence of systems to their specifications.

During the life span of ASTEC, several industrial case studies were carried out, in which industrial protocols and distributed software systems were verified using existing verification tools, such as UPPAAL, aiming at evaluating the industrial applicability and usefulness of the existing techniques and tools, some of which are developed in the Validation and Verification area. The UPPAAL tool implements techniques for modeling systems and their components on a high level of abstraction, and for analyzing whether a collection of components actually cooperate to meet system requirements. It has been successfully applied to the analysis of timing-dependent bus protocols. The Ph.D. thesis of Paul Pettersson (1999) contains a sequence of case studies which analyze the behaviour of systems of components, using the UPPAAL tool. Several case studies are taken from automotive applications. A conference paper presenting a case study on a gearbox controller, conducted in collaboration with Mecel AB, was invited for publication to the Springer Verlag journal STTT (Software Tools for Technology Transfer). Mecel AB and Uppsala also collaborated on the analysis of a car locking system at SAAB.

A result of the work on case studies within ASTEC, is the development of BUTLER by Mecel AB. BUTLER is a tool set for structuring requirements and design models for automotive systems.

Verification is carried out on a model of the system, the creation of which is a significant effort. It is not reasonable to expect that industrial software development develops both a software system and a model of it as separate activities. Moreover, it is a challenge to develop executable code from such models with predictable timing behaviours. Main research issues include schedulability analysis and schedule synthesis. The Software Synthesis project was created in 2000 to develop the TIMES tool, which is designed for schedulability analysis and generation of executable code with predictable timing behaviour from design models that can be analyzed by UPPAAL. The TIMES tool is based on UPPAAL, but also incorporates recent results on schedulabiliy analysis.

In classic scheduling theory, real time tasks (processes) are usually assumed to be periodic, i.e. tasks arrive (and will be computed) with fixed rates periodically. Analysis based on such a model of computation often yields pessimistic results. To relax the stringent constraints on task arrival times, we have proposed to use automata with timing constraints to model task arrival patterns. This yields a generic task model for real time systems. The model is expressive enough to describe concurrency and synchronization, and real time tasks which may be periodic, sporadic, preemptive or non-preemptive, as well as precedence and resource constraints. We believe that the model may serve as a bridge between scheduling theory and automata-theoretic approaches to system modeling and analysis. The standard notion of schedulability is naturally generalized to automata. An automaton is schedulable if there exists a scheduling strategy such that all possible sequences of events accepted by the automaton are schedulable in the sense that all associated tasks can be computed within their deadlines. It has been shown that the optimal schedulability checking problem for such models is decidable and for fixed priority scheduling strategy, the problem can be efficiently solved by reachability analysis on timed automata using only 2 extra clock variables. The analysis can be done in a similar manner to response time analysis in classic Rate-Monotonic Scheduling.

The TIMES tool can be downloaded at www.timestool.com. (It is freely available for research and educational purposes.) It provides a graphical interface for editing and simulation, an engine for schedulability analysis, and a compiler. Given a system design model consisting of

  • a set of application tasks whose executions may be required to meet mixed timing, precedence, and resource constraints,
  • a network of timed automata describing the task arrival patterns, and
  • a preemptive or non-preemptive scheduling policy,

TIMES will generate a scheduler, and calculate the worst case response times for the tasks. The design model may be further validated using a model checker (e.g. UPPAAL) and then compiled to executable C-code using the compiler.

The Testing project, which started in the previous period, has in the last years focused on model-based test generation, i.e., automated generation of test suites from a formal design model. The work extends existing techniques for finite-state models in two directions.

  • Automated generation of real-time tests, (which check also quantitative delays) from timed automata specifications, is developed in collaboration with Aalborg University. The generation is guided by supplying test purposes and/or a coverage criterion. Several different coverage criteria are supported. A distinctive feature of our techniques is that for a given test purpose and coverage criterion, a time-optimal (i.e., taking shortest time) test suite can be generated by using an existing extension of UPPAAL to generate optimal test executions.
  • Automated generation of tests that consider data parameters using symbolic techniques is developed in collaboration with MobileArts AB. Tests are generated from finite state machines extended with boolean data variables. The implementation work has been able to capitalize on other tools developed in the Erlang work of ASTEC.

In the previous period, techniques for translating formal specifications into so-called test oracles, i.e., programs that observe the specified system during testing and report when requirements are violated, were developed in a case study in collaboration with Volvo Technical Development AB. This work has been continued by connecting this generation to the Simulink environment, thus making the oracle generation facility usable by embedded systems engineers.

During 2002 – 2003, the SMC project in collaboration with Prover Technology AB has, based on the Prover Plug-in implementation of Stålmarck's algorithm, which in 2000 generated the tool FixIt, focussed on extending the design tool Esterel Scade with the Prover Plug-In to automatically perform fault tree analysis, a wide-spread method for finding minimal combinations of failures of components leading to a failure of the whole system. This allows designers to verify, for example, that it takes at least three components to fail simultaneously to cause the system to become unsafe. The automatic verification is done by repeatedly calling the Prover model-checker. Our implementation extends the Prover Plug-In model checker, The tool proved capable of analysing relatively large examples provided by ONERA CERT, Saab AB, and Airbus.

Final words

During its lifetime, ASTEC has witnessed the buildup of strong and internationally leading research units, primarily at Uppsala University and Mälardalen University. At its beginning in 1995, the involved research groups were rather small in size, but during the lifetime of ASTEC, several chairs were created, and the research infrastructure was expanded. ASTEC has been a major driving force for this development and also benefited from it. Several of ASTEC's results, in particular the software systems that were developed over many years, count among the best examples of combining industrial applications with first-class scientific research. ASTEC produced many successes, but its mission is by no means fulfilled. The importance of the just mentioned software systems will only grow in the future, judging by the available signs. It takes a long timed to change development processes in industry. Although much has been done, due to the development of system complexity ASTEC's initial vision "to increase the quality, safety and maintainability of software products" remains at least as valid now as it was 10 years ago. We are now entering a new era for software development, with the introduction of multicore processors. Tool support and high-level programming and specification languages will be even more important in this new era, implying that the mission of ASTEC must be carried on. It will be exciting to participate and to observe.






Statements from ASTEC industrial partners

  • The ASTEC partners developing the tool are very open for suggestions and try hard to make the tool as useful as possible for our needs. The development went a little slower than expected, mainly because of the underestimated amount of work that was involved in building EVT. However, without the ASTEC cooperation, we would not have had a tool at all.
    ASTEC brought, above all, much knowledge into Ericsson.
    Thomas Arts, (Computer Science Lab, Ericsson Utvecklings AB)

  • The HiPE team has been much more practical and concrete than we expected.
    The HiPE team has proposed and developed a new tagging schema for Erlang which means that Erlang programs have access to the full address space of 4 Gbyte. Their implementation has been incorporated into the Erlang/OTP compiler and this means that it can be presented to the users already in rev 7 instead of rev 8 which means several months earlier.

    Bjarne Däcker (Computer Science Lab, Ericsson Utvecklings AB)

  • The industrial partners of the centre have also contributed to our understanding of the end-user problems when using our products.
    Olle Landström (IAR-systems AB)

  • The initial work carried out in the project has resulted in a tool (FixIt) which scales up better than classical BDD-based techniques on several classes of systems.
    Gunnar Stålmarck (Prover Technology AB)

  • The techniques developed have been used in industrial pilot studies together with ESAB and Rolls-Royce Marine, and are being used today at CC Systems to develop new embedded control systems.
    Jörgen Hansson (CC-systems AB)

  • Some results from HiPE which are now integrated into the product are:
    - Improved Garbage Collection.
    - Native code generation for SPARC and Intel X86 (for evaluation in real products)
    - Compiler improvements and optimizations.
    - Packages , a hierarchical module system.

    Kenneth Lundin (Product Manager of Erlang/OTP within Ericsson).

  • During the first years of cooperation the center was a good way for IAR Systems to recruit skilled students.
    Olle Landström (IAR Systems AB).

  • Our (Enea Embedded Technology, formerly OSE Systems) membership in the ASTEC research group gives us several benefits. It allows us to try out, and influence the development of, some of the most advanced real time analysis tools on this planet.
    Our participation in ASTEC has also led us to participate actively in the european level research community, with many interesting contacts with researchers from UK, Germany, France and Finland.
    Jan Lindblad (Enea Embedded Technology)

  • The ASTEC-work has been done by a PhD student, Johann Deneux. The work is mainly an implementation of known theoretical “formal method” results into a “practical tool”. Doing this is a good example of technology transfer from academia to industry.
    Ove Åkerlund (Prover Technology AB)

  • Participating in ASTEC allows Virtutech to help explore these interesting issues that we would otherwise not have the competence to pursue on our own.
    Jakob Engblom, PhD. (Senior developer @ Virtutech)

  • "We have on top of the original plan made a cash contribution of 500 000 SEK since Dialyzer has been such success within the HiPE project and already shown to be valuable for Ericsson."
    Kenneth Lundin (Product Manager of Erlang/OTP within Ericsson).

  • The research results have been to very big benefit for us. To mentions a few points:
    - Typechecking of Erlang resulted in the Dialyzer tool which now is part of the Erlang/OTP product. Dialyzer is used within several development projects within Ericsson and is a very valuable tool in finding error in early phases (before function test) and this saves a significant costs during development.
    - The bitstring and binary comprehension suggestion (additions to the Erlang language) is very interesting and will be added to the product during 2006.
    - Many small ideas regarding SMP (Symmetrical Multi-processing) support in the Erlang emulator have sprung from the HiPE group and are now implemented in the product. The SMP support is a real important feature since it allows Erlang programs to take advantage of multi-core technology very easily.

    Kenneth Lundin (Product Manager of Erlang/OTP within Ericsson).

  • "Seen from my perspective, the two contributions from Astec which have gone straight into industrial use (in one way or another) are Hipe and Dializer."
    Michael Williams (Ericssson AB)

  • The collaboration with ASTEC on development of Tidorum's WCET tool was useful both directly -- much of the work on a tool version for the Renesas H8/300 processor was completed in 2004 -- and indirectly as it exposed the tool's architecture to outside review and comment. The contact with ASTEC contributed to Tidorum joining the ARTIST2 Network of Excellence, cluster on "Compilers and Timing Analysis" which started in 2004. The ASTEC/WCET work, in 2004 and currently, on improved modelling of the arithmetic computations in a program (interval analysis, pointer analysis) is very interesting to Tidorum and there is a clear need to add such functionality to Tidorum's WCET tool in the future. Niklas Holsti, Tidorum Ltd.

line
Updated Friday, 07-Dec-2007 17:41:45 MET by Roland Grönroos
e-mail: info -at- astec.uu.se    Location: http://www.astec.uu.se/Reports/final/ASTEC_final_report.shtml