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:
- The High Performance Erlang compiler system: this tools is now widely used in the telecommunication industry, and its importance will grow in the future.
- 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
- 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
- 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:
- "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.
- 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.
- "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.
- 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 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.
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:
-
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.
-
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.
- 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.
- 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.
|