ASTEC Advanced Software Technology

Final report for Phase 2 the years 1999 and 2000.

Up-to-date information about current activities can be found on the WWW page http://www.astec.uu.se/

Summary

The main results of ASTEC during Phase 2.

• The volume of work carried out has continued to increase with 40% per year.
• ASTEC has developed a critical mass with a clear profile and competence on highest international level in key strategic areas. This is reflected by the increased publication rate and decreased cost per publication to 50% of initial value.
• Impressive and recognized research results have been produced and published in totally 97 publications (58 during phase 2), of both theoretical and practical nature.
• Results from ASTEC work have been transferred and are nowadays used in industry.
• The industrial participation in and contribution to ASTEC has been steadily increasing.
• The production of Ph.D., Lic., and M.Sc. graduates has acquired momentum with 13 degrees in 2000.
• The centre contributes courses to national and local graduate and undergraduate education.
• Network activities such as seminars and meetings has increased from almost absent to several per month.
• ASTEC collaborates with other national research initiatives, and has strong international collaboration links, including several European Community research projects.

Sammanfattning

• Mängden arbete som utförs har fortsatt öka med 40% per år.
• ASTEC har uppnått en kritisk massa med en tydlig profil och inom strategiska områden på högsta internationella nivå. Detta visas av den ökade publikationstakten och minskade kostnade per publikation till 50% av kostnaden 1996.
• Impornerande och erkända forskningsresultat har producerats och publicerats i totalt 97 publikationer (58 under etapp 2) inom både teoretiska och praktiska områden.
• Resultat från forskningen har överförts och utnyttjas nu inom industrin.
• Industrins medverkan och instaser har fortsatt öka.
• Doktors, Licenciat och magisters examina har ökat kraftigt till 13 examina år 2000.
• Kompetenscentrumet bidrar med kurser nationellt och lokalt till både doktorandutbildning och grundutbildning.
• Nätverkaktiviteter som seminarier och möten har ökat till flera per månad.
• ASTEC samarbetar med andra svenska forkningscentra och har starka internationella kontakter inklusive flera EU-projekt.

Contents

• Executive Summary
• Introduction
• Basic Facts
• A. Performance and Development as a Competence Centre
  • A.1. Long-Term Goals and Progress of the Centre
  • A.2. International and National Collaboration
  • A.3. Linkages and Collaboration within the Centre
  • A.4.. the Centre and the Host University
  • A.5. Future Plans and Strategies
• B. Technical Results and Scientific Outputs
  • B.1. Research Programme
  • B.2. Technical and Scientific Achievements
  • B.3. Publications
  • B.4. Examinations
  • B.5. Education and Training Activities
• C. Industrial Relevance, Benefits and Effects
  • C.1. Industrial Involvement and Interaction
  • C.2. Industrial Partners' Expectations
  • C.3. Commercialisation and Technology Transfer Activities
  • C.4. Industrial Benefits
• Appendices
  1. ASTEC business ratios
  2. Partners and persons Phase 2
  3. Financial report phase 2
  4. Project descriptions
  5. Publications
  6. Industrial partners statements at mid-term evaluation.

Introduction

ASTEC has been 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 the first two years, the focus of ASTEC was to connect 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. After the initial phase, a strategic perspective for the long-term development of ASTEC was added, which has led to a focus and build-up of effort in key strategic areas.

Currently, ASTEC has developed into a focussed and distinct research unit, having a broad contact area with a number of companies. It is a natural forum for collaboration, discussions, and new contacts in the software technology area.

Basic Facts

• Research groups at Uppsala University, the Royal Institute of Technology, the Swedish Institute of Computer Science (SICS), and Mälardalen University, working mainly on formal methods, functional, logic and constraint programming, 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. These include companies: ABB Automation Products AB, Ericsson Utvecklings AB, Mecel AB, Telia Validation AB, and Volvo Technological Development Corporation, and
• companies that produce tools for software development: IAR Systems AB, Prover Technology AB, Telelogic AB, UPAAL AB, and Volcano Communication Technologies AB.

Appendix 1. ASTEC business ratios.

Give figures for the development of contributions to ASTEC, man power, publications, degrees and management.

Appendix 2. Partners and persons

ASTEC partners, Board, Scientific evaluators and Staff.

Appendix 3. Economic report for phase 2.

A. Performance and Development as a Competence Centre

A.1. Long-Term Goals and Progress of the Centre

Background

Industrial and academic collaboration should be particularly relevant for research on software systems: many advances in software technology occur in universities but on the other hand the major part of software production occurs in industry. Such a collaboration thus offers the opportunity for industry to exploit recent advances in software technology and for researchers in academia to evaluate the effectiveness of new techniques in a ''real-world'' environment.

Though this observation is probably universal, it is particularly applicable to a country like Sweden. Several major products of Swedish industry, e.g., data communication and process control systems, are to a significant extent based on software. Swedish academia has a strong tradition of research in some areas which have potential applications to software development. The indirect impact of this research on industrial practice, through mobility of individuals and ideas, has been noticeable: functional programming and formal methods have influenced software development in the Swedish telecommunications industry, as witnessed, e.g., by the creation of high-level languages such as Erlang, SDL, and TTCN. ASTEC is intended to build on this tradition, and strengthen direct contacts between academic research and industrial practice, so that advances in academic research can indeed benefit industrial software development, which in its turn can guide the agenda for academic research.

Goals and Strategies

1. carrying out industrially relevant pre-competitive research at the highest international research level which can be both published in leading scientific conferences and journals and exploited by the industrial parties,
2. building up and maintain a critical-mass concentrated research environment for research, graduate education, collaboration, problem solving, and long-term competence development, and
3. being a forum for contact between industrial and academic software researchers.

1. Academic-industrial collaboration and technology transfer require that both parties take an active interest. Therefore, ASTEC work should be conducted with active participation by both industry and academia. Collaboration and technology transfer will thus be built in from the beginning. This strategy has been successful in building strong links between researchers in academia and in industry.
2. Longer-term project planning and the build-up of a concentrated research environment is guided by a strategic research plan. The plan structures the challenges addressed by ASTEC into program areas, more precisely described in Section B.
3. ASTEC runs and supports seminars and workshops for contact between industrial and academic researchers.

History and Evaluations

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 board has conducted two self-imposed internal reviews (April -98 and March -00). Follow-up and administrative work has been taken on by a Research Coordinator (Roland Grönroos, 40%), and was made accessible and transparent by building a WWW structure containing all documents produced within ASTEC.

The First NUTEK Evaluation was not fully satisfied with ASTECs functioning. Its recommendations have been addressed by working out the strategic plan, including new competence areas, appointing the Advisory Board, and strengthening the administrative support. Industrial seminars have been conducted with a largely industrial audience, ASTEC work has been presented at industrial conferences, and ASTEC has developed courses for graduate education.

A follow-up review, conducted by NUTEK in September 1998, showed satisfaction with the measures taken since the first review, and added some recommendations, most of which have now been implemented. 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, has been phased out in favour of work on testing.

Phase 2

ASTEC is recognized and supported by Uppsala University as an important long-term strategic research unit. In written and oral presentations of research in IT at its hosting institutions, ASTEC is referred to as a strong pillar of research in Computer Science, and as a good example of successful collaboration with industry. The basis of academic partners is expanding, and now includes Mälardalen University.

The industrial participation in and contribution to ASTEC has been steadily increasing. The number of companies has grown from 6 to 10 during phase 2. The contributions from companies are now exceed 7 MSEK per year, and cash contributions have grown from virtually nothing to 1.6 MSEK per year. Results from ASTEC work have been transferred and are nowadays used in industry. The centre employs 3 industrial Ph.D. students. Senior researchers at companies are making substantial contributions to ASTEC work. ASTEC researchers and graduates have moved to the industrial partners of ASTEC, and senior ASTEC researchers have part-time appointments with companies.

The production of graduates (Ph.D., Lic. and M.Sc.) has now acquired momentum (5 in 1999, 13 in 2000). During ASTECs operation, three key researchers (Parosh Abdulla, Hans Hansson and Wang Yi) have been promoted to full professor rank, and one to docent (Konstantinos Sagonas), partly in recognition of work carried out in ASTEC. The centre has developed and conducted graduate courses in its area of competence, and is involved in industrially oriented undergraduate education.

A.2. International and National Collaboration

The companies also contribute to the centre's research profile. Several companies are world-leading suppliers of technology for software development, and are thus also on the frontier of international research in the areas of relevance. As examples, Prover Technology AB owns one of the the world's most powerful solver for satisfiability problems, and Telelogic AB is a leader in development of standards for testing of communication and embedded systems.

ASTEC researchers are firmly established in the international research community. Senior researchers are members of program committees in key conferences of the areas of the strategic research plan. For 1999-2000, these include

• CAV (Conference on Automated Verification, where also a 3-hour invited tutorial was given in 2000 by Parosh Abdulla and Bengt Jonsson),
• CONCUR (Conference on Concurrency Theory),
• LCTES (Workshop on Languages, Compilers, and Tools for Embedded Systems),
• RTCSA'2000 (Int. Conference on Real-Time Computing Systems and Applications) there Prof. Hans Hansson was also Program co-chair in 2000.
• RTSS (IEEE Real Time Systems Symposium),
• TACAS (Tools and Algorithms for the Construction and Analysis of Systems). Wang Yi will be Program Chairman in 2001.

Research of ASTEC has received numerous signs of recognition. Two notable examples are that an ASTEC paper received the best paper award of EAPLS -- the European Association for Programming Languages and Systems, at the ETAPS conferences in 2000, and that an international evaluation of Swedish Computer Science research supported by TFR (The Research Council for Engineering Sciences) conducted by prof. Ruzena Bajcsy (NSF), president Gilles Kahn (INRIA), and prof. Jeff Ullman (Stanford) in Nov. 1999 commended ASTEC groups by "over all this is a success story. It has the right combination of theory and practice".

ASTEC has a strong network of international contacts. As examples, the UPPAAL project has been collaborating very closely with Aalborg University in Denmark since 1995. ASTEC groups have has long been an active collaboration with Seoul National University (SNU) (Professor Sang Min from SNU was appointed as a senior lecturer during 1998-99, and Andreas Ermedahl (ASTEC Ph.D. student) has visited SNU for 6 months 2001), and with. C-Lab in Paderborn, Germany (including a longer visit by Dr. Peter Altenbernd visited ASTEC during 1997). Other international collaborations involving longer mutual visits include Rice University, Bell Laboratories, Paris Univ. 7, and Dortmund Univ.

In addition to visits within the collaboration just mentioned, ASTEC attracts both long- and short-term visitors. As an example, Dr. Thomas Noll was on a one-year visit to the Department of Teleinformatics at Royal Institute of Technology (KTH) from the Department of Computer Science at RWTH Aachen. During this visit he was actively participating in the ASTEC work on verification of Erlang code.

Through its partners, ASTEC participates in several European Community research projects. The WOODDES (Workbench for Object Oriented Design and Development of Embedded Systems) project is devoted to development technology for embedded systems in automotive and telecommunication industry within the framework of UML. The project has 6 industrial partners (Peugeot-Cit"oet, Verilog, Greek Telecom/INTRACOM, I-logix, Commissariat `a l'Energie Atomique and Mecel AB) representing European automotive industry, telecommunication and tools developers and 2 academic partners: Oldenburg University, Germany and Uppsala University. The European VERIFICARD project will study security aspects of the JavaCard programming platform for Smartcards, by means of software verification techniques. A contribution will be to adapt work on compositional proof techniques developed within ASTEC. The ADVANCE project "Advanced Validation for Telecommunication Protocols'', will develop tools that extend the power of formal analysis. Its partners include Uppsala and Ericsson. Our participation in all these projects builds directly on ASTEC work.

The national research programme ARTES which supports research and promotes graduate education, hosted at Uppsala University and funded by SSF (The Swedish Foundation for Strategic Research) with a budget of 88MSEK during 1998-2002, was initiated in 1998 with the support and involvement of several ASTEC researchers. Currently, Prof. Hans Hansson is program director, and he and Parosh Abdulla and Wang Yi conduct projects funded by ARTES. There is a close coordination between ASTEC and ARTES work: the two bodies share Roland Grönroos as research coordinator, and several ASTEC projects are closely related to ARTES projects.

ASTEC has co-organized several international workshops and conferences, including NWPT '99, the 11th Nordic Workshop on Programming Theory, in Uppsala, October 1999, and FTRTFT '96, the Fourth International School and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems in Uppsala, Sept. 1996. A collection of scientific papers, which represent ASTEC work, has been jointly submitted to the Springer Verlag journal STTT (Software Tools for Technology Transfer), together with a cover paper which presents the ASTEC framework, with the goal of presenting ASTEC to a wider scientific community.

ASTEC conducts technical seminars, and seminars directed to an industrial audience. Industrial one-day seminars have been conducted on the topics of Automotive software development (Gothenburgh 1999) and on Software development for the Telecom industry (Stockholm 1999). Topical seminars include regular one-day seminars on Verification Tools, on Programming Languages and Implementation. In addition, one-day seminars have been organized on topics like Security, and on Design Patterns.

A.3. Linkages and Collaboration within the Centre.

ASTEC Organisation and Meetings.

ASTEC is organised around the agreement between NUTEK, Uppsala University and the 10 industries (see appendix 2). The work has been regulated by a number of contacts with the main aim to provide research results to the participating industries. Within Uppsala University, ASTEC is a separate financial unit, hosted by the Department of Information Technology. All personnel involved in ASTEC are employed by the participating institutions and companies.

Management

The board (see appendix 2) has been formed by persons from the participating companies and universities. All funding decisions are taken by the board. The board follows activities through project reports every 6 months, and contributes to ensuring the industrial relevance of ASTEC work. The board also take part in the long term development and strategic planing of ASTEC.

The director (Bengt Jonsson, Uppsala University) carries out the daily and long term management and the decision taken by the board, initiate meetings, and keep contact with the scientific advisors.

The Scientific advisory board (see appendix 2) comments on long-term project planning and on project proposals and has also conducted 2 internal reviews the years 1998 and 2000.

The research coordinator (Roland Grönroos, Uppsala University) take care of daily administrative matters, prepare reports in cooperation with the director, arrange seminars and meetings, collect and prepare board meeting material.

Project leaders (see appendix 2), Proposes new projects and project areas, lead and carry out the day to day research in cooperation with industrial and academic staff.

Meetings

ASTEC-seminar series (see http:// www.astec.uu.se/Seminars) consist of scientific or industrial presentations in the area of software technology. The volume has increased from a few seminars per year to 10 and 28 for 1999 and 2000 respectively. There is now about one seminar each week during the semesters.

Project leader meetings (project leaders ca 7-8 persons) are held about once a month for information, planning and generation of new ideas.

Board meetings there have been 10 board meetings during 1999-2000.

Workshops, ASTEC has arranged 3 workshop meetings for the entire ASTEC during phase 2. The aim has been to increase contacts between industry and academia, plan projects and present results within the center.

Public seminars with substantial ASTEC involvement

• ASTEC Telecom software seminar May 20 1999 at Ericsson, Älvsjö, Sweden.
• Workshop on Security, Middleware, and Languages, Stockholm, June 15-16, 2000
• Sixth International Erlang/OTP User Conference, Tuesday October 3, 2000. Ericsson, Älvsjö, Sweden.
• Competence center day 2000 ( see www.astec.uu.se/cc-day2000/), ASTEC was one of the hosts at the NUTEK competence center day last year.

The scientific work in ASTEC is carried out in cooperation between the participating research groups, both in industry and academia. Beside the flora of formal meetings mentioned above there are many informal links, discussions, and technical links between projects within ASTEC.

An example of close coordination between different activities in ASTEC is the synergy between the Whole-Program Optimization (WPO) and Worst-Case Execution Time analysis (WCET) projects are collaborating around a common tool and algorithm base. They have common needs in that both projects need to have information about a an entire program, and not just individual source files. A research compiler based on a commercial product of IAR Systems AB has been used by both groups, and Jakob Engblom of the WCET project has been actively involved in developing an industrial proof of concept implementation of a WPO compiler at IAR. Also, the compiler infrastructure of the WPO project is used in the WCET project to research program flow analysis, and as a basis for the necessary gathering of information about an entire program.

The links between industry and academia are strengthened by the fact that several key researchers are appointed jointly by academia and industry. For instance, Parosh Abdulla is part-time employed by Prover Technology, thus bridging the development of techniques which occurs within the company with the development in academia. ASTEC currently employs 3 industrial Ph.D. students, which are part-time employed by companies to carry out research in ASTEC projects.

The contacts within ASTEC have inspired new contacts and collaborations between companies. Joint M.Sc. projects have been defined. The testing project involves 3 companies, and has also indirectly inspired technical contacts with other companies in ASTEC.

A.4. The Centre and the Host University

During the last several years Uppsala University has taken several measures in order to increase the visibility and operational efficiency of its educational and research programs in the information technology field. In 1998 the various small departments dealing with different aspects of IT were joined to two large departments, one in the Faculty of Science and Technology, the other one in the Faculty of Social Sciences. In order to help coordinate the work in these two departments and to increase the collaboration between the IT field and other fields at the university the "virtual IT faculty" was created. The head of the IT-faculty was appointed vice-rektor/rektorsråd i.e. senior advisor to the rector of the university, thus putting information technology on the same level as undergraduate education, graduate education and external relations in terms of the central university organisation. Several new chairs in the information technology field have been created and the already very extensive educational programs have been expanded both in terms of number of programs and courses and number of student positions.

ASTEC has been part of this development both in the sense that the program has had advantages from it and that the activities within ASTEC have been seen as part of the focus on IT at Uppsala University. The head of the IT-faculty, Ewert Bengtsson has also served on the ASTEC board thus linking the program directly to the central university organisation.

The merger of the two departments which had most of ASTEC activities at Uppsala University into the new IT department has facilitated many administrative routines. ASTEC is formally a separate administrative unit within Uppsala University. The administration is hosted in the IT department but the accounting is separated from that of the department.

ASTEC is together with a few other strategic research programs always presented as an important part of the research strategy of the university. It can for example be reached through only two obvious mouse clicks from the central web-page of Uppsala University, in contrast to most activities at the university which usually require many more or less obvious linking steps. ASTEC is (almost) always mentioned in accounts of the research program in Computer Science at Uppsala University. Examples include STUNS report, and presentation of Research in IT to representatives of the leadership of research at SUN and ABB.

Several of the new faculty chairs that have been created in the last years at Uppsala University (and also Mälardalens Högskola) are in areas that support ASTEC work, including real-time systems, computer architecture, computer communications, and computing science. ASTEC has indirectly catalyzed the creation of some of these chairs.

ASTEC researchers are involved in graduate and undergraduate teaching, and development of courses within its area. More details can be found in Section B.5.

A.5. Future Plans and Strategies

The future plans and strategies follow the goals outlined in the introduction and ASTEC's long-term goals described in Section A.1. They also include direct input from the industrial and academic partners, and from the recommendations given by ASTEC's International Scientific Advisory Board.

ASTEC projects that are state-of-the-art and have reached a sufficient level of maturity (e.g., HiPE, SMC) will strive towards achieving a complete technology transfer and become (or be integrated into) a commercial product. Similarly, projects that are successful in their prototype phase (e.g., ErlVer, WCET) will aim towards becoming more usable or integrated into an existing tool. In both cases, additional efforts (e.g., in the form of case studies) and closer collaboration between the academic and industrial partners will be required to evaluate and tune the performance/effectiveness of the resulting system in its actual industrial uses. The time investment, although substantial, is expected to have a substantial impact to industrial partners and achieve ASTEC's long-term goals.

Projects that are somehow related or whose research/application areas partly overlap should interact further and achieve greater cooperation between them. Also, as pointed out by the Scientific Advisory Board, greater interaction between other researchers in Sweden working on similar topics or projects is strongly desirable. ASTEC will encourage these activities more in the form of theme workshops or seminars.

On the educational side, ASTEC will continue its successful upper-level undergraduate courses (on verification, real-time systems and compiler technology) at Uppsala University, and will try to enrich them with new courses of current interest (e.g., a course on security of programming languages for the internet). Efforts will be made to also attract in them students from geographically close universities and encourage the participation from members of the industrial partners of ASTEC in its regular seminar series.

Last but not least, although it is expected that the research areas and application fields of ASTEC (see Section A.4) will remain as currently, ASTEC's competence and expertise should be also be applied in new research areas of active interest. Examples of new research activities currently under consideration include application areas related to the internet, and verification of safety and security properties of code for distributed applications. Also, it will be investigated to what extent experiences gained from working on an existing ASTEC project can be applied to a similar project of related nature: e.g., how techniques developed within the context of verification project can be applied to debugging, simulation, and other forms of validation of multi-threaded applications.

B. Technical Results and Scientific Outputs

B.1. Research Programme

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.

• 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.

Table 1. ASTEC projects per programme area 1999-2000.

The projects acronyms stands for:
Auto: A design methodology for embedded real-time systems
BUS: Modeling and analysis of a industrial bus protocol
ErlVer: A Verification Method for Erlang
HiPE: High Performance Erlang
SA: Analysis of types and process topology for static debugging
SMC: Symbolic Model Checking
Testing: Automated Testing
WCET: Calculation of Worst-Case Execution Times
WPO: Whole-Program Optimization in Compilers for Embedded Systems

A notable feature of projects carried out under the aegis of ASTEC is that state-of-the-art academic research can have access to production-size industrial-quality software, given as source code, which can be used to conduct experiments. 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 toy benchmarks.

B.2. Technical and Scientific Achievements

Software for Automotive and Vehicle Applications

Within ASTEC, several case studies using UPPAAL have been carried out 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 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. Recently a start-up company based on BUTLER has been established by the main developers of BUTLER.

Embedded systems often contain an interaction between discrete control and continuous behaviour, which must be modeled by a combination of discrete automata and differential questions, resulting in so-called hybrid systems. A tool for animating a hybrid system based on a mathematical definition of its behaviour has been developed and evaluated in case studies. The animator is being integrated with UPPAAL.

In recent years, there has been 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 (to appear) lays a foundation for such tools by providing a formal semantics for a significant portion of UML. Future plans include the development of UPPAAL as a plug-in module in commercial UML tools to support automated analysis of UML models integrated with timing information.

Software for Data- and Telecommunication Systems

ASTEC's vision is that development of communications software should be conducted, not by large organisations with heavy software development processes, but by small, well-qualified teams working with powerful development tools to turn an innovative idea into a product. 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. In this respect, ASTEC has been actively involved in the development of the Erlang programming language, both at the level of their efficient execution (cf. the HiPE system) and at the verification of applications written in Erlang (cf. the EVT tool described below).

An another important aspect of work that falls under this application area is the development of compilation techniques for embedded systems software, in which the code size of the programs is a very important consideration. Smaller code size means that the hardware can be made cheaper and have decreased power consumption. Minimizing code size by compression techniques at the level of source code and by employing manually clever tricks at the level of memory layout is a tedious and error-prone process for embedded software engineers. The ASTEC WPO project is working on powerful techniques for automatically shrinking the compiled code of such programs.

Validation and Verification Technology

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

Software for telecommunication systems often possess 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: 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.

ASTECs effort to develop new and more efficient symbolic verification techniques for finite-state systems have generated very interesting results. The FixIt tool which adapts standard algorithms for symbolic reachability analysis to work with SAT-solvers, such as Stålmarck's algorithm, instead of the classical technique based on Boolean Decision Diagrams (BDDs). Although BDDs have been the dominating tool in symbolic model checking for the last 15 years, the FixIt technique scales up better on several classes of applications. Furthermore, we have recently extended SAT-based techniques to deal with systems with infinite-state spaces, which are beyond the capabilities of BDDs.

The project on modeling and analysis of an industrial bus protocol was a very interesting case study, embodying one of the few full-scale applications of automated verification to a communication protocol used in process control industry. At ABB, several abstract models of a working Bus Protocol have been developed and analyzed using the UPPAAL tool. To our knowledge, this is the largest case study where the UPPAAL tool has been applied, involving 150 pages of protocol specification, and about 2000 lines of Modula-2 code. Various imperfections in the protocol logic and its implementation have been found, and respective improvements have been suggested.

An interesting example of how practical problems can inspire advances in fundamental research is the development of the regular model checking paradigm, presented in Marcus Nilsson's Lic. Thesis. The original inspiration was to improve the techniques for formally verifying systems of unbounded size, e.g., a bus protocol designed for an arbitrary number of nodes or processes, which are considered in the case study project at ABB, or in the effort to verify Erlang code. Through a sequence of papers, the approach was distilled and generalized, so that it is now formulated in basic automata-theoretic terms. It extends the techniques of basic automata theory by a powerful technique for computing, e.g., the set of configurations that may occur in a run of a Turing machine. The new general formulation is able to handle not only systems with an arbitrary number of components, but also several unbounded data structures, such as arrays, queues, and stacks.

We are applying techniques, developed within the formal verification, to improve techniques for testing of software. Techniques have been developed 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. Such translations exist in automated verification tools, such as UPPAAL, but they are also finding other applications. Among our contributions is to consider new types of constructs in formal specifications, which are relevant for embedded systems, for communication software, and for WWW-based internet services. Such a translation can potentially save much effort in writing test programs or test scripts, and they link requirements to the actual system behaviour in a direct way.

Programming Language Implementation and Compilation

The biggest effort in this area has been centered around the Erlang language. Erlang is a concurrent, strict, functional programming language designed to ease the development of large-scale distributed control applications. So far, it has 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). This has happened despite the fact that Erlang implementations are based on emulators of virtual machines and their performance is slow, even compared to implementations of other functional languages.

The work aimed to improve the performance characteristics of Erlang implementations has concentrated on the development of the HiPE (High Performance Erlang) system. HiPE is an efficient just-in-time native code compiler for Erlang programs incorporating many compiler optimizations which have been proven successful in the context of similar programming languages. In addition, many other compiler techniques have been adjusted and sometimes developed taking the characteristics of Erlang into account. These include support for concurrency, communication, distribution, fault-tolerance, on-the-fly code reloading, automatic memory management, and preservation of tail-recursion in the context of a mixed mode (i.e., emulated and native code) execution. The HiPE system, based on Open Source Erlang (OSE), has been publicly released as open-source in March 2000. It is currently the fastest Erlang system and is competitive in performance with implementations of other functional programming languages such as Concurrent ML.

During the last year, the "HiPE group" has also initiated stronger contacts with the Erlang/OTP development teams which are responsible for the Open Source Erlang implementation. This cooperation has already resulted in important technology transfer from academia to industry: a new data representation which removes the address limitations of OSE has been incorporated in Ericsson's current development version released in September 2000 (see also www.erlang.se). Other efforts are currently underway to transfer more technology and successful compilation techniques from HiPE to OSE. The eventual goal is to merge the two systems.

The WPO (whole program optimization) project has focused on the development of compiler optimization techniques for embedded systems. In embedded systems, memory is an expensive and sometimes limited resource, and thus it is desirable to find techniques that lower the hardware costs by reducing memory usage of programs for embedded system through efficient memory allocation techniques and code compression. In the context of this effort, algorithms for code compaction through a technique called procedural abstraction have been investigated. In procedural abstraction, the program control flow graph is scanned for semantically equivalent graph fragments, which are then factored out into a new procedure. The project has investigated the effectiveness and advantages of applying procedural abstraction at the level of intermediate code. It was found that doing so provides opportunities for more powerful code compaction by e.g., not interfering or be negatively influenced by the effects of register allocation or of other compiler optimization steps.

In order to correctly evaluate the effectiveness of the new compilation techniques developed, ASTEC projects have collected source code from industry sources and used them to evaluate tools and drive research in directions relevant for industry. The work has also generated two publications regarding how to benchmark tools for embedded systems.

Real-Time Distributed Systems

This area considers the particular challenges that arise when building embedded real-time and distributed systems. The emphasis is on the needs of software that operates under tight timing constraints and with high requirements for correctness. Analyzing and verifying the timing aspects of a system is the least understood and thus the most difficult part of developing embedded real-time systems. Reliable estimates of computation times are necessary for scheduling and resource allocation, and for analyzing whether a program will meet all deadlines.

ASTEC has produced a sequence of results related to the problem of calculating the worst-case execution time (WCET) of a code module. The main industrial partner is IAR systems, and the ultimate goal is to integrate WCET analysis into a commercial tool for development of embedded systems.

The WCET research in ASTEC has proposed an architectural framework for how to integrate the WCET calculation into a development tool used for real-world programs, and used this architecture as driver to generate research problems and to integrate research results. Part of the framework consists of target- and method-independent data representations which help making WCET tools retargetable and flexible. The initial steps in the framework were formulated in the M.Sc. thesis of Jakob Engblom (at ASTEC), which received the SNART award for best real-time M.Sc. thesis in Sweden in 1998.

On the software side, the execution time of a program depends primarily on the program flow and the timing aspects of the hardware used to run it. In Jan Gustafsson's Ph.D. thesis, it is demonstrated how techniques used for flow analysis in compiler research, such as abstract interpretation, can be employed to automatically extract flow information of a program, which is an important step towards an automatic WCET analysis tool.

On the hardware side, in order to yield reasonable and safe execution time estimates for a code module, the timing effect of processor pipelines must be addressed. A conceptually simple but powerful technique for analysing the effect of pipelines has been developed. The technique makes it easy to integrate the results of high-level program flow analysis and analysis of cache memories. Since the technique only depends on having a cycle-accurate simulator for the CPU available, it can easily be ported to new target architecture, which is very important in the highly fragmented embedded systems market.

Novel tool technology like WCET also needs appropriate packaging as a product in order to become mainstream. To better understand the needs of engineers in the field and guide research in relevant directions, a questionnaire and interview survey was conducted in 1997. We investigated the current methods for timing analysis in industry and the requirements on a static WCET tool.

Given information about the timing of each program part, analyzing the interaction between different nodes in a real-time distributed system is a very difficult problem. Here, the UPPAAL tool has been used in several case studies, reported in earlier sections, to show how such problems can be tackled analytically instead of using extensive testing (which is inherently unsafe and thus unsatisfactory for safety-critical systems).

Some Selected Highlights.

• The result on the use of SAT-solvers for symbolic verification techniques for finite-state systems. The paper on the tool FixIT received the best paper award of EAPLS -- the European Association for Programming Languages and Systems, at the ETAPS conferences in 2000. The ETAPS conferences receive a total of several hundred submissions.
• Flexible techniques for calculation of pipelines on execution times of programs
• The development of the regular model checking paradigm,

• The HiPE compiler, which has been publicly released, and
• the Erlang Verification Tool.

• the modeling and verification of a large bus protocol at ABB, which is in industrial use,
• compilation and benchmarking of the AXD/301 ATM Switch, and
• formal verification of a core part of the Mnesia distributed database in Erlang.

Short data for each project can be found in Appendix 4.

The ASTEC publications can be found in Appendix 5 .

B.4. Degrees

B.5. Education and Training Activities

• Upper-level undergraduate and graduate courses have been developed and given on Testing and Verification, Real-Time Systems, Compiler Technology, and Theory of Distributed Systems, by senior researchers in ASTEC.
• A national graduate course on modeling and analysis of Real-Time Systems has been developed and conducted (in collaboration with ARTES)
• In collaboration with ASTEC companies, one-semester project courses, with 20 participating students, have been conducted. It will most likely be given regularly in the future.
• ASTEC Companies are providing many guest lecturers for undergraduate courses given at Uppsala University and KTH, which helps to bring industrial aspects into university education and providing students with some impression of the realities of software development practice. For example, senior scientists at Prover Technology AB give lectures at the courses on Programming Theory and Software Engineering, and IAR Systems gives lectures in Compiler- and Real-Time courses.

C. Industrial Relevance, Benefits and Effects

C.1. Industrial Involvement and Interaction

The industrial involvement in ASTEC has increased during the last 3 years when measured as in natura and cash contributions (see figure). The number of companies has grown from 6 initially to 10. The industrial involvement is particularly strong on the level of individuals: many companies have reorganised and changed names during the period, but the involved personal contacts has been increasingly strong and expanding.

A company UPAAL AB was started in 1999, to a large extent because of experiences from previous projects and to take on new tasks. It is to provide consulting service in the area of modeling and verification of timed systems. The long-term goal is to develop and commercialize UPPAAL as a plug-in tool for verification and debugging of real time embedded systems.

Two companies has left the centre after the first phase. Rational Software Scandinavia AB (initially Objectory AB) moved research and development from Sweden to the US, and consequently withdrew from ASTEC. Ericsson Radio AB was initially involved in a case study, one of whose conclusion was that the technique applied in ASTEC performed well on one case study but would probably not perform as well on other important future applications.

Mobility between academia an industry is examplified by the following.

• Currently, the centre employs 3 industrial Ph.D. students (Jakob Engblom, Johan Runesson, Jan Sjödin). The students are employed half-time by a company in order to carry out their Ph.D. work in collaboration with the company. A 4th position has been announced and is being filled.
• Senior researchers at companies are making substantial contributions to projects.
• Senior academic researchers have moved to industrial partners. Examples are Thomas Lindgren and Ken Tindell, who are now valuable connections and discussion partners in industry
• A number of M.Sc. graduates have moved to ASTEC industrial partners.

C.2. Industrial Partners' Expectations

• to get in contact with state of the art research and techniques
• to benefit from these contacts
• to solve complex problems in simple ways, for specific info see Appendix 6
• to find new ways to solve problems

C.3. Commercialisation and Technology Transfer Activities

An industrial success story is the development of BUTLER by Mecel, partly performed within the Auto project of ASTEC. BUTLER is a tool set for structuring requirements and design models for automotive systems. Recently a start-up company, named Systemite, based on BUTLER has been established by the main developers of BUTLER.

C.4. Industrial Benefits

ASTEC work has also provided concrete solutions to company problems, "HiPE has been highly beneficial to us at Ericsson Utvecklings AB where we develop the Erlang/OTP product. During the six months of year 2000 we have achieved very concrete results in a short time thanks to assistance from HiPE." writes Kenneth Lundin, Ericsson Utvecklings AB.

Discussions conducted within ASTEC have generated contacts and ideas that resulted in industrially successful projects. An example is an M.Sc. project in collaboration between Volcano Communication Technologies and Mälardalen University, which developed new algorithms for scheduling analysis that are now incorporated into Volcano products.

An appreciated benefit is the potential for contacts with the international scientific community. As examples, six researchers in ASTEC's network of contacts from Korea, USA, Germany, and the UK have held research seminars at IAR Systems in conjunction with visits to Uppsala. Some presentations have concerned direct commercial collaboration.

One of the major advantages of ASTEC is its building of stable and long-term contacts between industry and academia. As Olle Landström, IAR System AB, writes: "The best results come from the projects not originally planned for but emerging in the creative environment where researchers meet the industry based developers."

Appendix 6 collects some statements from companies within ASTEC.

Appendices

1. ASTEC business ratios
2. Partners and persons Phase 2
3. Financial report phase 2
4. Project descriptions
5. Publications
6. Industrial partners statements at mid-term evaluation.