Annual Report 1998

Contents

2 Status of implementation of projects

1. Computing Science Research with Fellows

2. Advanced Software Technology Development with Fellows

3. Curriculum Development with Fellows

4. Fellow Training

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

6. Events

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

  
He Jifeng
Dang Van Hung
Xu Qiwen

Fellows

  
Xia Yong: 1 September 1997 -- 27 November 1998, China
Zhao Jianhua: 27 August 1997 -- 13 September 1998, China
Pablo Giambiagi: 5 September 1997 -- 13 March 1998, Argentina
Victor Braberman: 14 September 1997 -- 28 February 1998, Argentina
Gerardo Schneider: 1 September 1997 -- 28 February 1998, Uruguay
Hu Chengjun: 30 November 1997 -- 30 May 1998, China
Thomas Rasmussen: 15 January 1998 -- 7 March 1998, Denmark ¹
Sheila Karipel: 1 March 1998 -- 31 August 1998, India
Catalin Dima: 1 March 1998 -- 31 August 1998, Romania
Dimitar Guelev: 1 March 1998 -- 31 August 1998, Bulgaria
Wang Ji: 30 March 1998 -- 30 May 1998, China
Wang Hanpin: 15 May 1998 -- 31 August 1998, China
Zhan Naijun: 1 July 1998 -- 30 June 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 -- 10 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 November 1998 -- 8 February 1999, China

Visitor

   
Paritosh K Pandya: 15 June 1998 -- 30 June 1998, India

Partner Institutions

   
East China University of Science and Technology, Shanghai, China
Beijing University, China
Changsha Institute of Technology, Hunan, China
Nanjing University, China
Technical University of Denmark
Tata Institute of Fundamental Research, India
University of Buenos Aires, Argentina
Universidade Catolica de Pelotas, Brazil
National University of Hanoi, Vietnam
Naval Physical & Oceanographic Laboratory, Cochin, India
University of Bucharest, Romania
University of Sofia, Bulgaria
Chinese Academy of Sciences, Beijing, China
University of St. Petersburg, Russian Federation
University of Communication and Transport, Vietnam
University of Science and Technology, Hefei, China
Northern University of Malaysia, Malaysia
Beijing University of Posts & Telecommunication, China

Outputs

   The achievements in 1998 can be summarised as follows:

1. New algorithms for checking real-time systems against linear duration properties based on integer verification techniques [1][2]. In comparison with other conventional methods, these can reduce space complexity significantly.

2. A procedure for checking a timed automaton for a linear duration invariant using linear programming techniques [3]. Compared with the one developed previously in UNU/IIST, the new one can be applied to a much wider class of timed automata.

3. Integrating Duration Calculus with the industrially-applicable specification notation RSL [4]. As a result, the existing RSL tools can be employed to prove DC theorems. An operational semantics of the extended RSL is also being developed.

4. A first step towards a Duration Calculus semantics of a commercially available hardware description language Verilog [5].

5. Incorporating verification and refinement techniques for time automata in DC.

6. A calculus of duration on abstract domains ([6]). This provides a unified framework for some extensions of Duration Calculus dealing with superdense computation.

7. Verification of the STARI circuit ([7][8]).

8. Interval Temporal Logic with infinite intervals ([9]).

9. Further development of the DC proof assistant based on PVS ([10][11]).

10. Relationship between theory of real-time automata and simple Duration Calculus formulae ([12]).

Reports and Technical Notes produced in 1998 by the group are:
[1][5][3][13][6][14][15][2][16][17][18][19][7][8][12][10][11][9].

There were 18 presentations at international conferences and workshops in 1998 by fellows, ex-fellows and staff:
[20][21][22][23][24][25][26][27][4][1][5][3][28][29][30][31][32][33].

2.1.2 Future Project: Hardware/Software Co-design

Real-time embedded applications vary in size and scope from wristwatches and microwave ovens to factory automation and nuclear power plant control systems. Applying a general methodology to the development of such systems means that it must meet the tight performance and size constraints of small 4-bit and 8-bit controllers, yet also scale up to networked arrays of powerful processors coordinating their activities to achieve a common purpose. Most embedded systems interact directly with electrical devices and indirectly with mechanical ones. Programming these device drivers requires intimate knowledge of the electrical properties and timing characteristics of the actual devices. Furthermore, virtually all embedded systems either monitor or control hardware, or both. The design and analysis of such an integrated and tightly coupled mixed hardware/software system (e.g. a sensor or PC network card) and its associated software driver are bound to be challenging.

In the hardware industry, simulation is often considered synonymous with verification. The design process usually consists of developing an implementation from a specification without use of any formal proof techniques. The intended implementation's hardware and software are then simulated for a number of inputs (an approach known as co-simulation). Bugs are then discovered and removed, and the simulation process is repeated over again. In the past few years, there have been several successful hardware/software verification efforts, some using model-checking techniques, others using higher order logic systems, and others based on functional calculi. However, formal verification cannot completely replace the existing simulation approach. This is because simulation provides powerful and more accessible tools for rapid prototyping and testing. What is needed is an approach where the design process is soundly based upon formal techniques, but includes integrated support for simulation. This combination would bring more reliability within an environment which does not require a complete changeover from current practice.

Therefore, an important and timely issue for the correct design of mixed hardware/software in the next century is the search for a highly compositional lean formal approach that enables us to keep up with the fast growth in the complexity and variety of electronic devices and their associated software. By compositional approach, we include any method by which the properties of a system can be inferred from properties of its components, without additional information about the internal structure of those components. And by lean formal approach, we take the view that the method must be supported by automated tools which make the method more widely accessible to industrial users. Such tools should provide compositional rapid prototyping, testing and verification.

We are going to develop an integrated and practical approach for the compositional specification, design and analysis of mixed hardware/software systems. The project starts with a unified theory to ensure complete consistency between different stages in the development process and different parts of the product. The theory promises to cross all the boundaries involved:

• event and state

• continuous time and discrete time

• hardware and software

• simulation and verification

• abstraction and execution

Our semantics will take the form where each module may be modelled by a DC formula, based on hybrid time interval, describing its signal's behaviour during the module's life-time, and each component within a module is described in the shared-state model. Since sharing output is a main feature of hardware, we can tackle both racing conditions and instability. This requires a conservative extension to DC semantics.

We will test the theory by application to commercially available design notations (the hardware description languages Verilog and VHDL) and a number of case studies.

Our objective is to improve confidence in robustness of systems developed in a mixture of hardware and software, and to reduce development time for delivery and upgrading of consumer products, implemented in mixed technology. This would be achieved by performing the following work packages:

1. Unified model for co-design which incorporates features of CSP (Communicating Sequential Processes) and Duration Calculus or ITL (Interval Temporal Logic):

   • A combined event-state model.

   • Specification-oriented semantics of a subset of Verilog.

2. Exploring compositional development strategies:

   • Refinement calculus for the unified theory.

   • Algebra of Verilog programs.

   • Protocols for interfacing hardware and software components.

3. Linking specification-oriented semantics with simulation semantics of Verilog:

   • Consistency of various styles of semantics.

   • Derivation of a simulator from algebraic semantics.

4. Proof of concepts. It is fundamental to our approach that the theory developed should be applicable to real-world mixed hardware/software systems. We are going to perform some proof of concept experiment, and to ensure that the formal design process, analysis and algebraic manipulation can be supported by CASE tools so that eventually much of the burden of formal design refinement can be removed from the programmer.

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 development 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 6-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 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 and jointly carried out with the Chinese Ministry of 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

PortMan - Port Management

Date of commencement

September 1997

Date of completion

May 1998 (phase 1)

Staff responsible

Chris George

Abstract

Large ports need to deal with a number of disparate activities: the movement of ships, containers and other cargo, the loading and unloading of ships and containers, customs activities. As well as human resources, anchorages, channels, lighters, tugs, berths, warehouse and other storage spaces have to be allocated and released. The efficient management of a port involves managing these activities and resources, managing the flows of money involved between the agents providing and using these resources, and providing management information. Many separate computer management and information systems will be involved. Integrated port management is concerned with integrating these separate systems.

This project is concerned initially with a domain analysis of the port components and their relations, and specifying the overall "backbone" architecture of an integrated system.

Outputs

The objective in the first phase was to do the domain analysis and produce a specification of that domain. We produced specifications of several component systems:

1. Vessel traffic management

2. Container traffic control

3. Cargo management information

Later phases, possibly also involving other partners, will probably add financial management and executive information components, and elaborate components in more detail.

A major aim was to make the initial descriptions generic - applicable to any port, perhaps river ports as well as sea ports.

The basic domain analysis was completed, concentrating on ship and container management [34]. For ships it deals with anchorages, berths and channels between them. For containers it deals with various storage areas and the movement of containers between them. We also considered the creation and execution of tasks, like berthing a ship, involving the allocation of various resources, such as channels, tugs and pilots.

Fellows

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

Both Fellowships were partly supported by ECIL.

Partner

Electronics Corporation of India Ltd. (ECIL)

Status

It was hoped to have one or two Fellows from ECIL to start in September 1998. But apparently ECIL, while wanting to continue the project, is currently unable to find suitable people given its current staffing situation.

We hope also to invite one or more Fellows from Wuhan Jiaotong University, who are interested in river port management.

MIICI - Enterprise Modelling, Analysis and Implementation

Date of commencement

September 1997 (Phase 3)

Date of completion

Fellows are invited until May 1999.

Staff responsible

Tomasz Janowski

Abstract

The project is about the application of formal methods to enterprise engineering, for business organisations in general and for 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 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

In the current phase we concentrate on modelling of virtual organisations, composed from the enterprises for manufacturing discrete-parts products. We adopted a unified view on modelling core activities of an enterprise in terms of product-related resources, processes and business goals. The goal is to fulfill a set of orders for manufacturing and delivery of products to customers (other enterprises). Each customer order is implemented by a single process which executes a sequence of manufacturing operations on the shared resources, concurrently with other processes. The process may also issue orders for buying products from other enterprises, making its own goal conditional on the satisfaction of such orders. In the virtual organisation we are able to model supply-chains, outsourcing and cooperation between individual enterprises. We allow enterprises to interact by matching one enterprise's purchase orders with another enterprise's customer orders. We allow them to cooperate by a process which partly executes on the resources of one enterprise and partly on another's, crossing organisational boundaries. We also allow them to compete for purchase orders, by marketing activities which can influence the consumer's choice.

In this stage, we revised Research Report 92 about the integration of enterprise models and models for marketing analysis, which was presented by Gustavo Lugo at the 2nd IFIP Conference "Design of Information Infrastructure Systems for Manufacturing" (DIISM98), Denver, USA, May 1998 [35]. We also produced report Research Report 131 about composition of enterprise models, which was presented by Tomasz Janowski at the 3rd IEEE/IFIP International Conference: Information Technology For Balanced Automation Systems in Manufacturing (BASYS98), August 1998, Prague, Czech Republic [36]. Finally, we also produced report Research Report 137 about operational semantics for enterprise models, which was presented by Zheng Hongjun at the 2nd IEEE International Conference on Formal Engineering Methods (ICFEM'98), December 1998, Brisbane, Australia [37].

Fellows

  
Gustavo Lugo, CEFET, Parana, Brazil, 1 September 1997 - 31 May 1998
Zheng Hongjun, Peking University, China, 3 November 1997 - 15 August 1998
Huang Biqing, Tsinghua University, China, 16 November 1998 - 15 January 1999
Liu Yonghe, Tsinghua University, China, 16 November 1998 - 15 May 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

Status

The project is expected to continue. With two fellows from CIMS Centre in Tsinghua University, China, we aim to extend the model to include service-based interaction between members of a virtual enterprise, including but not limited to manufacturing services (e.g. logistics, sales, product design, production planning). With Liu Yonghe we also aim to design prototype software for partner selection for the virtual enterprise.

MultiScript

Date of commencement

September 1995

Date of completion

March 1999

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

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 [40] describes the (modified) basic model of multi-directional, multi-lingual documents; the second [41] describes the display and printing of such documents; and the third [42] 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 [43].

The reports from the second phase are being used as the foundation for the design and implementation of a prototype software system in the current phase of the project.

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 has been jointly prepared (UNU/IIST, Mongolia, and China) and was presented at a meeting of WG2 in London at the end of September 1998.

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

The development of the prototype MultiScript system is well underway and is expected to be completed by the end of this phase of the project.

ABC - Airline Business Computing

Date of commencement

September 1997 (phase 2)

Date of completion

March 1998 (phase 2)

Date of commencement

September 1998 (phase 3)

Date of completion

February 1999 (phase 3)

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 [44] 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 worked with the Fellow from the first phase and 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. He is developing a specification of part of the second component of the flight effectiveness analysis system, namely how results from the flight effectiveness reports are used to help the airline improve the effectiveness of its flight operations. This work is being supported (via email) by colleagues in Vietnam. When this specification is completed, it will be used, together with the output from phase 2 of the project, as the basis for building a demonstrator software system for the full flight effectiveness analysis system.

Outputs

One UNU/IIST technical report [44] was produced at the end of the second phase of the project. This gave both an informal and a formal description of the first part of the flight effectiveness analysis system. Informal and formal descriptions of the selected parts of the second component of the flight effectiveness analysis system is well advanced and construction of the prototype software system has begun.

Fellows

 
Tran Manh Thang, Vietnam Airlines, 5 September 1997 - 4 March 1998
Nguyen Hong Viet, Vietnam Airlines, 5 September 1997 - 4 March 1998
Than Quoc Dang, Vietnam Airlines, 1 September 1998 - 28 February 1999

Partner

  
Vietnam Airlines

Status

A technical report on this third phase of the project and the prototype software system are expected to be completed on schedule.

Casino - Methods and Tools for Building Software from Components

Date of commencement

May 1997 (Phase 2)

Date of completion

Fellows invited till May 1999.

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 do we check consistency if the implementation details are unavailable (because they are proprietary, remote or even non-existent)? How can we formulate a request for a component? How can we choose one? How can we assemble components and calculate the semantics of the composition? To what extent can we adapt a component which fits only partly into our design? How can we obtain components? How can we store them for effective retrieval? How can we postpone "assembly" till run-time, resulting in software which evolves with its environment? What is the semantics of this? 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. calculating the semantics of composition, generating proof conditions, generating component wrappers to monitor their 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 and integrate them at the end into a single environment: Composition Workbench.

Outputs

So far the project work has gone into three areas of study: (1) Fault-tolerance with Yun Xiaochun. PhD thesis based on the results of the project: "Research on the reconfiguration technology of reusable software components". One paper: "Fault-Tolerant Software Composition from Verified and Unverified Components", to be submitted. Describes how to assemble the components to achieve reliability of the composition despite possible failures of individual components. (2) Abstraction with Elsa Estevez. Paper is written: "Bisimulation Abstraction for Selection of Software Components in RAISE". Describes how bisimulation can play the role of an abstracting equivalence for selecting components described as RSL modules, concerned only with their external behaviour. (3) Monitoring, with Wojciech Mostowski from Gdansk, Poland, September 1998 until May 1999. Paper and software are written: "Pattern-Matching for Software Reliability via Run-Time Behaviour-Checking", how to use regular expressions as formal specifications of software components, suitable for checking their behaviour (by pattern-matching) at run-time. Implementation under way to generate a component wrapper from its specification.

Fellows

   

Yun Xiaochun, Harbin Institute of Technology, China, 5 May 1997 - 25 January 1998
Wojciech Mostowski, University of Gdansk, Poland, 1 September 1998 - 31 May 1999
Elsa Estevez, Universidad Nacional del Sur, Argentina, 31 August - 18 December 1998

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

Status

The project is expected to continue. A new fellow arrives in January 1999: Mr. Babatunde Opeoluwa Akinkunmi from the University of Ibadan, Nigeria. He will initiate the fourth area of study: Composition. How to exploit applicative part of the RSL language to specify individual components and imperative/concurrent part to assemble them together. How to calculate the result of such a composition, semantically.

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 [4] 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.

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 has also started work on the proof rules needed to verify that TRSL descriptions satisfy DC formulae. This work is now being continued by Li Li.

Fellows

 

Xia Yong, East China University of Science and Technology, China, 1 September 1997 -- 27 November 1998
Li Li, University of Science & Technology of China, Hefei, China, 1 September 1998 -- 31 July 1999

Partners

 

Technical University of Denmark

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 and it is hoped that her group at Peking University will work on further tools.

Fellows

 

Tan Xinming, Wuhan Jiaotong University, China, 14 July 1998 - 13 September 1998
He Hua, Peking University, China, 1 September 1998 -- 31 December 1998

Partners

 

Wuhan Jiaotong University, China
Peking University, China

2.2.8 Future Projects

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 the subjects in UNU/IIST's "agenda", specifically 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 [45][46][47][48][49][50][51][52][53][54] is publicly available on UNU/IIST's ftp site.

Fellows

 

Marcel Fouda, 4 September 1997 - 3 March 1998, Cameroon
Tsend Ganbat, 1 September 1997 - 12 January 1998, Mongolia
Hrushikesha Mohanty, 5 May 1998 - 4 August 1998, India
William Shu, 1 May 1998 - 30 September 1998, Cameroon
Jong Hyen Chol, 1 September 1998 - 30 November 1998, DPR Korea
Choe Chun Ho, 1 September 1998 - 30 November 1998, DPR Korea
S. Alejandra Cechich, 14 September 1998 - 23 January 1999, Argentina
Toshiyuki Tanaka, 1 June 1998 - 31 July 1998 Japan
He Bin, 8 December 1998 - 31 March 1999, China

Partner Institutions

  

University of Yaoundé I, Cameroon
Mongolian Technical University, Mongolia
University of Hyderabad, India
University of Buea, Cameroon
Wuhan Transportation University, Wuhan, China
Korea Computer Center, Pyongyang, DPR Korea
Central Information Agency for Science and Technology, Pyongyang, DPR Korea
Universidad Nacional del Comahue, Neuquén, Argentina
Kyushu University, Fukuoka, Japan
Southwest Jiaotong University, Sichuan, China

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. UNU/IIST also intends to extend the 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. One fellow will come to UNU/IIST for 3 months beginning 28th May 1999 to develop this course with UNU/IIST staff.

Annual Report 1998

Contents