Annual Report 1997

2 Status of implementation of projects

1. Computing Science Research with Fellows

2. Advanced Software Technology Development with Fellows

3. Fellow Training

4. Post-graduate/Post-doctoral Computing Science Courses

5. Events with Fellows

6. Dissemination

All projects are designed to serve the public and private sector institutions of developing countries by increasing self-reliance in the following three areas:

• [(a)] own development, by industry, of advanced software technology

• [(b)]highest-level post-graduate software engineering education

• [(c)] internationalised computing science research

Likewise, the post-graduate courses and the seminars and events sponsored or organised by UNU/IIST fit into UNU/IIST's research and advanced development agenda.

UNU/IIST's emphasis is on research into, advanced development of, and training in methods for the development of Real-time, Reactive, Hybrid and Safety Critical Systems and Software Support for Infrastructure Systems -- the former a major focal point for international research and the latter a major concern in the socio-economic development of developing countries.

2.1 The Research Agenda

2.1.1 DeTfoRS - Design Techniques for Real-time, Reactive and Hybrid Systems

Abstract

Real-time hybrid systems form an important class of today's computer-controlled systems, such as computer controlled lifts, robots, assembly lines, etc. Typically they are computer-embedded systems, where computers interface to and control physical equipment. Such systems are often required to respond to externally generated stimuli with specified real-time constraints. System safety and reliability are extremely critical.

The DeTfoRS project conducts research with UNU/IIST Fellows and Visitors on formal design of real-time hybrid systems to ensure their crucial requirements.

The DeTfoRS approach is based on the Duration Calculus (introduced by Zhou Chaochen, C.A.R. Hoare and Anders P. Ravn in 1991). Duration Calculus, abbreviated as DC, is a logic for specifying and reasoning about the duration of states over intervals of time, where states are boolean functions of time, and the duration of a state over a time interval is the accumulated time of the state presence in the interval. DC has attracted considerable attention from the international research community, and dozens of reports on DC have been published since 1991. UNU/IIST, as one of the main research centres for DC, has become an acknowledged leader in this field.

Staff responsible

  
Zhou Chaochen
Dang Van Hung
Xu Qiwen

Fellows

  
Gao Jianping: 2 September 1996 -- 9 September 1997, PRC
Pham Hong Thai: 1 September 1996 -- 31 May 1997, Vietnam
Zheng Tao: 2 January 1997 -- 30 August 1997, PRC
Wang Hanpin: 30 January 1997 - 20 September 1997, PRC
Suman Roy: 1 June 1996 -- 29 August 1996, India
Suman Roy: 1 October 1996 -- 26 January 1997, India
Qiu Zongyan: 30 January 1997 -- 27 September 1997, PRC
Li Xuandong: 11 April 1997 -- 23 August 1997, PRC
Arun Pujari: 15 April 1997 -- 8 July 1997, India
Fu Hong Guang: 12 February 1997 -- 11 May 1897, PRC
Rana Barua: 15 May 1997 -- 14 August 1997, India
Xia Yong: 1 September 1997 -- 30 June 1998, PRC
Zhao Jianhua: 27 August 1997 -- 27 August 1998, PRC
Pablo Giambiagi: 5 September 1997 -- 28 Feburary 1998, Argentina
Victor Braberman: 14 September 1997 -- 28 Feburary 1998, Argentina
Gerardo Schneider: 1 September 1997 -- 28 February 1998, Uruguay
Hu Chungjun: -- 30 November 1997 -- 30 April 1998, PRC

Visitors

   
Michael R. Hansen: 28 May -- 28 July 1997, Denmark¹
Paritosh K Pandya: 27 August 1997 -- 27 October 1997, India
P S Thiagarajan: 18 -- 21 May 1997, India
Anders P. Ravn: 2 November -- 2 December, 1997, Denmark²

Partner Institutions

   
Beijing University, P R China
Beijing University of Aeronautics and Astronautics, P R China
Changsha Institute of Technology, Hunan, P R China
Chengdu Institute of Computer Applications, Academia Sinica P R China
Institute of Information Technology, Hanoi, Vietnam
Nanjing University, P R China
Tata Institute of Fundamental Research, India
Technical University of Denmark
University of Hyderabad, India
University of Buenos Aires, Argentina
National University of Hanoi, Vietnam

Outputs

   In 1997 UNU/IIST staff and Fellows, together with visitors and collaborators, have studied new techniques and DC-based techniques for specification, refinement and verification of real-time, reactive and hybrid systems, and also tools to support these techniques. The achievements include:

1. Some new specification and verification techniques for designing real-time reactive systems have been developed. These are two-dimensional time interval logics, which can express the behaviour of real-time reactive systems both at the abstract and at the detailed level, and hence can help make the development of these systems easier. With these techniques, one can also specify and verify unbounded liveness and fairness easily.

2. A new variant of Duration Calculus, which includes super-dense states, fixed points and infinite intervals is proposed. Based on it, a comprehensive theory of sequential hybrid systems has been developed.

3. A geometric approach to solving the inverse kinematics for all 3-joint placeable robotic manipulators. This technique might be generalised to 6-joint manipulators as well.

4. Mechanical verification of the Biphase Mark Protocols using DC model and PVS³/DC tool; the results can be applied to choose an optimal value for the parameters of the protocol used in industry.

5. A comprehensive proof of the decidability of an important class of DC under synchronous interpretation. The result shows that one can check the consistency of real-time requirements by an algorithm.

6. Techniques and tools to check a class of real-time, hybrid, parallel systems for linear Duration Calculus invariants, an important class of DC formulas in specifying real-time, hybrid systems. That means that in many cases we can decide the correctness of a system automatically by using a computer. This is a great help for system designers since verification is not only tedious but also very difficult and complicated.

7. Deductive verification techniques for real-time parallel systems. In particular, the assumption-commitment rule is embedded in two-dimensional Duration Calculus.

8. An initial attempt to formalise the semantics of shared variable parallel programs, aiming at eventually formalising the semantics of Verilog (a hardware description language widely used in VLSI design).

9. Specification and verification of a fault-tolerant algorithm in hybrid systems.

The research achievements in 1997 resulted in 11 reports and 3 technical notes ([1][2][3][4][][6][7][8][9][10][11][12][13][14]).

2.1.2 Descartes - Design Calculi and Research for Telecommunication Systems

Period

1 January 1996 - 31 December 1997

Staff responsible

Kees Middelburg

Abstract

The UNU/IIST Research Project DesCaRTeS is concerned with rigorous approaches to software development in telecommunications. The project concentrates on formal techniques, and tools supporting them, to complement SDL (Specification and Description Language). In particular, it is aimed at enabling better grounded validation of SDL specifications and at enabling design steps made using SDL to be justified by formal verification.

Fellows

  
Radu Soricut: 1 September 1996 - 31 May 1997, Romania
Bogdan Warinschi: 1 September 1996 - 31 May 1997, Romania
Yaroslav Ussenko: 1 September 1996 - 31 May 1997, Ukraine

Visiting Researcher

   
Jan Bergstra: 1 May 1997 - 31 May 1997, the Netherlands⁴

Partner Institutions

  
University of Bucharest, Romania
Taras Shevchenko University of Kiev, Ukraine

Outputs

The technical reports [15][16][17][18] represent the achievements of this project. They address the following topics: (1) a process algebraic underpinning of the time-related features in SDL; (2) a model for an operational semantics of SDL that permits a link up with logics for expressing and analysing behavioural properties; (3) a logic to express and analyse behavioural properties of systems described in SDL, including time-related ones; (4) a model for an abstract semantics of SDL that matches the concepts around which SDL has been set up and thus facilitates devising proof rules for SDL.

In the period September 1997 - December 1997, three-week DesCaRTeS Training Seminars were delivered in Indonesia, Pakistan, Brazil and South Africa. These seminars comprised (1) a one-week course, at post-graduate/post-doctoral level, on SDL, its use in software development, and selected research topics of the DesCaRTeS project; and (2) a two-week workshop, for four to six selected participants, with exploratory research experiments on topics of the DesCaRTeS project. Three participants in the workshops have been identified for UNU/IIST-sponsored PhD Fellowships at Utrecht University (Netherlands) where this work will be continued.

2.2 The Advanced Development Agenda

2.2.1 Introduction

The Advanced Development Projects of UNU/IIST are loosely grouped by the idea of "Software for Infrastructures", and this notion should be clarified.

According to the World Bank, "infrastructure" is an umbrella term for many activities referred to as "social overhead capital" by some development economists, and encompasses activities that share technical and economic features (such as economies of scale and spill-overs from users to non-users). UNU/IIST takes a more technical view, and sees infrastructures as concerned with supporting other systems or activities. Software for infrastructures is likely to be distributed and concerned in particular with supporting communication of data, people and/or materials. Hence issues of openness, timeliness, security, lack of corruption and resilience are often important.

2.2.2 Motivation

UNU/IIST pursues advanced development projects in order to fulfil its Charter:

1. to train Fellows from the public and private sectors: universities, research institutes, business and industry

2. to contribute to research -- by trying also to understand the nature of infrastructures

3. to propagate Design Calculi-oriented (i.e. Formal) Methods for software development to universities, business and industry

4. to help develop advanced, initially public domain software in close cooperation with industry and business

5. to help bring software producing and/or relying industries, businesses and other institutions of developing countries at least on a par with those of industrialised countries

6. to disseminate results, including abilities and software, to other developing countries

A more detailed discussion on the motivation of UNU/IIST advanced projects is given in the Annual Report for 1996.

2.2.3 Project selection

2.2.4 Project structure

Partner identification

UNU/IIST finds one or more partners -- universities, research institutes or companies -- from one or more developing countries. This often happens through advanced courses.

Initial

Fellows from partners come to UNU/IIST, typically for 9-12 months, to do the initial domain analysis and requirements capture. This results in both natural language (English) documents and formal specifications.

Prototype

Perhaps as part of the initial phase, perhaps as part of a new one with new Fellows, a prototype may be created. This serves to train in the final stages of software development and also allows the project to obtain feedback from potential users.

Product

The focus of the project moves away from UNU/IIST to the developing countries involved and produces a product. UNU/IIST adopts a consultancy role.

2.2.5 Funding

Since the results of the initial and prototype stages are wholly or partly funded by UNU/IIST, they are therefore in the public domain.

2.2.6 Technical approach

There are two aspects of the technical approach that are critical.

1. Formality

   Formal techniques have two particular characteristics that allow one to deal successfully with large and complex systems.

   1. Abstraction

      At a particular stage in development one can abstract away from some details while concentrating on others.

   2. Rigour

      Formal systems allow one to prove properties of systems, anything from full correctness to particular properties (such as safety properties). Full proof of correctness is beyond the state of the art at present; rigour allows one to use (and document) informal arguments which can be backed up formally if required. The amount of rigour will vary between projects and between parts of a single project; rigour gives flexibility.

2. Domain analysis

   Domain analysis is the exploration and formal description of the domain in which the system will operate. For example, the RaCoSy project, concerned with train rescheduling for the Chinese Railways, starts out by asking, and formally answering, the questions "What is a railway?" and "What is a timetable?". These lead to other questions: "What is a station?", "What is a (railway) network?". Answering such questions, plus others about how these concepts relate, gives a formal model of the domain. Only when such a model is elaborated can the requirements capture of the actual system being developed take place.

   Domain analysis is often wider than the immediate system to be developed. For example, the same domain analysis of railways was used by another Fellow working on station management. Broad domain analysis helps the development of related systems in the same domain; one might say that the result of domain analysis provides an "infrastructure" for software package development.

The particular formal method used in the advanced development projects is RAISE. It is the most broadly applicable of the formal methods available, and also mature, with good documentation and tools. With the help of CRI, the tool providers, UNU/IIST also makes sure that its partners receive the tools (free of charge for research and education) for their continued work.

2.2.7 Current advanced development projects

Date of commencement:

January 1996

Date of completion:

July 1997 (Phase 2)

Staff responsible:

Chris George

Abstract

The MoFIT (Ministry of Finance Information Technology) project is being undertaken with the Vietnamese Ministry of Finance (MoF). The MoF is undertaking, with World Bank support, the development and installation of a Financial Information System. Key functions include synthesis of state budget plans, management of fund allocations, formulation and review of tax policies, and exchange of data between various levels and ministries.

This project is studying appropriate infrastructures to support the accurate, timely and secure collection and analysis of data.

Outputs

Five Fellows, four from the Ministry of Finance and one from the Institute of Information Technology in Hanoi, spent 6 months at UNU/IIST from March to September 1996. Two of these Fellows were funded through the Ministry of Finance by GTZ, a German development agency. In this first phase, work concentrated on specifying the taxation system. As well as a domain analysis of this system [19], it investigated tax system security [20] and taxation policy [21]. It also produced a simple prototype of the accounting part of the system and this was used for testing [22] and investigating optimisation [23]. This work was summarised in a UNU/IIST research report [24].

Two of these Fellows spent a further 6 months at UNU/IIST from October 1996 to April 1997, and were joined by a Fellow from Hanoi University from January to July 1997. In this second phase work was extended to the Treasury [25] and Budget systems [26], plus those for external aid and external debt [27][26]. This led to work on how to transform separate and independent specifications of hierarchical systems into loosely coupled, "flat" distributed systems with communication between them [28]. The phase 2 work was summarised in a UNU/IIST research report [29].

Fellows

  
Do Tien Dung, Ministry of Finance, 11 April 1996 - 27 September 1996, 14 October 1996 - 13 April 1997
Phung Phuong Nam, Ministry of Finance, 11 April 1996 - 27 September 1996, 14 October 1996 - 13 April 1997
Hoang Xuan Huan, Hanoi University, 15 January 1997 - 14 July 1997

Partner

  
Ministry of Finance, Hanoi, Vietnam
Institute of Information Technology, Hanoi, Vietnam
Hanoi University, Hanoi, Vietnam

Status:

The work has been much appreciated by the Vietnamese Ministry of Finance and it is hoped to continue collaboration with them on a consultancy basis. In May 1997 they wrote:

As far as the Ministry of Finance modernisation is concerned, we are
now seeking for an eligible consulting company to prepare the project
documentation.  After the project approval, we will call for the
project bid.  If it interests you, your cooperation in monitoring and
evaluating preparation and implementation processes will be highly
appreciated.

MoFIT has also led to the EDMaCS InfoDev proposal with Belarus.

PortMan - Port Management

Date of commencement

September 1997

Date of completion

May 1998 (phase 1)

Staff responsible

Chris George

Abstract

Port management has the aim of improving the efficiency of handling cargo and ships and thereby increasing productivity and reducing costs.

There are two main areas:

Vessel traffic management

including tracking of ships by radar and GPS systems, providing displays, supporting safe routing, berth allocation, etc.

Management information

including subsystems to deal with cargo, containers, financial services, material management, etc.

Integrating these systems requires a substantial domain analysis of the data involved and the operations to be performed on it. In phase 1 we will more precisely define the problem and carry out the domain analysis.

Outputs

To be identified.

Fellows

 
D.H.S. Sarma, ECIL, 1 September 1997 - 31 May 1998
N. Sathya Prakash, ECIL, 1 September 1997 - 31 May 1998

Both Fellowships are partly supported by ECIL.

Partner

Electronics Corporation of India Ltd. (ECIL)

Status

This project is just beginning.

MIICI - Manufacturing Industry Information and Command System

Date of commencement

September 1995 (Phase 2)

Date of completion

Fellows are so far invited until August 1998.

Staff responsible

Tomasz Janowski

Abstract

With growing pressure to sustain global competition, to deliver products of higher quality, at lower cost and with shorter time-to-market, perhaps even to fulfil individual customer requirements, many companies are forced to reconsider the ways they run their business. Companies are also forced to work more tightly together, perhaps sharing or outsourcing some of their business processes within an extended (virtual) enterprise. Answering such global trends clearly requires dedicated, empowered people provided with up-to-date information and modern Information Technology tools to support their decisions. The main concern of this project is to develop a sound basis which allows one to express requirements, carry out design in accordance with such requirements, and finally integrate such tools.

Outputs

Recent work has produced an informal domain analysis for manufacturing [30], a formal model of enterprises competing on the single-product market [31] as well as cooperating within the structures of a virtual enterprise [32]. The second, in particular, produced a unique formal model which combined previously separate models for marketing (four Ps: product, price, place and promotion) and its effect on the sales of an enterprise, and enterprise resources (four Ms: man, machines, materials and money). There is also on-going work on concurrent engineering, to exploit concurrency within the structures of a virtual enterprise; a report will appear.

Fellows

  
Ou Song, South China University of Technology, 1 December 1996 - 25 June 1997
Gustavo Lugo, CEFET, Parana, Brazil, 1 September 1997 - 31 May 1998
Zheng Hongjun, Peking University, 3 November 1997 - 31 August 1998

Partners

  
Peking University, Beijing, China
South China University of Technology, GuangZhou, China
De La Salle University, Manila, Philippines
Federal Centre of Technological Education (CEFET) of Parana State, Brazil

Status

The project is expected to continue, aiming to build a new language (then an automated environment) for modelling, analysis and design of manufacturing enterprises. This will properly build on the work done so far, applying existing RSL models to give a formal semantics to this language.

MultiScript

Date of commencement

September 1995

Date of completion

end 1998

Staff responsible

Richard Moore

Abstract

A wide range of information systems require support for pieces of text in different languages. The most obvious example is perhaps a library, though many other institutions, including universities, government departments (particularly in countries where many different languages are used, for example India), commercial industry, hospitals and tourist information services, often need to store or make available information in more than one language. This is particularly true in developing countries where a large amount of the information to be stored is likely to come from other countries.

The project is studying the design of a software system supporting the creation, presentation and browsing of documents in which more than one language is used, for example a dictionary from one language to another. Particular emphasis is being placed on allowing languages with different reading and writing directions to be intermixed in the same document while all still retaining their traditional directionality.

The project is also contributing, under the International Organisation for Standardisation's working group ISO/IEC JTC1 SC2 Working Group 2, to the definition of an international standard encoding system for traditional Mongolian script which will form part of the ISO/Unicode international standard, a coding system which covers the majority of the world's languages.

Outputs

The first phase of the project performed a comprehensive study of a wide range of existing multi-lingual documents, on the basis of which a formal model of generic multi-directional multi-lingual documents was defined. In addition, outline requirements for a software system supporting the creation and browsing of multi-lingual documents were also formulated.

Documents describing this domain analysis and outline requirements capture were written, and these are summarised in a UNU/IIST Technical Report [33]. This paper was presented at the 1997 International Conference on the Computer Processing of Oriental Languages (ICCPOL'97), Hong Kong, in April 1997 [34].

In the second phase of the project, the formal model was extended and slightly modified to incorporate specifications of functions for creating, editing and displaying (printing) multi-directional multi-lingual documents. Three UNU/IIST Technical Reports detail the results of this phase of the project. The first [35] describes the (modified) basic model of multi-directional, multi-lingual documents; the second [36] describes the display and printing of such documents; and the third [37] describes the creation and editing of such documents. These reports will be used as the foundation for the design and implementation of a prototype software system in the next phase of the project.

As part of its ongoing work with the International Organisation for Standardisation's working group ISO/IEC JTC1 SC2 WG2 on the standardisation of the coding for traditional Mongolian script, a paper [38] was submitted to the international meeting of ISO/IEC JTC1 SC2 WG2 in Singapore in January 1997 pointing out a serious error in the coding scheme which was currently under consideration by the group, on the basis of which a revised draft proposal was produced jointly (UNU/IIST, Mongolia, China) by delegates at the meeting and submitted formally to WG2.

This work has also led to the creation of a font covering the characters of the traditional Mongolian script.

Fellows

 
Yumbayar Namsrai, NUM, 1 October 1996 - 30 June 1997
Myatav Erdenechimeg, previously a Fellow from NUM (September 1995 - August 1996), returned to Macau in September 1996, since when she has continued to work on the project on a voluntary basis as an Honorary Fellow of UNU/IIST.

Partner

National University of Mongolia, Ulaanbaatar

Status

Further Fellows are being sought to continue work on the project, beginning in January or February 1998, and two potential candidates have been interviewed. This next phase will use the work done so far as the basis for the construction of a prototype software system supporting the creation, editing, presentation and browsing of multi-directional, multi-lingual documents.

Telephony

Date of commencement

September 1996 (phase 2)

Date of completion

May 1997 (phase 2)

Staff responsible

Richard Moore

Abstract

This phase of the project studied routing in a general, distributed, multi-media communications network, in particular the processes of connection and disconnection of routes.

Outputs

An abstract formal specification of a multi-media network as a hierarchy of local networks has been produced, on the basis of which specifications of route finding and the procedures for connecting and disconnecting routes have been formalised. These connection and disconnection procedures have been defined in such a way that each local network in the hierarchy performs as much of the task as it can using only its own local resources, then passes the task to the "next" network in the hierarchy for completion and so on recursively until the connection or disconnection is complete. The network as a whole is thus represented as a distributed system of local networks, each with its own control.

The work forms the subject of a UNU/IIST Technical Report [39].

Fellows

  
Hoang Thi Tung Lam, PTTC Vietnam, 1 September 1996 - 31 May 1997

Partner

  
Posts & Telecommunications Training Centre 1, Hatay, Vietnam

Status

Work on this phase of the project has finished.

MiTras - Metropolitan Transport Systems

Date of commencement

September 1996

Date of completion

June 1997

Staff responsible

Tomasz Janowski

Abstract

With increasing congestion in large and super-large cities the market for software solutions to the problems facing metropolitan passenger transport grows. There is now a catalogue of products to choose from, even a technology to put them together, as no single solution is likely to work here. But true integration requires products to have the same understanding of the basic concepts in the domain, not only formats of data, and often goes beyond customising off-the-shelf packages. In this project, the intention is to show how formal methods can help produce such integrated solutions in the domain of metropolitan transport.

Fellows

  
Gueorgui Satchok, 1 September 1996 - 30 June 1997

Partner

  
Belarussian State University of Informatics and Radio-electronics.

Outputs

The project has produced an ontology of the basic concepts in the transportation domain: street network, transport vehicles, traffic, traffic regulations, transport stops, transport routes, timetables, etc. The concepts have been described formally, helping to capture requirements for software solving a number of problems in this domain, under the common goal of maintaining (as much as possible) passenger timetables despite some unpredictable events in the streets: positioning of vehicles, detection of timetable violations, finding detours for congested street sections, etc. The emphasis always is on models that can integrate software used for different kinds of transport (buses, trains, trams etc.) through using a single, consistent underlying model. All this work is described in a report [40] which, revised, will be submitted to a conference.

Status

The work on this phase of the project has finished. The partner has approached UNU/IIST about the continuation of the second phase of this project.

Traditional Medicine

Date of commencement

January 1997

Date of completion

August 1997

Staff responsible

Richard Moore

Abstract

In many developing countries in Africa, the facilities for modern health care are not only insufficient, being concentrated mainly in the larger cities, but also expensive. This puts them beyond the reach of many people, particularly those in rural communities, both geographically and financially. As a result, many people are turning back to traditional medicine as the only viable source of medical treatment.

In general, however, traditional African culture is oral, and the traditional doctors, many of whom are illiterate, transmit their knowledge verbally from father to son and from mother to daughter. Knowledge is therefore easily lost, either if a family has no descendants or if the children forsake the traditional ways in favour of a more Western style culture.

The project seeks to redress this trend by providing a basis for the storing of information on medicinal plants and traditional medicine, and by collecting and storing information from the practitioners to ensure that the knowledge is preserved and promoted.

Outputs

A high-level, informed domain analysis of African traditional medicine, and a proposal for continuing the project into a second phase.

Fellows

  
Laure Pauline Fotso, University of Yaoundé I, 22 January 1997 - 15 August 1997

Partner

  
University of Yaoundé I, Cameroon

Status

Work on this phase of the project has finished. The proposal for the second phase is being submitted to potential donors and partners.

ABC'2000 - Airline Business Computing

Date of commencement

September 1997 (phase 2)

Date of completion

March 1998 (phase 2)

Staff responsible

Richard Moore

Abstract

In the first phase of the project (September 1995 to September 1996) a thorough analysis of the domain of airline business was carried out. Following on from this, five members of staff from the information technology division of Vietnam Airlines visited UNU/IIST in July 1997 to discuss possible ways in which the project might develop the earlier work. As a result of these discussions, it was agreed that the second phase of the project would concentrate on one important aspect of airline business, namely flight effectiveness analysis which allows an airline to assess a flight on the basis of the revenue it brings in through passenger and cargo transport and its cost.

Two Fellows are working on the specification and design of a software system for flight effectiveness analysis for an initial period of 6 months. One Fellow is entirely supported by Vietnam Airlines.

The work of this phase will be assessed jointly by UNU/IIST and by Vietnam Airlines towards the end of the initial 6 month period, and if favourable a further extension may be arranged.

Outputs

A document giving both an informed and a formal description of flight effectiveness analysis is in preparation.

Fellows

 
Tran Manh Thang, Vietnam Airlines, 5 September 1997 - 4 March 1998
Nguyen Hong Viet, Vietnam Airlines, 5 September 1997 - 4 March 1998

Partner

  
Vietnam Airlines

Status

Work on this phase of the project is ongoing. Discussions with Vietnam Airlines about continuing the project will be initiated in early 1998.

Casino - Categories for System Integration

Date of commencement

July 1996

Date of completion

Fellows invited till December 1997.

Staff responsible

Tomasz Janowski

Abstract

This is really a research project, but arises directly from the software for infrastructure theme in the need for integrating or "interoperating" different software packages. It also aims at the integration of formal and informal methods in software engineering:

• Formal methods allow software to be designed with proofs of correctness, in principle free of design mistakes. An example is RAISE - Rigorous Approach to Industrial Software Engineering.

• Informal methods allow software to be engineered from libraries of existing components, with no guarantee or even formal specification of what it means for them to be correct. An example is CORBA - Common Object Request Broker Architecture.

The project works towards integrating such techniques and enabling plug-and-play provably correct software. The basic idea is to extend interface descriptions for library components (informal part) by axioms which state their expected behaviour. They can be verified against such axioms. They can also be validated on-line, becoming separated from the environment by the special monitoring software. This software continues checking that all interactions follow the axioms and raise an exception otherwise. This idea is followed for RAISE and CORBA in particular, with RAISE becoming a formal extension of the CORBA IDL (Interface Definition Language).

Outputs

Two reports have been produced so far. The first is a contribution to formalise, in a systematic way, some of the issues related to CORBA, as a means to overcome problems caused by the heterogeneity of the interacting components (so-called specification- and implementation-barriers) [41]. The second outlines some initial ideas about an integrated CORBA/RAISE environment for building software from pre-existing components [42]. Given that CORBA IDL (Interface Description Language) describes only the signatures of operations that the component offers for its environment, the paper exploits the possibility that semantics is captured within IDL extended with RSL (Raise Specification Language). It also offers a mapping between the IDL type hierarchy and RSL, and investigates how modal logic (itself not supported by RSL) could provide a useful level of description for decisions about reuse, etc.

Fellows

   
Vladimir Zadorozhny, Institute of Systems Programming, Russia, 12 January - 31 August 1997
Yun Xiaochun, Harbin Institute of Technology, China, 5 May 1997 - 25 January 1998

Partners

  
University of Gdansk, Poland
Harbin Institute of Technology, China
Institute of System Programming, Russian Academy of Sciences

Status

Expected to continue. Conference submissions are in preparation.

2.2.8 Future projects

Annual Report 1997