|
|
|
Annual Report 2000 | Contents | |
1. Theory and Design Methods for Real-time Systems
2. Formal Techniques for Software Development
3. Curriculum for Formal Software Development
4. Development of Computer Science Departments in Developing Countries
5. IT Training Courses in Developing Countries 6. IT Development in
Macau
All projects are designed to serve the public and private sector institutions of developing countries and Macau 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
These projects are closely interlinked. All UNU/IIST projects have a training component and involve one or more Fellows.
UNU/IIST also organises events and dissemination activities. They fit into UNU/IIST's research, advanced development and training 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. At the same time UNU/IIST conducts
its training activities to improve the computer science curricula in developing
countries.
Real-time systems form an important class of today's computer-controlled
systems. Real-time software is already controlling critical functions such
as nuclear reactors, automobiles, aircraft and spacecraft, and is increasingly
governing the infrastructure for communication, power and transportation.
Such systems are often required to respond to externally generated stimuli
with specified real-time constraints. Safety and reliability of systems
are extremely critical. Design of real-time systems has rapidly become
one of the pervasive intellectual challenges of the modern age. A scientific
basis for real-time system development must lie on a formal conceptual
understanding of the application domain, the software requirements, and
the implementation mechanism so that the reliability of software rests
on formal calculations and reasoning rather than informal hunches.
The project aims to develop theory, design methods and tool support for the development of realtime systems, based on Duration Calculus (DC) which is designed for describing and reasoning about the real-time behaviour of systems.
The formal techniques we are developing include:
1. design calculi and refinement methods based on DC and its extensions.
2. formal semantics of real-time languages (Timed RSL, VERILOG, etc).
3. deductive verification methods and tools for real-time programs.
4. component-based design techniques.
5. model-checking techniques and tools for real-time systems.
6. integration of the DC framework with other real-time system design
techniques (such as
timed automata, timed diagrams, real-time UML).
7. formal engineering methods for co-design of mixed hardware/software
systems.
8. Program partitioning techniques for hardware/software co-design.
Staff responsible
Visitors
17 institutions from nine countries have participated in this project.
1. Li Yongjian (16 Mar. 2000 - 30 Nov. 2000)
2. Li Yong (21 Mar. 2000 - 20 Jan. 2000)
3. Hong Ki Tae (1 May 2000 - 30 Nov. 2000)
4. Juliano Iyoda (15 May 2000 - 14 Jan. 2001)
5. Francois Siewe (26 Aug. 2000 - 25 Nov. 2000)
6. Qin Shengchao (1 Sep. 1999 - 31 Jul. 2000)
7. Do Van Nhon (1 Sep. 1999 - 31 May 2000)
8. Wang Jianzhong (1 Sep. 1999 - 31 May 2000)
9. Dimitar Guelev (1 Mar. 2000 - 30 Jun. 2000)
10. Wasim Khan (1 Sep. 1999 - 14 Feb. 2000)
11. Dangaasuren Garmaa (1 Sep. 1999 - 28 Feb. 2000)
12. Ngo Hoang Huy (15 Apr. 1999 - 14 Jan. 2000)
13. Lutbat Yadamsuren (1 Sep. 2000 - 28 Feb. 2001)
14. Chang Chen (1 Nov. 2000 - 30 Sep. 2001)
15. Li Xuandong (1 Nov. 2000 - 30 Nov. 2000)
In 2000, under this project 7 off-shore training courses and lectures were delivered in 7 countries. The project engaged in the organisation of 9 international conferences. Please refer to sections 3.3 and 5.1 for details.
Publications
The technical reports produced by the project in 2000 are [26, 43, 39, 40, 18, 21, 24, 52, 38, 37, 22, 23, 41, 57, 67, 64, 61]. A total of 12 papers ([42, 48, 27, 60, 26, 25, 21, 24, 38, 37, 57, 9] ) has been presented and published in the proceedings of international conferences, and 5 other papers ([36, 45, 8, 46, 35]) have been published in journals during the year.
Details of Project Achievements
Design Calculi based on DC We have proposed a syntactical approach to design of real-time distributed systems that handles both continuous time and discrete models in a uniform logical framework. It approximates continuous state variables by discrete ones and defines a link between them. From a specification of the requirements of a real-time system as a formula over continuous states, it can derive a discrete design of a digital controller. This approach also provides a set of rules for verifying the correctness of the implementation syntactically [60, 52, 61].
Higher Order DC and Variants of Probabilistic Duration Calculus We have developed a new powerful technique for reasoning about the behaviour of real-time systems. Namely, we have introduced Higher Order Duration Calculus with recursion, and developed a complete proof system for it. With this technique we can link different levels of the development process of real-time systems together in a uniform logical framework. We introduced probabilistic neighbourhood logic and provided a complete proof system for it for reasoning about the dependability of real-time systems [21, 24].
Formal Semantics of Real Time Languages VERILOG is an IEEE standard HDL (Hardware Description Language) widely used in industry in support of design of hardware devices at various levels of abstraction. A hardware description language is a high level programming language, with the usual programming constructs, and appropriate extensions for real-time, concurrency and data structures suitable for modelling hardware. Different VERILOG modules of the same device are used during the design process and it is important that these be equivalent; formal methods for ensuring this could be commercially significant. However there is very little theory available to help. We have given an operational semantics for a simulator algorithm of VERILOG, and provided the first denotational semantics using the notations of DC for VERILOG. It acts as the basis for exploring algebraic laws of the language, which are useful in design of synthesisers and program partitioning algorithms for co-design [26, 41].
Formal Methods for Co-design Hardware and software co-design is a design technique which
delivers computer systems comprising hardware and software components. A critical phase of the co-design process is to decompose a program into hardware and software. We have proposed an algebraic partitioning method and verified its correctness in the algebra of programs. We also proposed an integrated approach to mixed hardware/software co-design. [57, 38].
Model-checking Techniques We have analysed when a system history property can be converted into a system timed state property, and developed an algorithm for the verification of a restricted history property like temporal linear duration properties which have the same complexity as for the state property [67].
At the same time, our off-shore partner institutes also helped us construct automatic tools for Duration Calculus. Paritosh Pandya, working at the Tata Institute of Fundamental Research, India, one of our off-shore partner institutes, has helped us to construct tools including a validity checker for DC formulae based on the tool MONA, and tools that
allow verification systems SMV and ESTEREL to be used for model checking real-time properties of designs. These model checking tools have been used in the verification of a multimedia communication protocol for our off-shore partner Beijing University of Post and Telecommunication [37].
Another of our off-shore partners, University of Nanjing, has also developed
a model checker (implemented in Java), to check whether a positive loop-closed
automaton satisfies a linear duration property. By using it, the models
of the gas burner, the water-level monitor and several other case studies
have been checked.
1. Integration of DC with other design techniques
2. Formal engineering methods for co-design
3. Component-based design methods
4. Modelling and verification of multimedia systems
5. New training courses
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.
UNU/IIST pursues this project 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
This project has evolved over time into three groups of subprojects:
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, with building software from existing components, and with object-oriented patterns.
RAISE projects have arisen from the need to support and develop the formal method that UNU/IIST uses for this project and the curriculum development project. 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 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.
Both these RAISE projects are open-ended and involve fellows coming
to work on particular components or aspects.
Almost all Fellows are identified through UNU/IIST's advanced development
courses. Fellows for application projects are often industrial but may
also be from academic institutions. Fellows for thematic and RAISE projects
are almost always from academic institutions.
For application projects, industrial partners are asked to contribute
to the initial and prototype phases, and to increase their share of funding
with each phase. To what extent they are able to do so varies. Partners
are expected to fund the product phase themselves.
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.
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.
(a) Abstraction
2. Domain analysisAt a particular stage in development one can abstract away from some details while concentrating on others.
(b) RigourFormal 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.
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. And, of course, we also give them the new tools for RAISE.
MultiScript
Date of commencement September 1995
Date of completion Spring 2001
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. In addition, there is an increasing interest in using computers to electronically archive historic documents, many of which are multi-lingual.
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 has also contributed, 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 now forms part of the ISO/Unicode international standard, a coding system which covers the majority of the world's languages. This international standard encoding for traditional Mongolian script was officially published by ISO (in ISO/IEC 10646, 2nd Edition) and by the Unicode Consortium (in The Unicode Standard, Version 3.0) in March 2000.
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 multidirectional 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 [12]. This paper was presented at the 1997 International Conference on the Computer Processing of Oriental Languages (ICCPOL'97), Hong Kong, in April 1997.
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 [14] describes the (modified) basic model of multi-directional, multi-lingual documents; the second [51] describes the display and printing of such documents; and the third [13] 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^alo, France, in March/April 1998.
The reports from the second phase were used as the foundation for the design and implementation of a prototype software system in the third phase of the project. This was 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 was completed in this phase, though no work was done on the top-level interface for displaying and printing documents.
This implementation work forms the subject of an M.Sc. thesis by the fellow responsible and is also detailed in a UNU/IIST Technical Report [3].
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, which was jointly prepared (UNU/IIST, Mongolia, and China) and presented at a meeting of WG2 in London at the end of September 1998, was officially adopted as the international standard encoding for traditional Mongolian script and published in the official standards in March 2000. A UNU/IIST Technical Report [15] describes the encoding and gives information on implementing software systems which conform to it. This report was presented at the 16th International Unicode Conference, Amsterdam, The Netherlands, March 2000. An overview of the MultiScript project as a whole as well as a demonstration of the prototype system were also given at the same conference.
Fellows
Ms. 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 is currently completing the development of the prototype MultiScript system.
Software Reuse
Date of commencement July 2000
Date of completion Continuing
Staff responsible Richard Moore
Abstract Software reuse is an important problem for many companies, as they try to make their "legacy" code into an asset they can draw on rather than a maintenance liability. This project is concerned initially with the specification and design of a system supporting component-based software reuse
Outputs This project has only just started.
Fellows
Ms Raoudha Beltaifa, Campus Universitaire La Manouba, Tunis, Tunisia,
1 July 2000 - 31 March 2001
Partner Campus Universitaire La Manouba, Tunis, Tunisia
Status Continuing
Engineering Design Database
Date of commencement September 1999
Date of completion Continuing
Staff responsible Chris George
Abstract A team at the CAD centre of Southwest Jiaotong University,
Chengdu, Sichuan,
China is developing an engineering design database to support architectural
design of buildings. The system will have three main components:
Intelligent design support will involve activities like finding
suitable design cases to use for the current problem, and checking design
rules.
The initial aim of the project at UNU/IIST was to formalise the basic design of the database. This was designed as a pair of a cases database to hold information about design databases, and a model database that holds generic information about cases and about design rules that need to be applied to them. A language for design rules, extended to a language for defining searches, was defined and given an operational semantics in terms of the databases. A prototype tool was also produced by (automatically) translating the specification into C++ and providing a front-end written in Tcl/Tk.
Outputs A UNU/IIST report [59] was produced. A short paper based on this report was accepted and presented at APSEC'2000 in December.
Fellows
Li Shuguang, Southwest Jiaotong University, 1 September 1999 - 31 March
2000 Jiang Qing, Southwest Jiaotong University, 1 September 1999 - 31 March
2000 Ms. Wang Yanjie, Southwest Jiaotong University, 10 September 2000
- 9 April 2001 Wang Zhuo, Southwest Jiaotong University, 10 September 2000
- 9 April 2001
Partner
CAD Centre, Southwest Jiaotong University, Chengdu, Sichuan, China
Status The first two fellows left at the end of March 2000. Two new fellows arrived in September 2000 and are continuing the project, working on the problem of supporting distributed interactive design work.
Thematic Projects
MIICI - Enterprise Modelling, Analysis and Implementation
Date of commencement September 1997 (Phase 3)
Date of completion Continuing
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 emergent concepts like outsourcing and virtual organisations, business process engineering and re-engineering, recycling and product life-cycle, lean and just-intime production, concepts which are increasingly adopted by manufacturing organisations worldwide to address challenges of global competition and unstable market conditions.
Outputs In this period:
Roger Atsa, University of Yaound'e I, Cameroon, 1 April 2000 - 30 September 2000 Nitesh Shrestha, Kathmandu University, Nepal, 1 June 2000 - 30 November 2000 Phan Cong Vinh, Vietnam National University, HCM City, 1 July 2000 - 31 December 2000 Adegboyega Ojo, University of Lagos, Akoka-Lagos, Nigeria, 1 July 2000 - 31 December 2000
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
University of Yaound'e I, Cameroon
Kathmandu University, Nepal
Vietnam National University, HCM City, Vietnam
University of Lagos, Akoka-Lagos, Nigeria
Status Continuing.
Casino - Methods and Tools for Building Software from Components
Date of commencement May 1997 (Phase 2)
Date of completion Continuing
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 preexisting 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 The project continued in this period with one fellow, Ms Balkhis Abu Bakar. Her report [6] shows how to write formal result-based specifications, how to generate a verifier program to check a given specification and to carry out result-verification according to the generated program. The execution result is written as a text file, the verifier is written in AWK (special-purpose language for text processing) and verification is done automatically by the AWK interpreter, given the verifier and the execution result as inputs.
The project's area of interest overlaps with the planned work of the research group on component based software development, as part of the DeTfoRS project. Although the two projects have chosen different approaches to component reliability: run-time behaviourchecking 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 wrappergenerators) 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
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 Continuing.
Object-oriented Design Patterns
Date of commencement November 1999 (though earlier work was done by Ms Alejandra Cechich on a Curriculum Development fellowship September 1998 - January 1999).
Date of completion Continuing
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 activity, we have developed a formal model of patterns which can form the basis for demonstrating that a particular design conforms to a given pattern, and we have used this model as a basis for formal specifications of most of the patterns in the GoF catalogue (Gamma, Helm, Johnson and Vlissides; Design Patterns - Elements of Reusable ObjectOriented Software; Addison-Wesley, 1995). We have also investigated extending the model to allow matching an object-oriented design against multiple patterns simultaneously. In future work we plan to look at variants of patterns and at the possibility of using the formal model as the basis for software tools which could help designers apply patterns.
Outputs Initial work by Alejandra Cechich [10] formally specified properties of some of the GoF patterns directly, concentrating in particular on the responsibilities and collaborations of the pattern participants. Based on this, a more general model [17] was developed which not only permitted many of the behavioural properties of the patterns to be specified but which also could be applied to an arbitrary object-oriented design and not just to individual patterns. In addition, this model specified formally how to match a design against a pattern, thus allowing us to formally specify the patterns in such a way that their consistency and completeness can be checked, and also providing a means of formally verifying that a given subset of a design corresponds to a given pattern.
Using this model, Luis Reynoso, Andres Flores and Gabriela Aranda specified respectively the properties of the behavioural [56], structural [16] and creational GoF patterns [5]. Gabriela Aranda also extended the model to describe compound patterns, involving the composition of two or more GoF patterns [4].
Fellows
Luis Reynoso, Universidad Nacional del Comahue, Neuqu'en, Argentina, 7 November 1999 - 31 May 2000 Andres Flores, Universidad Nacional del Comahue, Neuqu'en, Argentina, 7 November 1999 - 31 August 2000 Ms Gabriela Aranda, Universidad Nacional del Comahue, Neuqu'en, Argentina, 1 May 2000 - 15 December 2000
Partner Universidad Nacional del Comahue, Neuqu'en, Argentina
Status Intended to continue
RAISE Projects Timed RAISE
Date of commencement August 1997
Date of completion Continuing
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 There has been no activity on this project in this period.
Status Expected to be resumed.
RAISE Tools
Date of commencement October 1997
Date of completion Continuing
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.
During 1999 confidence condition generation (written by Tan Xinming,
Wuhan Jiaotong University, China) and and pretty printing (written by Ms
He Hua, Peking University, China) were added, along with a feature to graphically
display the module dependency tree.
During 2000:
Ke Wei wrote a translator to Standard ML. A test case construct was added to RSL to support animation of specifications using SML [20] Ms Hoang Thi Tung Lam worked on a translator to Java as part of her PhD [44]. Ahn Yong Jun wrote a translator to C++ [1].
Fellows
Ke Wei, Chinese Academy of Science, China, 1 April 1999 - 31 July 2000 (part time) Hoang Thi Tung Lam, Hanoi University of Natural Science, Vietnam, 1 May 2000 - 28 August 2000 Ahn Yong Jun, Kim Il Sung University, Pyongyang, DPR Korea, 1 May 2000 - 30 November 2000
Partners
Wuhan Jiaotong University, China
Peking University, Beijing, China
Chinese Academy of Science, Beijing, China
Hanoi University of Natural Science, Vietnam
Kim Il Sung University, Pyongyang, DPR Korea
Status Continuing.
Date of commencement June 1996
Date of completion Continuing
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 [66, 70, 54, 20, 55, 11, 47] is publicly available on UNU/IIST's ftp site.
Fellows
Jin Zhendong, 1 November 1999 - 21 April 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
R. K. Ghosh, 15 May 2000 - 14 August 2000
Ngolah Cyprian Foinjong, 1 June 2000 - 31 August 2000
Manas R. Patra, 1 April 2000 - 31 August 2000
Ms Virginia Mauco, 13 July 2000 - 14 December 2000
Partner Institutions
Tianjin University, Tianjin, China
East China Shipbuilding Institute, Zhenjiang, Jiangsu, China
Central Information Agency for Science and Technology, DPR Korea
University of Buea, Cameroon
Indian Institute of Technology, Kanpur, India
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 [7] and Alejandra Cechich's work on object-oriented patterns
[10].
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 [49].
During 1999-2000 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.
See section 6.1.4.
Date of completion Continuing
Staff responsible Richard Moore
Abstract The Computer Science Department 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 Computer Science Department 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.
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 the recommended text book for each of the courses the fellows study, these text books becoming the property of the fellows' home department when they return, and supplements this by offering more general support to the participating countries to help them to improve the overall standard of their computer science libraries.
In addition to the activity described above, the project has also developed a recommended computer science curriculum for developing countries [50] under a Special Service Arrangement with an experienced professor from Mongolia. This will be used in the future to help universities in developing countries set up new computer science departments, and will also be used to advise universities which already have computer science departments how best to develop and expand their teaching curriculum.
Partners
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
Hanoi University of Technology, Hanoi, Vietnam
University of Yaounde I, Cameroon
in Industrialised Countries:
Queen's University, Belfast, UK
University of Leicester, UK
University of Oxford, UK
University of Queensland, Brisbane, Australia
University of Toronto, Canada
University of York, UK
Status Intended to continue.
|
|
|
Annual Report 2000 | Contents | |