Annual Report 1999

Contents

2 Status of Implementation of Projects

1. Computing Science Research

2. Advanced Software Technology Development

3. Curriculum Development

4. University Development

5. Fellow Training

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

7. Events

8. 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 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 Agenda

DeTfoRS - Design Techniques for Real-time Systems

Since the establishment of UNU/IIST, the research group has centred its effort on theories, techniques and tools based design of real-time systems. UNU/IIST is one of the main research centres in developing and applying Duration Calculus (DC) in support of the design of real-time hybrid systems and has become an acknowledged leader in this field.
Real-time systems are ones in which timeliness is essential to correctness. They encompass all devices with performance constraints. Hard deadlines are performance requirements that absolutely must be met. A missed deadline constitutes an erroneous computation failure. Most real-time systems also interact directly with electric devices and indirectly with mechanical ones. One of the problem that arises with environmental interaction is that external events are frequently not predictable. Systems must react to events when they occur rather than when it might be convenient. The software for real-time hybrid systems is therefore more difficult to construct because it must concern itself with timeliness, robustness and safety.
The research group will continue to focus on DC-based design methods in the concerned period, and at the same time will widen its technical scope by paying more attention to other application-oriented research.

2.1.2 Current Projects

Specification, design and verification of safety-critical real-time, reactive and hybrid systems

1. Integrate RAISE with DC:
   We provide a DC semantics for Timed RAISE equipped with delay and time-out constructs. A simple alarm system is used to demonstrate how the proof rules are applied in design and verification of hybrid systems ([49],[48]).

2. Design theory for real-time systems:

   • The class of DC formulae closed to regular real-time programs
     A complete proof system and decidability results for the class have been given ([31]).

   • A method for designing real-time control systems in Duration Calculus

     We formalise the design process of the real-time control system in Duration Calculus by taking into account the discretization of time caused by the interaction of different components with different clocks. We give DC formulas to express the relationships between the states of different components and rules for deriving a specification of components from a specification of the global systems. We also study the rules for the refinements of a DC specification into simple DC formulas.

   • Temporal logic over infinite intervals

     The classic interval temporal logic is defined over finite intervals and subsequently cannot express liveness or describe infinite computations directly. We have investigated two proof systems for infinite intervals and have shown that they are complete ([27]).

3. Tools in support of the verification of real-time systems:

   • Algorithmic verification for linear duration properties of probabilistic real-time systems.
     We have developed a polynomial time-algorithm for the verification, which is a significant improvement from the previous one ([40]).

   • The proof assistant for interval logics based on PVS has been improved. A Gentzen like system supporting systematical proofs is implemented, as well as a set of strategies for efficient verification. The fellow who worked on this project has been awarded a PhD in his home university in China and published two papers in journals in China based on his work at UNU/IIST.

   • Verification method for real time programs has been investigated. The programs involve concurrency and shared variables. A set of proof rules are being studied.

4. Case studies:

   • Formalisation of the concurrent control in real-time database systems in DC.
     We have formalised the correctness criteria for the concurrent control protocols in real-time database systems and have given a formal proof for the correctness of the two-phase locking protocol ([55]).

   • We formally study Liu and Layland's classic theorem on the Rate Monotonic Scheduler. By using the proof system of Duration Calculus, we formally prove that the feasibility condition due to Liu and Layland is sufficient ([56]).

   • Formal specification of protocols used in multi-media (joint research with Beijing University of Posts and Telecommunications).

   • Specification and implementation of a motor control system.
     A list of informal requirements has been formalised in the notation of DC. The design process produces a set of Harel's Statecharts with time constraints for analysis and reasoning of the properties of the control programs, and delivers a Timed RAISE as the software implementation.

   • Specification and design of a satellite controller.
     We have formalised a collection (around 100) of safety and time requirements (from the Euro Standard about the satellite controller), and proposed a software architecture based on communication-based paradigms. Both the sequence diagram and collaboration diagram of UML are used to describe the behaviour of individual components and their interactions. We also design a RSL program to deal with the shared objects of the system.

An integrated approach for compositional specification, design and analysis of mixed hardware/software systems

1. Formalisation of VERILOG
   Hardware Description Languages (HDLs) are an increasingly popular way to develop hardware in industry as tools and standards become established. Two of the major HDLs in use are VHDL and VERILOG. The formal semantics of VHDL has been studied quite extensively, but that of VEROLOG less so. We take advantage of the algebraic approach in investigation of simulator algorithms, and formalise an event semantics for a subset of VERILOG in the form of relations and use Relation Calculus to prove properties of combinational circuits. We also produce an operational semantics for a substantial subset of VERILOG, and implement it in Prolog. ([17],[8]). We are also working on a DC-based denotational semantics of VERILOG by applying some advanced features of DC ([47], [44]).

2. Specification language for mixed hardware/software systems:
   We enrich DC with a parallel operator to integrate systems evolved at various time rates. The framework provides a unifying means for presenting the features of event-based hardware description languages and state-based imperative languages ([42]).

3. A common framework for co-design:
   A computational model is introduced to describe the behaviour of digital devices, the hardware description language VERILOG and the temporal programming language TEMPURA, which serves as the semantic domain for co-design ([41]).

4. Integrating variants of DC:
   In order to support DC-based programming, we add some features into DC to deal with local variables and super-dense computations ([10],[43]). The new logic framework unifies Neighbourhood Logic, Higher-order Duration Calculus, DC with super-dense chop, DC with iteration, and Recursive Duration Calculus. It has also been successfully used in formalising Timed RAISE.

Formal description of various entities that appear in object-oriented and component-based development

Staff responsible

  
He Jifeng
Dang Van Hung
Xu Qiwen

Fellows

  

Zhan Naijun: 1 September 1998 -- 31 August 1999, China
Ekaterina Pavlova: 1 September 1998 -- 28 February 1999, Russia
Hou Jianmin: 1 September 1998 -- 28 February 1999, China
Tran Van Dung: 1 September 1998 -- 11 April 1999, Vietnam
Li Li: 1 September 1998 -- 31 July 1999, China
Rusdi Md Aminuddin: 1 September 1998 -- 28 February 1999, Malaysia
Ma Huadong: 9 Nov 1998 -- 8 Feb 1999, 10 Aug 1999 -- 4 Sep 1999, China
Zhu Huibiao: 1 March 1999 -- 31 December 1999, China
Ngo Hoang Huy: 15 April 1999 -- 14 January 2000, Vietnam
Francois Siewe: 1 May 1999 -- 27 December 1999, Cameroon
Li Guoming: 17 May 1999 -- 22 December 1999, China
Zhang Zhongping: 17 May 1999 -- 22 December 1999, China
Mao Xiaoguang: 2 June 1999 -- 31 August 1999, China
Wang Jianzhong: 1 September 1999 -- 28 February 2000, China
Wasim Khan: 1 September 1999 -- 14 February 2000, India
Qin Shengchao: 1 September 1999 -- 31 July 2000, China
Dangaasuren Garmaa: 1 September 1999 -- 28 February 2000, Mongolia
Do Van Nhon: 1 September 1999 -- 31 May 2000, Vietnam

Visitor

   
Jonathan Bowen: 17 July 1999 -- 9 September 1999, UK

Partner Institutions

   
University of St. Petersburg, Russian Federation
Nanjing University, China
Institute of Communication and Transport, Hanoi, Vietnam
University of Science and Technology, Hefei, China
Northern University of Malaysia, Malaysia
Beijing University of Posts and Telecommunications, China
East China Normal University, Shanghai, China
Institute of Information Technology, Hanoi, Vietnam
University of Dschang, Cameroon
Beijing Institute of Information and Control, China
Changsha Institute of Technology, Hunan, China
Shri G.S. Institute of Technology & Science, Indore, India
Beijing University, China
National University of Mongolia, Mongolia
Vietnam National University, Ho Chih Ming City, Vietnam

Outputs

  

The achievements in 1999 can be summarised as follows:

1. Integrate RAISE with DC: A DC semantics for Timed RAISE equipped with delay and time-out constructs has been given. ([49],[48]).

2. A complete proof system and decidability results for the class of DC formulae closed to regular real-time programs have been given ([31]).

3. A method for designing real-time control systems in Duration Calculus taking into account the discretization of time caused by the interaction of different components with different clocks.

4. Polynomial time-algorithms for verifying linear duration properties of probabilistic real-time systems ([40]).

5. A formalisation of the concurrent control in real-time database systems in DC ([55]).

6. A formal specification of protocols used in multi-media (joint research with Beijing University of Posts and Telecommunications).

7. Formalisation of event semantics for a subset of VERILOG in the form of relations, an operational semantics for a substantial subset of VERILOG, and an implementation in Prolog ([17],[8]), and a DC-based denotational semantics of VERILOG ([47],[44]).

8. A specification language for mixed hardware/software systems that provides a unifying means for presenting the features of event-based hardware description languages and state-based imperative languages ([42]).

9. A common framework for co-design ([41]).

10. Integrating variants of DC that can deal with local variables and super-dense computations ([10], [43]).

2.1.3 Future Project

Component Based Software Development
(a joint project with Oxford University and Leicester University of UK)
Abstract Computer-based software development captures the essence of best practice in the construction of complex systems. In order to reduce system development to the construction and re-use of high quality components, we require notations and techniques for the description and analysis of component behaviour which give us a precise understanding of component roles and properties.
Technical Approach
The proposed research will be built upon the Unified Modelling Language (UML), a standard notation being developed by the Object Management Group, a consortium of over 700 companies and organisations, including both IBM and Microsoft. The intention is to enhance the semantic basis of object-oriented development, and provides a process-oriented semantics to UML, and a rigorous treatment of refinement and a description and use of components.
The research will focus on the following topics:

1. Identifying a collection of standard description techniques in terms of generic and specific models (for example, pre-post condition for individual method, invariant for consistency of abstract date type, interface protocol for module, state diagram for the behaviour of object, interaction diagram for synchronisation of parallel threads).

2. Providing a process semantics for various diagrams and their relationships used in UML.

3. Constructing a mathematical theory of refinement and simulation underpinning these description techniques.

2.2 The Advanced Development Agenda

2.2.1 Agenda

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.

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 development projects is given in the Annual Report for 1996.

Project Structure

Application

projects are usually with a specific partner with a specific development goal. An application is identified and the first goal is always to do an initial domain analysis and requirements capture. This involves fellows from the partner institution coming to UNU/IIST for 6-12 months. They are trained in the appropriate techniques and produce a technical report involving both natural language (English) narrative and formal specifications.

The first phase is sometimes followed by another, typically involving more fellows from the partner institution, again for 6-12 months. The goal may be to extend the scope of the original work into a new area, or to work in more detail on a component of the original work, or to develop a prototype implementation.

The aim is that the work at UNU/IIST is followed by actual implementation by the partner, with UNU/IIST adopting a consultancy role. We also hope to be able to attract new partners into the projects. This has not generally proved very successful. The software industry in developing countries tends to adopt a very flexible and hence rather short-term approach. Projects tend to be brief and labour in short supply, so that training is rather neglected. This is one of the reasons for UNU/IIST shifting its focus to also include the thematic projects.

Thematic

projects are less focussed on products. They have more of a research component, but they are applied research, concerned with the application of formal methods to new areas. They are more open-ended than the application projects, allowing them to reflect the particular interests of the fellows who come to work on them.

Currently there are three such projects, concerned with enterprise modelling (MIICI), with building software from existing components (Casino), and with object-oriented design patterns.

RAISE

projects have arisen from the need to support and develop the formal method that UNU/IIST uses for its advanced development and curriculum development projects. The original RAISE tools are powerful and comprehensive, are freely available for education and research, but only run on Sun workstations. The RAISE tools project is developing a new set of tools for RAISE that will run on any platform.

The Timed RAISE project is concerned with extending RAISE with support for the specification and development of real-time software. It is a collaboration between the advanced development and research groups of UNU/IIST and is described in section 2.2.2.

Both these RAISE projects are open-ended and involve fellows coming to work on particular components or aspects.

Funding

Thematic and RAISE projects are funded by UNU/IIST.

The results of all activities wholly or partly funded by UNU/IIST are in the public domain, i.e. freely available to others.

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 TERMA, 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. And, of course, we also give them the new tools for RAISE.

2.2.2 Current Projects

Application Projects

MultiScript

Date of commencement

September 1995

Date of completion

mid 2000

Staff responsible

Richard Moore

Abstract

The MultiScript project is designing and implementing a software system for creating and processing multi-lingual documents, that is documents in which the text may be composed of several different languages and scripts mixed together. Examples of such documents include dictionaries which give translations from one language to another, language teaching material, international business contracts, and official documents in countries and territories which have several different languages (e.g. Hong Kong, Macau, India) or two different ways of writing the same language (e.g. Mongolia where both the traditional Mongolian script and the Cyrillic script are used).

A wide range of information systems require computer support for such documents. The most obvious example is perhaps a library, though many other institutions, including universities, government departments (particularly in countries where several different languages are used), 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 places particular emphasis on allowing languages and scripts with different reading and writing directions to be intermixed in the same document while all still retaining their traditional directionality. This is in direct contrast to much of the existing software support for multi-lingual documents which tends to be uni-directional, often imposing the standard left-to-right horizontal directionality of the Latin script on all text.

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 [18]. This paper was presented at the 1997 International Conference on the Computer Processing of Oriental Languages (ICCPOL'97), Hong Kong, in April 1997 [19].

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 [21] describes the (modified) basic model of multi-directional, multi-lingual documents; the second [53] describes the display and printing of such documents; and the third [20] describes the creation and editing of such documents. Some of the results from the second phase were presented at the Workshop on the Principles of Digital Document Processing, part of the 1998 Conference on Electronic Publishing (EP'98), which was held in St. Mâlo, France, in March/April 1998 [22].

The reports from the second phase are being used as the foundation for the design and implementation of a prototype software system in the third phase of the project. This is being built using the Delphi system on top of Windows NT so as to enable a tie-in with the project's work on the international standard encoding scheme described below. Much of the underlying functionality of the system has already been completed, though work on the top-level interface for displaying and printing documents is still in progress.

This implementation work is covered in a UNU/IIST Technical Report [2], and part of it also forms the subject of an M.Sc. thesis by the fellow involved.

A report on the MultiScript project as a whole has been accepted for presentation at the forthcoming 16th International Unicode Conference to be held in Amsterdam in March.

As part of its ongoing work with the International Organisation for Standardisation's working group ISO/IEC JTC1 SC2 WG2, of which UNU/IIST is an official member (category C), a proposal for the standardisation of the coding for traditional Mongolian script was jointly prepared (UNU/IIST, Mongolia, and China) and was presented at a meeting of WG2 in London at the end of September 1998. This proposal is now passing through the third and final stage of the international review process and is expected to be officially adopted as the international standard encoding for traditional Mongolian script in early 2000. A UNU/IIST Technical Report [23] describes the encoding and gives information on implementing software systems which conform to it, and a paper on this work has also been accepted for presentation at the 16th International Unicode Conference to be held in Amsterdam in March.

Fellows

 

Avirmed Amar, National University of Mongolia, 2 May 1998 - 25 March 1999
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 a Visiting Scientist at UNU/IIST.

Partner

National University of Mongolia (NUM), Ulaanbaatar

Status

Ms. Myatav Erdenechimeg will complete the development of the prototype MultiScript system.

ABC - Airline Business Computing

Date of commencement

September 1995

Date of completion

February 1999

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

In the second phase of the project (September 1997 to March 1998), two Fellows from Vietnam Airlines developed a specification [61] of the first of the two parts of the flight effectiveness analysis system, namely which data on cost and revenue are needed in flight effectiveness analysis and how they are analysed to generate IATA standard reports on flight effectiveness. One of the Fellows was entirely supported by Vietnam Airlines.

After they returned to Vietnam, the two Fellows from the second phase and the Fellow from the first phase worked with a group of potential new Fellows on planning and preparation for the third phase of the project. One new Fellow from the group came to UNU/IIST in September 1998 and developed specifications of two specialised aspects of airline business computing: future demand forecasting, which is a technique an airline company uses as part of its business planning process to estimate future market demand; and a frequent flyer program, which is a bonus scheme operated by an airline to try to ensure that existing customers develop some loyalty to the company, thereby ensuring future sales. These specifications [13] were then used as the basis for building demonstrator software systems.

Outputs

One UNU/IIST technical report [13] was produced at the end of the third phase of the project. This gave both an informal and a formal description of both future demand forecasting and frequent flyer programs. Prototype software systems for each of these aspects of airline business computing were also developed.

Fellows

 
Than Quoc Dang, Vietnam Airlines, 1 September 1998 - 28 February 1999

Partner

  
Vietnam Airlines

Status

No new fellows are planned so far for 2000.

Engineering Design Database

Date of commencement

September 1999

Date of completion

not yet known

Staff responsible

Chris George

Abstract

A team at the CAD centre of Southwest Jiaotong University, Sichuan, China is developing an engineering design database to support architectural design of buildings. The system will have three main components:

• A CAD front end for viewing and editing designs

• A database of relevant engineering information

• Intelligent design support linking the database to the CAD component.

Intelligent design support will involve activities like finding suitable design cases to use for the current problem, and checking design rules.

The aim of the project at UNU/IIST is initially to formalise the basic design of the system. This may be followed later by more detailed work on particular parts.

Outputs

There are as yet no outputs from the project, but some preparatory work was done by He Bin, a lecturer at the CAD centre, who came to UNU/IIST as a curriculum development fellow [5].

Partner

 
CAD Centre, Southwest Jiaotong University, Chengdu, Sichuan, China

Status

Continuing.

Thematic Projects

MIICI - Enterprise Modelling, Analysis and Implementation

Date of commencement

September 1997 (Phase 3)

Date of completion

Ongoing

Staff responsible

Tomasz Janowski

Abstract

The project is about the application of formal methods to enterprise engineering, for business organisations in general and manufacturing organisations in particular. We study formally-based notations, methods and tools to analyse, design and re-design an enterprise as an engineering artifact. We emphasise the need for building representations of enterprises at different levels of abstraction and the need for formal underpinning for such representations to allow comparing them. The issues range from building enterprise models, relating models at different levels of abstraction, analysis of models at a given level, refinement from abstract to concrete models, composition of models to represent virtual organisations, implementation using current information technology etc.

By addressing such issues formally, we aim to provide a technical context to express and support newly emerged concepts like outsourcing and virtual organisations, business process engineering and re-engineering, recycling and product life-cycle, lean and just-in-time production, concepts which are increasingly adopted by manufacturing organisations worldwide to address challenges of global competition and unstable market conditions.

Outputs

Before the current period the project produced three technical reports. The report [32] about the integration of enterprise models and models for marketing analysis was presented at, and published in the proceedings of the 2nd IFIP Conference on Design of Information Infrastructure Systems for Manufacturing, Denver, USA, May 1998. The report [35] about the modelling of an extended/virtual enterprise by the composition of enterprise models was presented at, and published in the proceedings of the 3rd IEEE/IFIP International Conference Information Technology For Balanced Automation Systems in Manufacturing, Prague, Czech Republic, August 1998. The report [33] about operational semantics for the models of manufacturing enterprises was presented at, and published in the proceedings of the 2nd IEEE International Conference on Formal Engineering Methods, Brisbane, Australia, December 1998.

The project continued in this period with four fellows, Huang Biqing and Liu Yonghe from China and Francisco Moreira and Rui Sousa from Portugal. Two Portuguese fellows were fully supported by the grants from the Calouste Gulbenkian Foundation, Portugal. The outputs from this period are as follows:

1. A revised and extended version of the Research Report 131 [35] will appear in the Special Issue of the Journal of Intelligent and Robotic Systems, Kluwer, on Intelligent Manufacturing Systems.

2. With two fellows from China we focused on the problem of partner selection for a virtual organisation. Partner selection requires to identify individual member enterprises as well as prescribe the roles they should play in the organisation. Most of the work in this area assumes that such enterprises can be identified based on their static area of `competence'. We decided instead to base partner selection on how an enterprise is able to dynamically deliver services to its clients, within the area of its competence. The output is a model which explains the behaviour of a virtual organisation in terms of the services it can offer to and receive from its environment, by means of the services by its members and service-based interactions between them. The model has been instantiated for different service domains (product delivery, logistics, marketing) and applied to provide a formal definition to the problem of partner selection, in order to seek an automated solution to it. The results are described in the Research Report 165 which was presented at, and published in the proceedings of the IFIP/PRODNET Working Conference on Infrastructures for Industrial Virtual Enterprises, October 1999, Porto, Portugal [6].

3. With two fellows from Portugal we sought a method to build models of production organisations to allow to animate/simulate their behaviour in addition to reasoning. We demonstrated how it is possible to build and execute such models using some of the Unix system tools: awk for text processing, bash for process management and mail for information exchange. Technically, we used plain text files to represent the state of the production cell, implemented production operations as text-transformations, composed such operations into one or several processes for their sequential or concurrent execution and allowed remote processes (located in different cells) to communicate with each other by automatically sending and processing emails. The models are highly configurable, able to represent assembly lines, flexible manufacturing systems, even virtual organisations. But they are also concrete and implementation-dependent, therefore we also presented their formalisation in RSL. This paradigm of "Production Modelling as Shell Programming" has been described in two Research Reports: [36] concentrates on the sequential case, single cell, and [37] extends the model with concurrency and distribution. Both reports are submitted for publication.

Fellows

  

Huang Biqing, Tsinghua University, China, 16 November 1998 - 15 January 1999
Liu Yonghe, Tsinghua University, China, 16 November 1998 - 1 May 1999
Rui Sousa, University of Minho, Portugal, 1 September 1999 -- 28 November 1999
Francisco Moreira, University of Minho, Portugal, 1 September 1999 -- 28 November 1999

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
National CIMS Centre at Tsinghua University, Beijing, China
University of Minho, Minho, Portugal

Status

Ongoing. Two fellows are invited: Mr. Phan Cong Vinh from the Posts and Telecommunications Institute of Technology, Ho Chi Minh City, Vietnam, to work on the coordination protocols for information exchange in virtual organisations, and Mr. Roger Atsa Etoundi from the University of Yaounde I, Department of Computer Science, Cameroun, to specify and implement the enterprise-wide time-management system.

Methods and Tools for Building Software from Components

Date of commencement

May 1997 (Phase 2)

Date of completion

Ongoing

Staff responsible

Tomasz Janowski

Abstract

Most software today is built from pre-existing components, often given in a form which allows then to be used but not analysed (typically off-the-shelf components distributed as binary files). Software design means composition and correctness of the design relies on the correctness of individual components. This practice saves on time and the cost of development and results in products which are easier to upgrade and maintain. But it also creates a host of basic but technically challenging questions and problems: What in essence is a reusable component? What is the semantics of a component? How can we abstract away from the details of the semantics in order to decide suitability of a component for the design? What is the "best" abstraction level for this? Given two descriptions of one component (a specification and an implementation) how can we make sure they are consistent? How to check consistency if the implementation details are unavailable? To what extent can we adapt a component which fits only partly into our design? And so on.

The goal of the project is to study formally-based methods for software design from pre-existing components, including but not limited to the issues above. In particular, we look for a common ground to use together formal methods (to predict the result of putting components together) and fault-tolerance (to detect and recover from errors of individual components at run-time). Based on the results of such study we want to implement prototype tools to perform specialised tasks like e.g. generating component wrappers to monitor component behaviour at run-time, discovering automatically the presence of redundancy among components, carrying out transformations to exploit this redundancy, etc. We plan to implement such tools rigorously using RAISE.

Outputs

Before the current period the project produced a number of reports. Two reports were written by Vladimir Zadhorozny, both related to CORBA (Common Object Request Broker Architecture), an environment for the composition of distributed objects: [64] about the integrated CORBA/RAISE environment for semantic interoperability and [63] about the orthogonal formalisation of CORBA. The earlier report about real-time and fault-tolerance [34] was revised as part of the project (to be used in the future work) and will appear in the Journal of Real-Time Systems, Kluwer. The report [39] about design for fault-tolerance was presented as the invited paper at the conference on Information Technology in Education and Training, Ho Chi Minh City, Vietnam, January 2000.

The project continued in this period with three fellows: Wojciech Mostowski, Babatunde Akinkunmi and Balkhis Abu Bakar. We follow the general theme of methods and tools for building software from components. In particular:

1. Wojciech investigated the use of regular expressions as formal specifications of software components, suitable for checking their behaviour at run-time. Such expressions are built from the logical properties over the component's observer operations which must hold about the state of the component in different points of its recorded execution history. The expression can become part of an automatically generated wrapper which carries out run-time checking as a kind of pattern-matching. The output of this work is the prototype wrapper-generator for a restricted set of Java classes. The generator takes a Java class and a regular expression as input and produces a `wrapped' Java class (sub-class of the input class) as output, together with an applet which tests the behaviour and compares the performance of the original and the wrapped class. The work has been described in the Research Report 164, which was presented at, and published in the proceedings of the Workshop on Run-Time Result Verification, part of the Federated Logic Conference, Trento, Italy, July 1999 [38].

2. The topic of Babatunde is formalising reuse with imperfect components. Design with reuse typically accepts only those components in the repository which successfully match a given query specification, otherwise tries to obtain the needed components by adaptation, composition or programming. We argue that the specification method used for component retrieval must allow for a compromise between what is required from a component and what the repository has to offer. This leads us to study design which can accept imperfect components - satisfying one in a chain of increasingly weak specifications. In this context we investigate what effect using such imperfect components has on the system quality (its controlled degradation) and how we can improve this quality by upgrading individual components (a design method based on upgrading); for instance which components we should upgrade to achieve the target upgrade on the system level. The work is described in the report [1].

3. The topic of Balkhis is run-time result verification with awk. The goal of result-verification is to prove that one execution run of a program satisfies its specification, unlike implementation-verification where the proof extends to all possible runs. Due to its modest goals, result-verification has much fewer preconditions for its applications in practice, while sharing the same goal: making software more reliable. In this work we demonstrate how it is possible to carry out a fully automated result-verification with an awk interpreter; awk is a well known language for text-processing. As the formal specifications we use logic-based regular expressions [38]. Then we apply the awk interpreter in two ways. As the generator engine: given a specification the interpreter generates the awk program for checking this specification (on any input). As the verification engine: given a record of one execution (of the program we want to verify) as input the interpreter executes the generated awk program on this input to decide if the execution complies with the specification. This work is in progress.

The project's area of interest overlaps with the work of the research group on component based software development. Although the two projects have chosen different approaches to component reliability: run-time behaviour-checking and formal design support for correctness by construction, the two approaches can actually support each other. Run-time behaviour checking can support design assumptions about those library components which correctness cannot be verified statically, typically off-the-shelf components distributed as binary files. On the other hand, correctness by construction can support design of reliable and efficient component wrappers (or wrapper-generators) to carry out such run-time checking. Casino also focuses more on the design of tools while `component based software development' of DeTFoRS on mathematical theories and semantics. Whenever possible, we plan to seek opportunities for interaction between both projects.

Fellows

   
Wojciech Mostowski, University of Gdansk, Poland, 1 September 1998 - 31 May 1999
Babatunde Opeoluwa Akinkunmi, University of Ibadan, Nigeria, 4 January 1999 - 31 August 1999
Balkhis Abu Bakar, University of Northern Malaysia, Kedah, 5 September 1999 - 31 May 2000

Partners

  
University of Gdansk, Poland
Harbin Institute of Technology, China
Universidad Nacional del Sur, Bahia Blanca, Argentina
Institute of System Programming, Russian Academy of Sciences
University of Ibadan, Nigeria
University of Northern Malaysia, Kedah

Status

Ongoing. We plan to invite one or two fellows for this project from September 2000, to work on the component-based design with integrated use of formal methods (specification and verification) and fault-tolerance (run-time error detection/recovery).

Object-Oriented Design Patterns

Date of commencement

September 1998

Date of completion

ongoing

Staff responsible

Richard Moore

Abstract

Object-oriented patterns represent abstractions of good solutions to recurring problems in object-oriented software design. This abstractness means that a given pattern can be used in many different applications, which makes it a valuable tool for constructing reusable software and for helping object modellers achieve more effective results. However, patterns are invariably described informally in the literature, generally using natural language together with some sort of graphical notation, which makes it very difficult to give any meaningful certification of software developed using them.

In this project, we are attempting to develop a formal model of patterns which can form the basis for demonstrating that a particular design conforms to a given pattern.

Outputs

The project began as a case study conducted by Alejandra Cechich in which general properties of the structure of a range of different object-oriented patterns were specified. This work formed the contents of a UNUIIST Technical Report [9] and was also presented at and published in the proceedings of the 6th Asia-Pacific Software Engineering Conference (APSEC'99), Takamatsu, Japan, December 7-10, 1999.

In the current phase of the project, the model is being further developed to include behavioural properties of patterns, and at the same time it is being generalised to allow the matching between a general design and a specific pattern to be specified formally. This work is still in progress.

Fellows

 

Alejandra Cechich, Universidad Nacional del Comahue, 14 September 1998 - 23 January 1999
Alejandra Cechich, Universidad Nacional del Comahue, 7 November 1999 - 22 December 1999
Andres Flores, Universidad Nacional del Comahue, 7 November 1999 - 7 May 2000
Luis Reynoso, Universidad Nacional del Comahue, 7 November 1999 - 7 May 2000

Partner

Universidad Nacional del Comahue, Neuquén, Argentina

Status

This project is expected to continue beyond the end of the current batch of fellowships with one or two more fellows from Neuquén coming to UNU/IIST in 2000.

RAISE Projects

Timed RAISE 

Date of commencement

August 1997

Date of completion

Ongoing

Staff responsible

Chris George

Abstract

RAISE allows time to be modelled but has no specific built-in facilities for dealing with real-time problems. Duration Calculus (DC) is designed to describe and analyse timing properties of hardware or software but does not have the features to support the description of data structures, algorithms or the modularity of medium or large-scale systems.

This project aims to integrate RAISE and DC. It also therefore involves close collaboration between the advanced development and research groups at UNU/IIST.

There are several aspects of the project:

Extension of RSL: The features for describing time need to be added to the RAISE Specification Language (RSL). Currently these are a type for representing time (the non-negative real numbers) and a wait construct for specifying delays. The static and dynamic semantics of these extensions need to be defined. The extended language is called Timed RSL (TRSL).

Integration of TRSL and DC: If DC formulae and TRSL descriptions can both be used in a specification of a system then there needs to be some defined relation between them. One possibility is to define DC in terms of RSL. This is possible but makes it complicated to reason about DC formulae. A second possibility is to define a semantics of TRSL in DC. This needs only to be a partial semantics that expresses the timing characteristics of a TRSL description, as the untimed characteristics can use the existing proof theory of RSL. This is the approach currently being investigated.

Combined method: The development methods of RSL and DC need to be combined to support the development of TRSL descriptions. The convenience and effectiveness of the method ultimately justifies the choices made in the previous two activities.

Outputs

Anne Haxthausen of the Technical University of Denmark drafted in 1996 a paper DC + RSL which encoded DC in RSL, i.e. defined DC in terms of RSL. This was developed further by Xia Yong [62] into a proof assistant for DC using the RAISE justification editor, and used to verify the Gas Burner example.

Chris George proposed the extension of RSL with Time and wait constructs, defining the syntax, static semantics, and proof rules and outlining an operational semantics, all based on the existing definitions for RSL. Xia Yong corrected an error in the proof rules and completed the definition of the operational semantics [26].

Chris George started work on the method with a description of an alarm system, developing the use of "timer variables" to support the interpretation of RSL descriptions in terms of DC. He also started work on the proof rules needed to verify that TRSL descriptions satisfy DC formulae. The work to establish a DC semantics of TRSL was done by Li Li and He Jifeng [48]. This work also establishes some of the algebraic laws of TRSL, essential for its practical use.

Fellows

 

Li Li, University of Science & Technology of China, Hefei, China, 1 September 1998 - 31 July 1999

Partners

 

Technical University of Denmark

Status

Ongoing. The project has contributed considerably to the work on a motor control system undertaken with the DeTfoRS group. The proposed method to be used for developing and verifying timed systems is the main current area of investigation.

RAISE tools

Date of commencement

October 1997

Date of completion

Ongoing

Staff responsible

Chris George

Abstract

The current RAISE tools are comprehensive, robust and suitable for industrial projects. They are free of charge for teaching and research. But they currently only run on Sun workstations, which are often not available in developing countries.

This project aims to provide tools for RAISE that are easily portable, including to PC environments, and freely available as source as well as executable form.

A second aim of the project is to involve universities in developing countries in developing extensions to the tools.

Outputs

Chris George wrote a syntax and type checker for RSL (RSLTC) at the end of 1997. It uses a public domain compiler development system Gentle which seems to be a good basis for such a tool. Gentle produces C code which is easily compilable on a wide range of platforms.

The first version was placed on UNU/IIST's ftp site in February 1998. A second version which also catered for Timed RSL was made available in July 1998. Both versions were built on Sun, Linux, DOS and Windows platforms.

Tan Xinming produced a confidence condition generator and intends to work in future on a translator to C++. He Hua produced a pretty printer [28]. A third version including these two components plus a feature to display the module dependency tree was made available in February 1999. In September 1999 a fourth version including the expansion of implementation relations appeared.

Fellows

 

Ke Wei, Macau, 1 April 1999 - 31 March 2000 (part time)

Partners

 

Wuhan Jiaotong University, China
Peking University, China

Status

Ongoing. Currently Ke Wei is working on an animator. Interest has also been expressed by Nanjing and Hanoi Universities in working on translators, and Peking University plans to send another fellow during 2000.

2.3 Curriculum Development Project

Date of commencement

June 1996

Date of completion

Ongoing

Staff responsible

Chris George, Tomasz Janowski, Richard Moore

Abstract

UNU/IIST introduced the curriculum development project in 1996. Under this project, UNU/IIST is trying to increase its impact by assisting universities in developing countries to develop their ability to teach formal methods, the use of design calculi in software development. This is a common feature of computer science curricula in developed countries but much rarer in the developing ones. Fellows are professors or lecturers who come to UNU/IIST, usually for 3-4 months, to develop material for use in undergraduate and post-graduate courses. The material generally complements UNU/IIST's own material used on its advanced development courses. At the end of their stay, fellows take home the course material and software for the support of the methods being taught.

Outputs

Fellows produce a report during their visit, usually concentrating on a case study that can be used in teaching, and sometimes producing some other course material like OHP foils.

All the material, both UNU/IIST's and that developed by Fellows [9][5][52] is publicly available on UNU/IIST's ftp site.

Fellows

 

Ms S. Alejandra Cechich, 14 September 1998 - 23 January 1999, Argentina
He Bin, 8 December 1998 - 31 March 1999, China
Yumbayar Namsrai, 28 May - 27 August 1999, Mongolia
Shirnen Nyambaa, 28 May - 30 September 1999, Mongolia
Ishdorj Tseren-Onolt 28 May - 30 September 1999, Mongolia
Ming Zhong, 27 July 1999 - 26 October 1999, China
Jules Tapamo, 3 August - 30 November 1999, Sénégal
Jin Zhendong, 1 November 1999 - 10 March 2000, China
Wu Xiaojun, 1 November 1999 - 29 February 2000, China
Ms Ri Hyon Sul, 1 November 1999 - 29 February 2000, DPRK
Ms Pak Zong Ok, 1 November 1999 - 29 February 2000, DPRK

Partner Institutions

  

Universidad Nacional del Comahue, Neuquén, Argentina
Southwest Jiaotong University, Sichuan, China
Mongolian Technical University, Mongolia
National University of Mongolia
State Pedagogical University of Mongolia
Shenzhen University, China
Université Gaston Berger, Saint-Louis, Sénégal
Central Information Agency for Science and Technology, DPR Korea
Tianjin University
East China Shipbuilding Institute

Status

We expect this project to continue. As well as being able to introduce the material into their university curricula, we use the expertise of these Fellows to teach UNU/IIST off-shore courses, which reduces the cost of these courses in terms of the time, travel and subsistence of UNU/IIST staff.

We have also extended this project by developing a course on mathematics for computer science which could be offered alone or as a preparatory course to the RAISE and Duration Calculus courses. Yumbayar Namsrai developed this course with UNU/IIST staff [52].

During 1999 we have also collaborated under the curriculum development project with UNESCO's Beijing office on training teachers in higher education in formal methods and designing software for higher education administration. Two fellows each from Mongolia, China, and DPR Korea have come as Curriculum Development fellows and are doing their case studies in this particular area. Results will later be presented at a workshop in Beijing organised by UNU/IIST, UNESCO, and Macau UNESCO Centre. Implementation work based on the designs is planned. Funding of these fellows is joint between Japanese Funds in Trust, UNESCO and UNU/IIST.

Some work done as curriculum development reports is used as preparation for more substantial projects, such as He Bin's work on engineering design databases [5] and Alejandra Cechich's work on object-oriented patterns [9].

2.4 University Development Project

Date of commencement

January 1999

Date of completion

Ongoing

Staff responsible

Richard Moore

Abstract

The University Development Project, which complements the Curriculum Development Project, aims to strengthen all aspects of computer science teaching in universities in developing countries.

Many of these universities suffer not only from a serious lack of resources, including basic text books and teaching materials, but also in many cases from isolation from the international academic community: not only do they tend to have very little money available for international travel, but electronic connections via the internet are often prohibitively expensive and unreliable, even when they exist at all. This makes it very difficult for them to keep abreast of advances in the subjects they teach, particularly in a field such as computer science which changes so rapidly.

Under the University Development project we are trying to alleviate this situation by arranging for (generally young) computer science lecturers or professors from universities in developing countries to learn new courses at partner universities in industrialised countries, at the same time providing them with the supporting course materials. Then when they return to their own universities they use the knowledge they gain, together with the supporting course materials, as the basis for improving and updating existing courses or introducing new courses into the teaching curriculum of their own university.

The lecturers generally spend one semester at one of the partner universities, during which time they study several (generally four or five) courses offered by the partner university. These courses may be at either undergraduate or postgraduate level, depending on the specific needs of their own university.

In order to maximize the benefits from the project for any given country, we try as far as possible to run it on a "knowledge sharing" basis. This means that different lecturers selected for the project from the same developing country study different sets of courses, then the course material and text books they acquire through the project are made available to other universities in the same country after they complete their studies.

To this end, we have signed a Memorandum of Understanding with the Mongolian Universities Consortium, who will administer the knowledge sharing aspect of the project in Mongolia, and we are trying to make a similar arrangement with Vietnam. We are also looking at ways in which the knowledge could be shared amongst different countries, for example by making the courses developed by the lecturers available through our world wide web server.

The partner universities all provide the use of their facilities (attendance at lectures, use of office space plus library and computing facilities, and general assistance) and copies of their course material (lecture material, student's notes, course exercises, etc.) free of charge and in particular without payment of tuition fees. In addition, UNU/IIST provides recommended text books for each of the courses the fellows study, and these text books become the property of the fellows' home department when they return.

Outputs

Fellows produce a report on their fellowship after they return home describing what they have studied and how they will use the knowledge in their future teaching.

Fellows

  

During 1999, three computer science lecturers from Vietnam and three from Mongolia were awarded fellowships to study in the UK (Queen's University, Belfast and the Universities of Leicester, York and Oxford) and in Australia (University of Queensland), and one expert from Ethiopia to study in University of Macau. These are:

Hoang Viet Ha               04/01/99 -- 04/06/99 Vietnam  (York)
Agvaan Otgonbayar           23/01/99 -- 01/06/99 Mongolia (Leicester)
Le Quan Ha                  01/02/99 -- 28/05/99 Vietnam  (Belfast)
Tserenjav Uranbileg         01/02/99 -- 12/06/99 Mongolia (Queensland)
Le Nam Hien                 22/09/99 -- 20/12/99 Vietnam  (Leicester)
Tsedenpurev Myagmarsuren    28/09/99 -- 18/03/00 Mongolia (Oxford)
Dessalegn Mihret            19/02/99 -- 18/08/99 Ethiopia (Macau)

Partner Institutions in Developing Countries

  

Mongolian Technical University, Ulaanbaatar, Mongolia
National University of Mongolia, Ulaanbaatar, Mongolia
University of Natural Sciences, Ho Chi Minh City, Vietnam
University of Technology, Ho Chi Minh City, Vietnam
Vietnam National University, Hanoi, Vietnam
United Nations Economic Commission for Africa, Addis Ababa, Ethiopia

Partner Institutions in Industrialised Countries

  

Queen's University, Belfast, UK
University of Leicester, UK
University of Oxford, UK
University of Queensland, Brisbane, Australia
University of York, UK
University of Macau

Status

UNU/IIST sees this as an extremely important project and plans to continue it in the forseeable future. In the year 2000 specifically, we plan to further broaden the impact of the project in both Mongolia and Vietnam by selecting new fellows for training under the project in both the Spring and Autumn semesters, and also to extend the project to include fellows from Cameroon at the same times. In fact we have already arranged for one fellow from each of these three countries to take up four month fellowships at the University of Queensland beginning in February 2000, and have begun negotiations with potential host universities for the Autumn semester.

In the less immediate future, we plan to extend the project to other developing countries in Africa, Asia and Latin America. We also hope to extend the scope of the project in order to help partner universities in developing countries in other ways. First, we plan to make additional donations of text books to the libraries of the participating universities in order to further assist the development of their teaching. Second, we plan to help universities which do not have a computer science department set up such a department. To this end, we plan to invite a fellow who has experience in setting up such a new department to come to UNU/IIST for around three months during the first half of 2000 to design a suitable curriculum for a new department, and also to suggest how this curriculum should be developed as the department matures. Fellows from the target universities would then be trained in the appropriate courses at partner universities in industrialised countries as normal. Finally, we plan to help universities which currently do no research in computer science set up research groups.

We are actively seeking new universities to act as hosts for the fellows under this project, and we have already received an agreement to this effect from the University of Kent at Canterbury and are currently engaged in negotiations with a number of other universities in the UK and Canada.

We also plan to seek external co-funding for the project from bilateral and multi-lateral funding agencies in developing and developed countries.

Annual Report 1999

Contents