Executive SummaryExecutive Summary
Top Top
Postgraduate training/teaching activities Postgraduate training/teaching activities
Status of implementation of project activities

Status of implementation of project activities

Formal Techniques for Software Development

Staff responsible
Chris George, Bernhard K. Aichernig

Budgetary provision for 2002
USD 60000

Amount expended and obligated in 2002
USD 48804.75 (81%)

Project abstract
This project covers much of the training activites of the advanced development group at UNU/IIST. It is centred around the technique of using formal (precise, mathematical) methods to develop reliable software, and in particular uses the RAISE method. It consists of a number of sub-projects in which particular software development tasks are undertaken by fellows (trainees) from developing countries. Sub-projects active during 2002 are:

Multiscript
This sub-project was completed in March 2002 with the delivery of a demonstrator tool. Chris George was responsible, while the actual work was carried out by Ms Myatav Erdenechimeg from the National University of Mongolia under an SSA agreement.

Distance learning
This sub-project started in October 2002. The aim is to define the content infrastructure of a Web-based Distance Learning System using XML. Components such as program, course, lecture and exercise will be defined in terms of XML schemas, together with tools to support remote, off-line authoring of such components. Chris George is responsible, and Ms Uyanga Sambuu from Mongolia is the fellow. Completion is expected by July 2003.

RAISE tool
This sub-project is concerned with the development of open-source, portable tools to support the RAISE formal method. Chris George is responsible. In 2002 Ms. Ana Funes from Argentina completed a translator from UML class diagrams to RAISE [1], Aristides Dasso, also from Argentina, completed a translator from RAISE to the proof language PVS [2], and Abdugani Abdukhamidov from Tajikistan started work on a translator from RAISE to the database language SQL, to be completed by June 2003.

Specification-based Testing
This sub-project is concerned with the automated generation of test-cases from formal requirements specifications as well as with the associated testing theories. Bernhard K. Aichernig is responsible. The project started on the 1st of April. Li Dan from China has developed a prototype of a test-case generator for applicative RSL specifications [3]. Bernhard Aichernig worked on a theory of mutation testing based on the refinement calculus [4]. This sub-project is ongoing.

Coalgebraic Methods
This sub-project investigates the use of coalgebras as a theoretical framework for specification and verification of software. Bernhard K. Aichernig is responsible. SUN Meng from China worked on a coalgebraic semantics for UML diagrams [5][6]. Furthermore, the use of RSL as a coalgebraic specification language has been investigated [7]. The results have been incorporated in a course on Specification and Semantics of Components. Partners: Univ. of Minho, Portugal and Beijing University, China. This sub-project is ongoing.

Status and plans
Continuing.

Sources of funding
UNU/IIST

Specifying XML-based Enterprise Software

Staff responsible
Tomasz Janowski

Budgetary provision for 2002
USD 40300

Amount expended and obligated in 2002
USD 16820.09 (42%)

Project abstract
This is a new project concerned with the language XML. XML is a recently developed language for describing the structure and contents of documents and is becoming increasingly important, particularly in commerce. Tomasz Janowski was responsible. The project has worked on

  1. Developing X2Rel, an XML Relation Language with formal semantics. X2Rel is a new language to express binary relations between XML documents which may differ substantially in both their content and structure. The syntax of X2Rel is given in XML and its semantics is defined formally, using inductive and co-inductive relations based in a simple set theory. X2Rel relies on a number of XML technologies, in particular XPath, XML Schemas and XSL Transformations. As well as its use to compare XML documents directly, we envision X2Rel as a specification and run-time verification language for XML processing software. The paper presented at the Lisbon Colloquium describes the on-going development of the language. The report will be made official with the final version of the paper.

  2. A case study in developing an XML system -- a serials (journals) management system for a library -- from formal specifications [8]. Ms Arifa Bhutto and Ms Uzma Khadim from Pakistan were the fellows.

  3. Developing X2Walk, an XML Programming Language with formal semantics. X2Walk is a special-purpose language to describe XML-processing applications. It takes its name from the way the application "walks" through the document tree and modifies the structure and content of the visited nodes, in the style of the XML DOM (Document Object Model) API. X2Walk describes such applications with XML syntax, assigns them with precise formal semantics, and executes by translation to Java [report pending]. Ms Yang Hongli from China was the fellow.

Status and plans
The items listed above are complete, and this project is currently suspended following the departure of Tomasz Janowski.

Sources of funding
UNU/IIST

Formalising UML and Object Oriented Programming

Staff responsible
He Jifeng, Liu Zhiming

Budgetary provision for 2002
USD 40000

Amount expended and obligated in 2002
USD 20689.33 (52%)

Project abstract
Object-orientation is now a popular approach in software industries. UML is the de-facto standard modelling language for the development of software with broad application ranges. It covers the early development stages of requirement analysis and specification and has strong support for design and implementation.

This project investigates the general theoretical issues in object-orientation and in the formalization of UML. The overall purpose is to establish a sound theory to improve the understanding of object-oriented programming and system development, and to enhance the application of UML with a formal semantics. The theory will include a specification notation with a formal semantics and a calculus. When it is used within a software development process, such as the Rational Unified Development Process, the theory allows formal requirement specification and analysis, stepwise refinement and supports component-based development.

Main achievement includes:

Specification language
We have defined an object-oriented specification language with classes, visibility, dynamic binding, mutual recursive methods and recursion. A relational semantics is given to the language in terms of the notion of design in Hoare and He's Unifying Theories of programming. We have investigated the algebraic properties of this language. He Jifeng, Liu Zhiming from UNU/IIST and Li Xiaoshan from the University of Macau have worked on this work [9].

Refinement calculus
Further to the algebraic properties of the specification language, we have developed a refinement calculus for object-oriented design. It supports the effective use the relational model for specifying and reasoning in activities of an object system development process. He Jifeng, Liu Zhiming from UNU/IIST and Li Xiaoshan from the University of Macau have worked on this work [10].

Formalisation of UML
We have used a model of transition systems for concurrent and reactive systems to unify UML models for object-oriented requirement analysis, i.e. use-case models, conceptual class models and object-models. We also applied our specification notation to formally writing and analysing UML requirement specifications. He Jifeng, Liu Zhiming from UNU/IIST, Li Xiaoshan from the University of Macau, and Yifeng Chen from the University of Leicester (UK) have worked on this work [11][9].

Applications
We have applied our formal notation and method with two case studies: a library system and an on-line ticketing system. The latter is now being used in practice by the Macau government [12].

Training activities
We have give lectures on Object-Oriented Software Development with UML at the Almaty School in August 2002. The lecture notes are available in a form of UNU/IIST technical report [13]. A fellow from North Korea, Choe Sun Ying, is now applying UML to a distance education system.

Status and plans
Continuing. Future work includes further investigation on the refinement calculus, case studies, definition and composition of components, refinement in component-based development, concurrency, real-time, fault-tolerance.

Sources of funding
UNU/IIST

Collaborations
The University of Leicester (UK), the University of Macau, Formal Techniques for Software Development Project at UNU/IIST.

Co-design of Mixed Hardware/Software Systems

Staff responsible
He Jifeng

Budgetary provision for 2002
USD 40300

Amount expended and obligated in 2002
USD 32674.36 (81%)

Project abstract
This project attempts to provide a tool-based design technique in support of design of mixed hardware/software systems. Hardware and software co-design is a design technique which delivers computer systems comprising hardware and software components. This project covers the key development phases of co-design, including

An Algebraic Approach to VERILOG Programming
The semantics of a hardware description language is usually given in terms of how a simulator should behave. This paper adopts a different strategy by first listing a collection of equational laws expressing algebraic properties of VERILOG programs. It outlines some techniques of formal derivation of operational model and denotational presentation of the language VERILOG from its algebraic definition. This work is going to appear in the proceedings of the Lisbon Symposium'2002.

Decomposition Strategy
We propose an algebraic approach to hardware/software partitioning in VERILOG HDL. We explore a collection of algebraic laws for VERILOG programs, from which we design a set of syntax-based algebraic rules to conduct hardware/software partitioning. The co-specification language and the target hardware and software description languages are specific subsets of VERILOG , which brings forth our successful verification for the correctness of the partitioning process by algebra of VERILOG. Facilitated by VERILOG's rich features, we have also successfully studied hw/sw partitioning for environment-driven systems.
This work is jointly done by Qin Shenchao of NUS and He Jifeng, and presented in ICFEM'2002.

Completeness and Non-redundancy of Operational Presentation
Regarding operational semantics, there are three typical questions we should face: (1) By which rule can we say our operational semantics is sound. (2) How can we guarantee our operational semantics is complete. (3) How can we say there will not any redundant rules among all our transition rules.
We investigate these questions of the VERILOG's operational semantics based on its denotational model. This work is jointly done by Zhu Huibiao and Jonathan Bowen of South Bank University at London and He Jifeng, and presented in ICFEM'2002.

Limited Resource Models
Traditional system specifications always abstract from resource. However, it is unavoidable to append resource constraints in later system implementation. This work defines a hierarchy of semantic models for programs with limited resources. Each model in the hierarchy is a refinement to the one defined formally. We also investigate algebraic laws in these models. Based on that, we develop a set of program transformations to deal with the situation where resource is in shortage [14].

Status and plans
The sub-projects on Optimal Partitioning Strategy and Semantic Model for Reconfiguration are in preparation.

Sources of funding
UNU/IIST, National Natural Science Foundation of China.

Specification and Design of Hybrid Systems

Staff responsible
He Jifeng, Dang Van Hung, Liu Zhiming

Budgetary provision for 2002
USD 44000

Amount extended and obligated in 2002
USD 43103.69 (98%)

Project abstract
Hybrid systems are interactive systems of continuous devices and digital control programs. Typical examples are digital modules that control a physical environment evolving over time. The principal problem of the subject is to model them so that given a specification for the continuous component of the system, we can extract, if this is possible, from the description of the total system and the specification of the continuous component, the specification of the control program which will force the continuous device to meet its specification. We adopt the notations of DC in specifying and reasoning about real-time feature of embedded computer systems. The development process is associated with various well-known formalisms (such as CSP and state-based specification notations. Our main achievements include

Model Checking real-time constraints
Temporal Duration Properties are real-time constraint for a untimed trace of a system. We show that Temporal Duration Properties are in the class of discretisable real-time properties of Timed Automata, and give an algorithm to solve the problem based on linear programming techniques and the depth-first search method in the integral region graph of the automaton. The complexity of the algorithm is in the same class as for the solution of the reachability problem of timed automata [15]

Integrating DC and CSP
This work presents a formal description language for hybrid systems, which is an integration of CSP, which describes digital control programs, and DC for specification of continuous devices. We define primitive systems and operators over systems in DC and prove that so defined operators meet basic algebraic laws of these operators [16]. This work is presented in ICECCS'2002.

A Time Model for Circus
We propose a time model for Circus (an integration of CSP, Z, the Guarded Command Language and Specification Statements). The model is an extension to the model proposed by the unifying theories of programming and used by Circus. This work creates an abstract function that maps the timed model to the untimed one, which enables us to address most of safety properties of real-time systems in the untimed model [17]. This work is presented in ICFEM'2002.

Linking Temporal Logics
Using generic composition to unify different temporal logics and their proof methodologies. In particular, the Linear Time Temporal Logic (LTL) is linked with the Duration Calculus (DC) for specifying and reasoning about hybrid systems. This work is done joint by Chen Yifeng from Leicester University (UK) and Liu Zhiming at UNU/IIST [18].

A Framework for Development of Timed Circus Programs
This work proposes a framework for the specification, validation and development of real-time programs using Circus. The framework consists of two approaches: the first shows how to validate time requirements using the untimed model, whereas the second one deals with enriching an untimed programs by adding time constraints. We explore the considerations to be taken by each approach, and illustrate the use of each of the approaches with the help of a case study [19].

Case Study
By linking interval logics with Duration Calculus and Duration Calculus with weakly monotonic time, we develop a formal reasoning technique for deriving a timed OCCAM program from a Duration Calculus specification. We apply this technique to develop a control program for a double tank system. We also built a DC model for real-time databases with periodic transition systems [20].

Status and plans
A sub-project on A Complete Verification System for Timed RSL is in preparation. We have invited Prof Wang Yi and Dr Michael Pont to visit us next year.

Sources of funding
UNU/IIST

Curriculum for Formal Software Development

Budgetary provision for 2002
USD 60000

Amount extended and obligated in 2002
USD 3913.09 (7%)

There were no curriculum development fellows in 2002.

Development of Computer Science Departments in Developing Countries

Staff responsible
Dang Van Hung

Budgetary provision for 2002
USD 101000

Amount expended and obligated in 2002
USD 67167.92 (66%)

Project abstract

This project aims to strengthen all aspects of computer science teaching in universities in developing countries.

Under the project, we are trying to arrange for (generally young) computer science lecturers or professors from universities in developing countries to learn new courses at partner universities in industrialised countries for one semester as a fellow, 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. With our arrangement, the partner universities provide the use of their facilities free of charge and in particular without payment of tuition fees. 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.

Status of implementation
In the year 2002, 13 lecturers from 9 universities in 5 developing countries have been trained under the project. See appendix  * for the complete list of the fellowships by the project in 2002.

Partner Institutions in Developing Countries
So far 19 institutions in developing countries have benefited from this project. They are (with currently active ones marked by *):
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
Posts and Telecommunications Institute of Technology, Ha Tay, Vietnam
University of Dschang, Cameroon
University of Yaoundé I, Yaoundé, Cameroon
University of Buea, Buea, Cameroon
University of Lagos, Lagos, Nigeria
* University of Ibadan, Ibadan, Nigeria
Chittagong University, Bangladesh
* Obafemi Awolowo University, Ile-Ife, Nigeria
* Kathmandu University, Nepal
* Gui Zhou University, Gui Yang, China
Wuhan University of Technology, Wuhan, China
* Xian University of Post and Telecommunications, Xian, China
* Nanjing University, Nanjing, China
* Technological University of Tajikistan, Dushanbe, Tajikistan

Partner Institutions in Industrialised Countries
11 institutions in industrial countries have been involved in training lecturers from developing countries in this project. They are (with currently active ones marked by *):
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
* University of Calgary, Calgary, Canada
* Swinburne University of Technology, Australia
* South Bank University, London, UK
* National University of Singapore
* Kwangju Institute of Science and Technology, South Korea

Status and plans
Currently ongoing.

Sources of funding
UNU/IIST and Partner Institutions in Industrialised Countries.

IT Training Courses and Schools in Developing Countries

Staff responsible
Chris George, He Jifeng, Tomasz Janowski, Liu Zhiming, and Dang Van Hung

Budgetary provision for 2002
USD 95800

Amount expended and obligated in 2002
USD 120709.31 (126%)

Project abstract

Under the project IT Training Courses and Schools in Developing Countries, UNU/IIST aims to disseminate sound modern approaches to software development in developing countries. IT Schools and Courses are organised jointly with host institutions. The courses are in two categories: formal methods and software engineering and system development.

Formal (mathematical) methods are being increasingly used in Europe and the USA and are starting to be important in developing countries. In particular, formal methods are becoming advised or even mandatory for the development of safety-critical and defence software.

The aim of the courses is to propagate research into and application of formal software development techniques, with the hope that developing countries can accelerate their progress in being self sufficient in software technology, and even become providers of services and products elsewhere.

The courses on software engineering and system development aim to introduce the advanced methods, techniques and tools that are widely used in industries for software development. They cover project management, object-oriented software development with UML and the Rational Unified Development Process Good management, Component-Based Software Development, and Software Testing. These topics are often taught together with the those on formal methods so that the participants can integrate formal methods and practical software engineering in their further study and practice.

IT Schools, however, have a wide range of topics in computer science not just in software technology, and consist of several courses. Courses in a school are taught by experts invited from universities and industries as well, not just by UNU/IIST staff.

Status of implementation

In 2002, together with their host institutions, UNU/IIST organised 5 training schools in India, Kazakhstan, the Lebanon, Nigeria and Vietnam. About 250 participants from 20 countries attended the schools. See appendix * for details.

UNU/IIST staff presented:

See appendix * for the list of courses.

Status and plans
Currently ongoing.

Sources of funding
Schools and courses are organised on a cost-sharing basis between UNU/IIST and the host institution. We have tried in many cases to get local UNDP support, but without success.

IT Projects in Macao

Staff responsible
Fu Guoyi, Tang Xinbei, Edward Iong (all fellows). Fu Guoyi was responsible for this project until he left UNU/IIST in January 2002 (to start a PhD at the University of Canterbury, UK). Tang Xinbei left in August 2002 (also to start a PhD at the University of Canterbury).

Budgetary provision for 2002
USD 44250

Amount expended and obligated in 2002
USD 14854.92 (34%)

Project abstract
The Information Network Centre of Macao (INCoM) 2002 is a joint project, (INCoM), between the Macao Foundation (MF) and UNU/IIST. Main tasks were:

  1. Expansion and Maintenance of Macao Virtual Library System. According to the plan, over 500 local publications and 20 magazines are targeted for full-text on-line publishing. 316 publications have now been processed and made available on-line: new books continue to be added. A new improved searchable section of Academic Forum was added to the site, which users can search by article, author name, category, source, and abstract.

  2. Proposed intranet design for the MF. MF consists of headquarters, a financial department, an institute and the UNESCO Centre of Macao, which are located separately. We have proposed an intranet design using VPN and ADSL.

  3. Expanding the web sites of the MF and UNESCO Centre of Macao. A whole new MF web site is complete and is currently awaiting for approval to be put on line: this should happen early in 2003.

  4. Building a web site for the Macao Science Centre A new web site will be built for Macao Science Centre. Phase 1 was finished and on line in November 2002. Phases 2 and 3 will be implemented when the Macao Science Centre is operational in 4 years time.

  5. Maintenance and technical support.

Status and plans
INCoM 2002, which started on 1 November 2001, was completed at the end of October 2002. A further project, INCoM 2003, to maintain and continue development started on 1 November 2002. An additional project to develop an on-line database for the Subsidy Department of the MF is currently being considered.

Sources of funding
Macao Foundation (USD 44250)
Status of implementation of project activities
Executive SummaryExecutive Summary
Top Top
Postgraduate training/teaching activities Postgraduate training/teaching activities