Subsections

Dansk Datamatik Center[*]

Abstract

In 1979 a software research and development (R&D) centre was created to demonstrate the power of systematic and formal methods in software development. One of the first and biggest projects at Dansk Datamatik Center (DDC) was to develop an Ada compiler and an Ada run-time system. The US Department of Defense had decided that most future programs should be written in Ada. DDC succeeded in making the first European validated Ada compiler, and the Ada project was carried on in a subsidiary called DDC-I, Inc. which worked successfully from Copenhagen and Phoenix, Arizona. The paper describes the background and the start of DDC and some aspects of the formal development method RAISE, Rigorous Approach to Industrial Software Engineering, as well as other DDC activities.

A Factual History of DDC

The idea of forming DDC was first aired by Christian Gram of the Department of Computer Science at the Technical University of Denmark (DTU). The idea was discussed with his colleague Dines Bjørner during the spring 1979. The background was that software development in business, administration, and industry still was very unsatisfactory. Already in 1968 the NATO Science Committee arranged a conference on software engineering concerned with ``a problem crucial to the use of computers, viz. the so-called software, or program, developed to control their action.'' The problem was that many programs were late, cost much more than estimated, and contained many errors. ``The phrase `software engineering' was deliberately chosen as being provocative, in implying the need for software manufacture to be based on the types of theoretical foundations and practical disciplines, that are traditional in the established branches of engineering.'' A few years later a second conference was held on the same problem area, but problems with software development in practice continued. Dines and Christian felt in 1978 that computer scientists had developed foundations and theories that -- if properly implemented -- could make programming a more professional, engineer-like job and make it possible to develop large, reliable programs on schedule.

We contacted ATV, the Danish Academy for Technical Sciences, because ATV was an umbrella for a significant number of `Science-Engineering-Technology' institutes working to help industry applying the newest technologies in their field. ATV responded positively, and 10 of the largest users and/or producers of IT in Denmark agreed to become members of the institute, each paying 100,000 DKK. per year. On this ground, DDC was created in September 1979 as an ATV society for advanced software development. In a way it was a follow-up on the computer company Regnecentralen which started (in 1955) as an ATV institute for computers (with start-up funds from the Marshall Help). The members were Christian Rovsing A/S, Crone & Koch edb, Danish Defence Research Establishment, Datacentralen af 1959, Jydsk Telefon A/S, Kommunedata, Regnecentralen af 1979 (RC), Sparekassernes Datacenter (SDC), Teleteknisk Forskningslaboratorium (TFL) and ØK Data.

An attempt to make Danish financial institutes interested in DDC failed, and none of them wanted to join the initiative.

Right from the beginning, Dines Bjørner took upon himself to be the scientific leader and inspirator of DDC's activities. The first 3-4 months he also worked as a managing director a.i., until Leif Rystrøm was employed as full time managing director. Other employees were graduates of computer science from DTU and Copenhagen University.

During a period of 10 years, from 1979 to 1989, a number of projects on software tools were carried out. The projects were made in close cooperation with one or more of the members. Typically the projects dealt with methods and techniques for software development as, e.g., the cooperation with SDC on methods and tools for program construction which ended up with a 230 pages report discussing how SDC's software development could be improved . But two larger projects dominated the activities for several years, i.e., the Ada compiler development, sponsored by the Commission of the European Communities, CEC, and the CHILL compiler development in cooperation with the Danish Telecommunications Research Centre. Both projects are described in more detail below.

Most projects used formal specification methods -- VDM, the Vienna Development Method developed at IBM, and later RAISE, Rigorous Approach to Industrial Software Engineering , a method designed and developed at DDC, see below.

A main DDC goal was to act as a link between Danish IT companies and Danish/European IT research, in order to make these member companies capable of using the most advanced software design and development tools. Besides the projects mentioned above DDC arranged a number of courses and workshops to spread knowledge and awareness of advanced development methodology.

The Ada compiler project was so successful that a separate company, DDC International A/S (DDC-I), was created in 1985 to market, sell and further develop the Ada system. DDC-I was formally separated from DDC. DDC-I later created the limited company, DDC-I Inc., which is still in the market, and the Ada system and other systems developed at DDC-I have been sold in USA, China, and other countries. Some years ago DDC-I moved the headquarter to Arizona, USA.

Over the years some of the original member companies lost interest in DDC and the services offered by DDC and it became more difficult to find funding for the kind of projects, DDC wanted to further. Therefore it was decided - after almost 10 years - to close down DDC, but the larger projects were carried on under new hats. The development of Ada systems continued in DDC-I, using the formal methods and framework established at DDC, and DDC's shares in DDC-I were bought by a Danish investor. The RAISE project and the people working on it were transferred to the Danish software house CRI Inc. (CRI), who completed the project and used it as a base for the LaCoS project (Large-scale Correct Systems using formal methods).

The Use of Formal Techniques at DDC

At this point it may be opportune to emphasize the special approach that DDC took to the development of software - as witnessed in its two compiler development projects: CHILL (Sect. 4.4.1) and Ada (Sect. 4.4.2). First we can say this: the approach to software development as propagated also in seminars and courses, and subsequently, after the CHILL and Ada projects, in the RAISE project (Sect. 4.4.3), was that of using formal techniques. In the early 1980s the main tool was the formal software specification language VDM .

Figure ada.fig shows the phase, stage and step-wise approach taken at DDC for the development of compilers.

First a formal description was developed for the programming language in question. Then, in usually three-four stages a requirements specification was developed. These requirements, see the five boxes of the $\mathcal{R}$ ``layer'' of Fig. 1, were systematically, but not automatically, derived, from the formal description as well as from such requirements as ``the compiler shall handle the full language, the compiler shall generate code for 128KB address spaces'' and ``the compiler shall itself reside in a 128KB addressing space''. Before actual coding a specification of a multi-pass administrator and a run-time system was developed. Finally, from the indicated stages of the requirements and from the specification of the multi-pass administrator, the $n$ phases of the compiler were coded. Each of the boxes of Fig. 1 designates (amongst other things) a formal specification. In the case of the two compilers these specifications were expressed in the VDM specification language .

In both compiler development projects the VDM approach was one of systematic development: formal specifications of all phases, stages and steps, but no formal proofs of correctness. See Sect. 4.4.2 for more details.

Figure 1: The DDC CHILL and Ada Compiler Development Graph
\begin{figure}\begin{center}
\epsfig{file=/home/db/ddc/ada.eps,height=11cm}
\end{center}
\end{figure}

DDC Activities 1979-1989

DDC was centered around a succession of projects, some taking place concurrently ``across'' the approximately 35 member professional staff: advanced software development projects: the CHILL and Ada compiler projects, etc.; research: the Ada Formal Definition project, etc.; explorative studies: Formal Methods Appraisal, Office Automation, etc.; seminars; courses; and other dissemination.


The CHILL Projects

The Formal Definition of CHILL

In 1978 Prof. A. Kjerbye Nielsen, an ardent supporter of the foundation and operations of DDC, asked Dines Bjørner to follow the development of the CHILL programming language by an international group of the C.C.I.T.T.[*] (now ITU[*]).

It was, from the start, Kjerbye's intention to attempt a formal description of CHILL. Through the work of Dines Bjørner and his colleague, Hans Bruun, as well as our MSc students (incl. Peter Haff ) such formal descriptions were researched and experimentally developed at the department of computer science at DTU. Once DDC was established, that work was moved to DDC with the employment of Peter Haff (as first professional).

A story may be worth telling: Hans Bruun, in his painstaking analysis of the informal descriptions of CHILL, and in discussions with Dutch and Belgian members of the C.C.I.T.T. CHILL group, found that a tiny little identifier scope issue, if simply removed, would shorten the definition by some substantial percentage (20% was mentioned). At the next group meeting, in Florence, that scope issue was nullified by its simple removal - vastly simplifying any CHILL compiler.

The CHILL Compiler Development

In 1979, before the formation of DDC, work started on the development of a compiler for the full CHILL language. The work was done by Peter Haff and Søren Prehn partially funded by TFL.

The CHILL compiler was for the full CHILL programming language -- with, for example, its three ``independent'' sets of parallel programming constructs. That CHILL compiler was then made public property by TFL and DDC. As such it played a not insignificant rôle in the teaching of CHILL worldwide.


The Ada Projects

The Ada Compiler Project

The Danish/Italian Collaboration and the Initial Contract:
The Ada programming language had been designed on behalf of the US Department of Defense as a new cure-it-all standard programming language targeting development of embedded software. At the time more than 200 languages were in use within the US DoD and a significant savings would be possible if this number could be reduced to just one, Ada.

DDC had heard that the Commission of the European Communities had set aside significant funding for the development of a European Ada compiler system because the CEC thought that similar savings might be possible within European software development. We had also learned that a French/German consortium was slated to receive the funding for this European Ada Compiler System and that the call for proposal would end soon. Ole N. Oest was seconded, and later transferred to DDC from the Danish Defence Research Establishment to manage DDC's Ada activities.

DDC formed a partnership of Olivetti (Italy) and Christian Rovsing (CR) (Denmark) and in record time developed a bid for the funding. It was a requirement that two EC countries be involved and that the proposal was delivered in two EC languages. We wrote the proposal in English and Olivetti established a team of students who then almost overnight translated the entire proposal to Italian so that we could submit it according to the rules. No one ever read the Italian version (probably as well) and we were henceforth allowed to sôlely use English.

Now followed several months of hectic technical evaluations of the DDC/Olivetti/CR proposal. It was very inconvenient, for certain people in the EC, that this Danish/Italian group had surfaced thus providing competition for the money, we had basically thrown a wrench in the machinery.

Each time we went to Brussels for another technical evaluation, the experts found some show-stoppers. It was typically in some part not discussed at the previous meeting. A contract was finally concluded, in early 1981. 50% funding from the CEC and 50% from Danish sources. DDC's part of the project was to develop a portable Ada compiler technology.

Some years later, after the Ada standard had been finalized, DDC won a contract for developing a formal specification of the language. We considered that a significant acknowledgement of VDM and of DDC's high technical level.

Technical Approach:
DDC's charter was as mentioned elsewhere to try out advanced software engineering methods and transfer these methods to industry.

The driving method behind development of the DDC Ada Compiler System was to be the Vienna Development Method (VDM) and this demonstration of the viability of using VDM was initially perhaps considered more important to DDC and its members than the end product itself.

In 1980 a team of five MSc students from DTU under the direction of Dines Bjørner, Hans Bruun and Ole Oest, had developed a formal definition of Ada and of the underlying execution model as their Master's Thesis projects . This specification became the foundation for the actual compiler development. The compiler was developed as a number of refinements of this definition.

It was a requirement on the Danish/Italian co-operation that the Ada compiler should be suitable for mini computers with limited memory resources. The compiler was therefore designed as a multi-pass compiler, and the formal definition of Ada was basically distributed into buckets, where each bucket would correspond to a compiler pass.

Even though the Ada language underwent changes in this period and the host computer platform changed a number of times, the project became a success and resulted in a commercial viable product. The DDC team even managed to achieve formal US DoD approval (validation) of the compiler ahead of the French/German project. This, of course, was considered a significant victory by the young development team .

Although the DDC Ada compiler project was delayed, less than 20%, that resource over-run compared, man-year-wise, well to competition which consumed more than at least double the resources, usually far more.

The First Commercial Sales:
DDC presented the DDC Ada compiler project and the use of VDM at several conferences worldwide.These presentations showed not only the high level of correctness of the compiler but also provided productivity numbers which showed that VDM was a cost-effective development method even when used without the support of computerized tools which only became available much later .

Those technical presentations raised enough interest that Nokia one day knocked on the door to DDC wanted to license the DDC compiler technology for the purpose of developing an Ada compiler for a proprietary minicomputer. In other words, without any sales and marketing organization in place DDC, had succeeded making its first commercial sale of what became known as the DDC OEM Compiler Kit. Nokia represented Honeywell in Europe and had let Honeywell know about DDC and the Ada compiler technology. Honeywell thus came knocking on the door next. Honeywell had two projects needing an Ada compiler: a minicomputer, for which they soon selected DDC, whose technology was well suited for minicomputers, and a main frame computer, for which they were leaning to purchasing from the French/German consortium. However, in the end Honeywell placed both orders with DDC.

The Formation of DDC International (DDC-I):
Several other OEM contracts resulted and, in 1985, DDC created a subsidiary, DDC-I, to commercialize the DDC Ada Compiler System, which came to be used on many long-lived projects (aircrafts like Boeing 777, MD-80 and MD-90, satellites and various military programs) and is still in 2010 generating revenue for DDC-I.

Commercializing the other outcome of the project, the successful use of VDM, turned out to be much more troublesome. The industry was not ready to adopt formal methods until some 20 years later, where formal methods become mandatory in validation of MILS (Multiple Independent Levels of Security) operating systems.


The Formal Definition of Ada

During the early 1980s there was a lively discussion forum, supported by the Commission European of the Communities, CEC, resulting in the CEC supporting the R&D of a formal definition of Ada. A group was formed, again anchored in Denmark (DDC) and again with Italian partners (University of Pisa, University of Genoa, IEI (Istituto di Elaborazione della Informazione, Pisa) and CRAI [Cosenza]). The project covered the period from 1984 to 1987 . The Ada formal definition project was truly a research project. It was not known exactly, from the outset, how the result, , would look: which specific abstraction and modelling techniques to deploy, which abstractions to use, etc. During the project a number of exciting research problems were solved and many scientific papers were published.


The RAISE Project

The RAISE project, in a sense, had two parts: a precursor project, FMA, and the main project, the RAISE development project.


The Formal Methods Appraisal Project (FMA)

During the developments of the CHILL and Ada compilers the need for a revision of VDM was identified. Other formal techniques approaches to software development and, especially additional formal specification constructs had been introduced in the late 1970s and early 1980s. DDC obtained funds under the Multi-annual Programme of the CEC for a Formal Methods Appraisal study . This study took place during 1983-1984. It came up with a number of requirements that formal specification languages ought to satisfy were they to be applied to problems involving distributed, real-time and concurrent systems.

The RAISE Development

We make a distinction between the RAISE project and the RAISE product.

The RAISE Project:
The result of the FMA project was that a basically Danish/British consortium was formed and eventually DDC (DK), ABB (Asea Brown Bovery, DK), ICL (UK) and STL (UK), obtained an initial four year contract with the CEC ESPRIT Programme for researching and developing a successor to VDM.

RAISE was thus initially developed under that contract, from 1985 to 1990, with the aim of providing a unifying improvement over formal methods such as VDM, Z, CSP, CCS, Larch and OBJ. RAISE was later further developed (after DDC) in the ESPRIT Project LaCoS (Large-scale Correct Systems using formal methods), from 1990 to 1995.

RAISE stands for Rigorous Approach to Industrial Software Engineering. RAISE emphasises the use of formal (mathematical) techniques in the development of software: in requirements analysis and formulation, specification, design and development. RAISE offers the RAISE Specification Language (RSL ) and the RAISE method .

The RAISE Product:
There are three facets to the RAISE product. (i) The RAISE Specification Language (RSL) which provides a rich, mathematically based notation in which requirements, specifications and steps of design of software may be formulated and reasoned about. RSL is a wide-spectrum language: it facilitates abstract, axiomatic styles of description as well as concrete, operational styles. It may be used from initial domain and requirements analysis through design to a level at which it may be translated into code; (ii) The RAISE Method which provides a set of techniques and recommendations for how to use RSL in the various life-cycle phases of software development, as well as techniques for verifying properties of specifications, implementations and their relationships, formally, rigorously or informally. (iii) The RAISE Tool Set which supports the use of RSL and the RAISE method.

RAISE comes with comprehensive documentation. Books on the language and method are available. The first on RSL is provided to institutions from which course attendees come (one per institution or one per every two participants, whichever is the larger number, in either case to be given to the institution library). The second on the RAISE method is available by ftp . See for general information about the RAISE product and for information about industrial use of RAISE. See also for web pages from UNU-IIST[*] about RAISE.


The Office Automation Project

DDC concluded several office automation projects during its existence.

In 1981 a study was performed describing office automation systems. An office automation system was understood as a computer based system assisting the office staff in their daily tasks. At the time there was a growing amount of literature and commercial products concerning office automation.

The two main purposes of the project were:

A further purpose of the project was technology transfer established through the project work, since the project was carried out by persons from DDC together with persons from two of DDC's members.

In the taxonomy part of the project the concepts of the office automation area are identified, analyzed and classified. In the terminology part general terms, concepts and abbreviations used within office automation are explained and listed alphabetically. More than 70 items are explained.

To overcome the problems with a general office automation system - not fulfilling the requirements of a specific office - and a tailored system - being expensive to update as the needs of an office changes - a generic office automation system was specified and characterised. The generic office automation system was modelled using the VDM formal specification language. The model was also described informally and could thus be used by persons without knowledge of the VDM language. The project report had an extensive list of 61 references.

Another office automation project in which DDC participated was a project called FAOR (Functional Analysis of Office Requirements). The project was supported by the CEC under the ESPRIT (European Strategic Programme for Research and Development in Information Technologies). Organisations from UK, Germany and Denmark participated in the project, which ran from 1983 to 1987. The Danish participant was a DDC member, ØK Data with DDC as subcontractor.

The purpose of the project was to develop a method, which could help systems analysts in the field analysing and specifying the office automation requirements to IT-systems. The work processes in an office for which IT-support was needed became more and more complex and were often unstructured. The FAOR project addressed this challenge of analysing the complex office work and specifying functional requirements to IT-solutions. The method gives the analyst detailed instructions for the analysis and refers to a set of techniques and tools to use. The method was tried in field studies within the FAOR project with good results. The project is described in .

Technology Transfer Activities

Cubus:

In 1987 DDC expanded its technology transfer activities, bringing its know-how out to Danish IT companies, by introducing a quarterly magazine Cubus[*].

The main content in Cubus was technical and scientific articles. They covered subjects, in which DDC had deep insight from actual project work. The articles were mainly addressed to an IT-knowledgeable audience, but they did not require special knowledge in the subject covered. Besides these articles, Cubus had some articles for a wider audience, and Cubus gave overviews/summaries of conferences, new DDC projects, new DDC reports and coming DDC seminars and courses.

Seminars and Courses:

Through most of its existence DDC arranged seminars and courses. They could cover subjects from DDC projects or often a wider scope, but typically within the area of software design and development. Examples of seminars subjects are: Object oriented programming, Why and how change to the programming language Ada?, Local area data net? and Selling Danish software worldwide?

Reports:
To a large extend the results of DDC projects were publicly available through the reports prepared during the projects. The reports were sold for the reproduction costs. Reports were listed in the magazine Cubus, were mentioned at seminars and courses and information about reports could be obtained by contacting DDC.

Appraisal of DDC

In the mid 80s some 40 people worked at DDC, some part-time but most of them full-time. Of these around 20 had a master degree in computing. The two large compiler development projects Ada and CHILL were successful and lead to usable and useful products. But in the long run it was difficult to derive advantage and profit from these products. Ada did not gain the widespread use we had hoped for in spite of US DoD and CED support. The knowledge and the rights for the Ada system were transferred to the subsidiary DDC-I Inc., which earned money but not sufficient to give a surplus to DDC. CHILL was developed for Danish tele-authorities as a new standard language for the international tele-community CCITT, but after completion CHILL didn't generate income for DDC. At the same time, these products had very little interest for several of the DDC members.

A third large project was the RAISE software engineering method. It was paid for by an EU-contract, and its scope was too ambitious to be of immediate interest for the DDC members. The project was transferred to the software company CRI Inc. and there it was completed and marketed with some success.

Besides the above compiler-oriented projects DDC had a number of smaller software development projects, a.o. concerned with user-friendly software and administrative databases.

To assess what the work of DDC achieved for the Danish software milieu is difficult, but in our opinion the major effects of DDC were as now listed.

(a) Some of the larger Danish IT users and producers became aware of modern software development techniques.

(b) A reliable, DoD-verified Ada system was produced and gave the basis for the incorporated company DDC-I Inc. still existing.

(c) RAISE and LaCoS -- methods and tools for large-scale reliable software development -- were developed and brought to market. The company, CRI Inc., which took over leading staff and main assets of DDC, completed the RAISE project (and conducted the LaCoS project). Subsequently Terma Inc. took over CRI and Terma is today using RAISE and the results of the LaCoS project, notably in its Space Division, a leading Danish contractor to the European and US space programmes.

(d) Between 50 and 100 young masters in computer science got an experience in using advanced software technology, that they carried with them into many other companies in Denmark and internationally.

(e) The following facts can now, with the hindsight of 20+ years, be said to have contributed significantly to the R&D and propagation of formal methods: that DDC undertook and completed (1) the CHILL compiler development, (2) the CHILL formal definition, (3) the Ada compiler development, (4) the Ada formal definition, (5) the RAISE projects, and (6) that DDC completed all these projects with better resource performance and higher product quality than was common in the 1980s.

Acknowledgement

This is not the time and place for thanking those hundreds of people and dozens of institutions for making it possible to create and operate DDC. But we do wish to acknowledge the help of Assoc. Prof., Dr. Hans Bruun (emeritus). Without his diligent and painstaking investigations as how to formalise the static semantics of CHILL and Ada it is rather safe to say that DDC could not have gotten off the ground. In writing this paper we got help from Messrs Peter L. Haff, Klaus Havelund and Jan Storbank Pedersen, and now acknowledge with gratitude this help.

Dines Bjorner 2010-06-01