 | Executive Summary |
| 
| Top |
| 
| Postgraduate training/teaching activities |
|
| Status of implementation of project activities |
Status of implementation of project activities
- Staff responsible
- Chris George, Bernhard K. Aichernig
- Budgetary provision for 2002-3
- USD 134000
- Amount expended and obligated by 15 October
- USD 128092 (96%)
- Project abstract
- This project covers much of the training
activities 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
2003 are:
- 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. In January 2003, Li Dan from
China finished his work on a prototype for generating test-cases
from RSL specifications [1]. Gabriel Adenawo
from Nigeria worked on a testing theory for the Unified Theories of
Programming. Bernhard Aichernig continued his
research on the foundations of specification-based testing resulting
in 4 external publications (see appendix *).
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 [2] and on a semantic model for
components [3][4]. Furthermore, the use
of RSL as a coalgebraic specification language has been
investigated [5]. The results of an earlier report
on this subject [5] have been incorporated in a
course on Specification and Semantics of
Components held as part of the summer school in Neuquen, Argentina.
Partners: Univ. of Minho, Portugal and Beijing University, China.
This sub-project is ongoing.
- OpenCert
- On October 15, we have submitted a project proposal
for the 2nd call of the European Framework VI program. Bernhard
K. Aichernig is the coordinator of this STREP project. The full
title of the project is OpenCert - Methods and Tools for Open
Source Software Certification. The goal of the OpenCert project
is to strengthen the role of open source software in the European IT
sector. Open source software is increasingly important for public
and industrial organisations, but its quality can be very hard to
measure. This makes its use a risk. This risk could be
substantially reduced if there were appropriate standards, supported
by analysis tools, for certifying such software. Defining such
standards, and developing an online infrastructure in which
independently developed analysis tools can be inserted, is the main
aim of the OpenCert project. A second, long-term, goal is the
creation of an international certification authority for open source
software, ideally under the umbrella of the United Nations.
To achieve its objectives OpenCert brings together techniques for
certification, program understanding, validation, and verification,
culminating in a framework for monitoring, evaluating, and
certifying open source software products. While not intended to
directly change the process of open source development, some effect
on that process is likely as certification becomes common.
The partners are UNU-IIST (UN), Delft University of Technology (The
Netherlands), Hewlett Packard (Italy), Sidereus (Portugal), Software
Improvement Group (The Netherlands), TU Graz (Austria), TÜV
(Germany), University of Minho (Portugal).
- Distance learning
- This sub-project started in October 2002.
The aim was to define the content infrastructure of a Web-based
Distance Learning System using XML. Components such as program,
course, lecture and exercise have been defined in terms of XML
schemas, and a start has been made on developing tools to support
remote, off-line authoring of such components. Chris George is
responsible, and Ms Uyanga Sambuu from Mongolia is the fellow.
Completion was expected by July 2003, but the project was affected
by the SARS outbreak. Ms Sambuu had to return early to Mongolia,
and will come back to UNU-IIST to complete the project in 2004.
- 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 2003 Abdugani Abdukhamidov from Tajikistan
completed work on a translator from RAISE to the database language
SQL, an extension to the existing translator to C++ [6].
- Status and plans
- Continuing.
- Sources of funding
- UNU-IIST
There are two other projects undertaken by the development group which
were inactive in 2003 but were originally budgeted to run:
- Developing Software Specifications from Business Models
- was
led
by Tomasz Janowski, who left UNU/IIST in 2002. This project had a
budget of USD 89300 for the biennium, with an expenditure of USD
25225 (28%).
- Curriculum for Formal Software Development
- This project
provided 3-4 month fellowships for university lecturers to learn to
teach formal methods. It has been superseded by the Development of
Computer Science Departments in Developing Countries
(section *). The budget was USD 131000, and
expenditure USD 3913 (3%).
- Staff responsible
- He Jifeng, Liu Zhiming
- Budgetary provision for 2002-3
- USD 89000
- Amount expended and obligated by 15 October
- USD 92214 (104%)
- 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 formalisation 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 a subset 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 (RUP), the theory allows formal
requirement specification and analysis, stepwise refinement and
supports component-based development.
Main achievements include:
- Specification language
- We have extended the specification
language for object-oriented system (OOL) developed in
2002 [7] with reference types. The calculus
(COOL) for OOL has been re-investigated as well. A relational
semantics is given to the language in terms of the notion of design in Hoare and He's Unifying Theories of
Programming [8]. We have investigated the algebraic
properties of this language. He Jifeng, Liu Zhiming from UNU-IIST,
and Li Xiaoshan from the University of Macao have worked on
this [9].
- Formalisation of UML
- We have applied OOL and COOL to specify
and reasoning about UML models of
requirements [10], and to unify different views
of UML models to reason about their
consistency [11]. He Jifeng, Liu Zhiming from
UNU-IIST, Li Xiaoshan from the University of Macao, Yifeng Chen
from the University of Leicester (UK), and two fellows, Liu Jing
and Yang Jing, from China have worked on this [10][11].
- Component-Based development
- We have extended COOL to the
specification, composition and verification of component
software [12]. We also organised the first workshop on Formal
Aspects of Component Software (FACS03) and the proceedings are edited as a UNU-IIST
technical report [13].
- Papers and Presentations
- in addition to the publications
referred to above, Liu Zhiming gave a 2-hour tutorial on COOL at the
1st IEEE International Conference on Software and Formal Methods
(SEFM2003: http://www.itee.qu.edu.au/SEFM03), Brisbane, 21-26
September 2003, and a seminar at the School of Computer Science of
the University of Birmingham (UK) on 17 September, 2003. The
following papers have been submitted:
- Linking UML Models of Design and Requirement, to appear in Proc. ASWEC2004.
- A Formal Semantics of UML Sequence Diagrams, to appear in Proc. ASWEC2004.
- Contract-oriented development of component systems,
submitted to MCP2004.
- Towards an integration of a formal method with Rational
Unified Process, to appear as invited contribution of a chapter for an
edited book on Software Evolution with UML and XML.
- A Design Calculus for OO Software Development, to be presented as an invited lecture at FMCO04.
- Formal support to incremental development, to appear in the
proceedings of IRMA 2004.
- Training activities
- In 2003, we gave two courses on
Object-Oriented Software Development with UML in Hanoi, Vietnam
and a training school in Guiyang, China. (See
appendix *). The lecture notes are available in the
form of a UNU-IIST technical report [14]. Three
fellows, Liu Jing, Yang Jing, Long Quan from China, and Bhim
Upadhyaya from Nepal are now working on the project.
- Status and plans
- We will continue this project under the
new project Formal Methods for Object and Component Systems
(FMOC). We will make further investigations into the semantics of OO
and component-based programming, and extend our specification
language to cover more aspects such as exceptions. We will carry
on our work on the refinement calculus with respect to the support
of iterative and incremental programming. A major task in the
follow-up research is to test the theory with case studies. We
We will work on the extension of the theory to deal with
concurrency, real-time, and fault-tolerance. We will start to look at tool development too.
- Sources of funding
- UNU-IIST
- Collaborations
- We have close collaboration with the University
of Leicester (UK) and the University of Macau. We will seek more
collaborations with research groups, such as Prof. Anders Ravn's
group at Aalborg, Denmark, Prof. Mathai Joseph's group at the Tata
Research and Development Centre in Pune, India, and possibly some
institutes in China.
- Staff responsible
- He Jifeng
- Budgetary provision for 2002-3
- USD 89300
- Amount expended and obligated by 15 October
- USD 50931 (57%)
- Project abstract
-
Hardware and software co-design is a design technique which delivers
computer systems comprising hardware and software components.
This project attempts to provides a tool-based design technique
in support
of the design of hardware/software mixed systems, and
covers the following development phases
- Semantic Issues
- Link the Operational Semantics with the Algebraic Semantics
- A Resource-oriented Model for HW/SW Systems
- Algorithms
- Optimal Partitioning Algorithm
- Performance Estimator
- Resource-oriented Program Transformer
- Optimal Partitioning Strategy
- Computer aided hardware/software
partitioning is one of the key challenges in hardware/software
co-design. We propose a new approach to hardware/software
partitioning for a synchronous communication model. In this approach,
we transform the partitioning into a reachability problem in timed
automata. By means of an optimal reachability algorithm, an optimal
result can be obtained in terms of limited resources in hardware.
We developed two algorithms to explore the dependency relation among
processes in the initial specification, and a scheduling algorithm
to improve the synchronous communication efficiency further after
the partitioning stage.
- Status and plans
- The sub-projects on
the implementation of Optimal Partitioning Strategy and Semantic
Model for Reconfiguration
are ongoing.
- Sources of funding
- UNU-IIST, National Natural Science Foundation
of China, the 973 Project 2002CB312001 of the Ministry of Science and
Technology
of China.
- Staff responsible
- Dang Van Hung
- Budgetary provision for 2002-3
- USD 99000
- Amount extended and obligated by 15 October
- USD 50819 (51%)
- 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 Duration Calculus (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, OCCAM, and state-based specification notations). Our main
achievements include
- A relatively complete axiomatisation of DC with projection onto state
-
We give a relatively complete axiomatisation of DC with projection onto
state. This is a useful technique for the refinement of real-time hybrid
systems using Duration Calculus. This is a generalisation and revision
of our techniques developed
earlier [15][16][17] for a journal
publication.
- Model-checking interval based properties
-
A tool is developed based on the Spin model
checking system to verify the proposed general satisfaction relation
for a decidable subset of Discrete Time Duration
Calculus [18]. We have also developed a
discretisation technique for Linear Duration Calculus Invariants (a
report is under preparation).
- Sources of funding
- UNU-IIST
- Staff responsible
- Dang Van Hung
- Budgetary provision for 2002-3
- USD 224000
- Amount expended and obligated by 15 October
- USD 103797 (46%)
- 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 2003, 6 lecturers from 6
universities in 4 developing countries have been trained under the
project. See appendix * for the
complete list of the fellowships by the project in 2003. This
figure is less than planned for two reasons. First, two North
Korean fellows were not able to obtain visas to take up their
fellowships. Secondly, SARS prevented NUS in Singapore from
receiving our fellows.
- 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
* Northwest University, Xian, China
* National University of Laos
* Nong Lam University, HoChiMinh City, Vietnam
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.
- Staff responsible
- Chris George, He Jifeng, Bernhard
K. Aichernig, Dang Van Hung, and Liu Zhiming,
- Budgetary provision for 2002-3
- USD 203800
- Amount expended and obligated by 15 October
- USD 152353 (75%)
- 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, Component-Based Software
Development, and Software Testing. These topics are often taught
together with 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 2003, together with their host institutions, UNU-IIST organised
or sponsored 4 training schools in Argentina, Tunisia,
Vietnam, and China. Another in Zhengzhou, China had to be postponed
to year 2004
due to the outbreak of SARS. About 170 participants from
25 countries attended the schools. See
appendix * for details.
UNU-IIST staff presented:
- One course on component software as part of a school in
Argentina.
- Two courses on OO software development with UML in Hanoi,
Vietnam and as part of a school in Guiyang, China.
- Two courses on model checking techniques in
Hanoi, Vietnam, and in Dakar, Senegal.
- One course on fault-tolerant and real-time systems in an
IFIP 2.3 School in Tunis.
- One course on formal methods in software development in
Peru.
- Two courses on unifying theories of programming in Hanoi,
Vietnam and as part of a school in Guiyang, China.
- One course on the B Language and method in as part of a school in
Guiyang, China.
- One course on RAISE applications as part of a school in Guiyang,
China.
- One course on software testing in Dakar, Senegal.
- One course on software project management in PyongYang, DPR
Korea.
- One course on formal methods in software development in Lanzhou, China.
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.
There are several projects funded by the Macao Foundation and/or the
Government of Macao, our host community.
The Government of Macao is making available funds for science and
technology research and development projects. We have formed a
consortium with a government department responsible for implementing
e-government in Macao, the University of Macau, and an institute
INESC-Macau, to propose a project to develop e-government services in
Macao, and to develop the capacity of the government to continue to
develop them in the future. We expect this proposal to succeed, given
the very positive response we have so far had from the government.
We intend to use the results of this project in collaborating with
institutions in developing countries that are interested in developing
similar software. We also expect one or two research assistants from
developing countries to work on the project, and take their expertise
home again.
Expected results are a domain model for e-government
in Macao, training of government employees in the relevant techniques,
some demonstrator applications, and some standard open source packages
that can be used elsewhere.
We will involve Tomasz Janowski, a former Research Fellow of
UNU-IIST, as the project manager. He spent 3 months as a visitor to
UNU-IIST in the summer of 2003, spending part of his time preparing for the
Macao project, and part preparing a course on XML, a new and
increasingly standard technology for such applications. This course
was presented publicly in UNU-IIST at the end of September and
attracted some 40 attendees, mostly practising software engineers from
Macao companies and government departments.
An agreement between UNU-IIST and the Macao Foundation on carrying out
and funding the e-Macao project was drawn up by the government and
signed by UNU-IIST at the end of the year.
It was suggested at the CONDIR in March 2003 that we should organise a
UNU-wide on-line repository of research materials, which we would hope
to extend later to other UN bodies. This would be a convenient source
for researchers, serve as a means of protecting the data over the long
term, and add to the visibility of the UNU. UNU-IIST offered to
develop the repository, and has since reached agreement with the Macao
Foundation that they will cover half the cost. The requirements for the
repository are currently being discussed, and work started
in December 2003. The person in charge of technical development is
Frank Wong, supervised by the system administrator and by a member
of the academic staff.
There were a group of projects that we ran on behalf of the Macao
Foundation.
- Staff responsible
- Edward Iong
- Budgetary provision for 2003
- USD 44250
- Amount expended and obligated by 15 October
- USD 42840 (97%)
- Project abstract
- INCoM was a joint project between the Macao
Foundation (MF) and UNU-IIST. Main tasks were:
- 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. Most
have now been processed and made available on-line: new books
continue to be added. A search system is also included.
- Intranet design for the MF.
MF consists of a headquarters, a financial department, an
institute and the UNESCO Centre of Macao, which are located
separately. We have designed an intranet using VPN and ADSL
and much of the installation is done.
- Expanding the web sites of the MF and UNESCO Centre of
Macao. A whole new MF web site was put on line early in 2003.
- Building a web site for the Macao Science Centre.
A new web site has been designed and a preliminary version put on
line.
- Maintenance and technical support.
- Status and plans
- INCoM 2003, which started on 1 November 2002,
was completed at the end of October 2003. By that time the person
responsible had been recruited to be employed directly by the MF,
and the work moved with him. This project will therefore not be
repeated. The two servers used by INCoM continue to be co-located
with UNU-IIST's web server at the premises of the local ISP, and
UNU-IIST and the MF will continue to share the cost of the rack
space and connection.
- Sources of funding
- Macao Foundation
| Status of implementation of project activities |
| Executive Summary |
| |
| Top |
| |
| Postgraduate training/teaching activities |
|