| | | Annual Report 2001 | |
Since the establishment of UNU/IIST, the research group has centred its effort on theories, techniques and tool-based design of real-time systems. In 2001, we are working on the following subjects
Staff responsible
Fellowships, Courses and Conferences
In 2001, under this project 10 fellows from 6 countries were trained, and 4 off-shore courses and 2 training schools were delivered in 4 countries. The project engaged in the organisation of 8th Asia-Pacific Software Engineering Conference in Macau.
Publications
14 technical reports were produced by the project in 2001. They are [1][2][3][4][5][6][7][8][9][10][11][12][13][14]. A total of 14 papers has been presented and published in the proceedings of international conferences or in journals during the year.
Details of Project Achievements
We researched into and obtained interesting results on the following subjects.
Prefix and Projection onto State in Duration Calculus
We study a new operator of projection onto state and the prefix
operator in the extension of Duration Calculus by quantifiers over
state and a polyadic least fixed point operator. We give
comprehensive lists of axioms and rules which enable deduction in the
extension of µHDC by the new operators. Our axioms can be used as
reduction rules which enable the elimination of the new operator from
the formulas which commence in specification of the proposed kind.
This entails that there is a big fragment of µHDC where the prefix
and projection-onto-state operators can be regarded as derived
operators and the decidability of certain sub-fragments of this big
fragment is preserved in the presence of the new operators.
A DC-based Approach to Refinement of Real-time Systems
We introduce a notion of timed transition diagrams for modelling
real-time systems. The semantics of a timed transition diagram is
defined to be a DC formula. We propose a method for verification of
properties of a timed transition diagram, and for proving the
refinement between timed transition diagrams by simply checking the
simulation of simple step-transitions together with the calculation of
the time bounds of paths of transitions.
A Formal Model for Channel Allocation in a Distributed Computing
System
The wireless channels are the most important resources in a
mobile computing system. The possibility of reuse of wireless
channels in different cells subject to satisfying the reuse constraint
is the main concern for optimising channel usage. We present a
formal model for channel allocation in a distributed mobile computing
system using Duration Calculus. We propose a new distributed dynamic
channel allocation algorithm based on the formal model. The proposed
algorithm attempts to bring in the best features of the
permission-based and token-based principles.
A Prolog Prototype for the Synthesis of Verilog
This work develops a prototype for an algebraic synthesis of Verilog.
The implementation language adopted is Prolog. The integration of this
system with an Occam hardware compiler is also addressed.
Interface Design for Mixed Hardware/Software Systems
We have investigated Bus Extended Technology and its application in
design of communication interface between hardware and software
components in the embedded systems. We treat both synchronous
mechanism and asynchronous interface, and as well as their converter,
and work out their specification in Verilog behaviour modules, and
corresponding physical devices.
Formalising the Use of UML in Requirement Analysis
We have developed a method to support the formal use of UML in
object-oriented software development. The method includes formal
definitions of the modelling elements in UML, which can be used to
relate the different UML models used at different stages during
the software development process. It intends to support step-wise
refinement and component-based development in building models. We
have also applied the formalisation to a library system as a case
study. This illustrates how the approach supports a use case-driven
and incremental development in building models for requirement
analysis.
A Behavioral Model for Object-oriented Programming
We have
provided a semantics for an object-oriented language with classes,
visibility, dynamic binding, mutual recursive methods and recursion.
Our framework identifies both class declarations and commands as
design. All the programming constructs of our language are defined in
exactly the same way as their counterparts in the imperative
programming languages. This makes the approach more accessible to
users who are already familiar with the existing imperative languages
and also enables the use of tools and methods of verification and
refinement developed for these languages. Furthermore, the algebraic
laws developed for the imperative languages remain applicable in
designing object-oriented programs.
Refinement and Specification of the Spatial Data Type with the
B-toolkit
We specify realms, an underlying structure for
spatial data types, in B language. Then, we use the B-toolkit to formally
verify the algorithms for modifying a realm such as inserting or
deleting an element.
This project aims to develop a method to support the formal use of UML in object-oriented software development.
This project attempts to provide a tool-based design technique in support of mixed hardware/software systems.
We adopt the notations of DC in specifying and reasoning about real-time features of embedded computer systems. The development process is associated with various well-known formalisms (such as CSP and state-based specification notations).
The activities of the Formal Techniques for Software Development Project of UNU/IIST are loosely grouped by the idea of "Software for Infrastructures", and this notion should be clarified.
According to the World Bank, "infrastructure" is an umbrella term for many activities referred to as "social overhead capital" by some development economists, and encompasses activities that share technical and economic features (such as economies of scale and spill-overs from users to non-users). UNU/IIST takes a more technical view, and sees infrastructures as concerned with supporting other systems or activities. Software for infrastructures is likely to be distributed and concerned in particular with supporting communication of data, people and/or materials. Hence issues of openness, timeliness, security, lack of corruption and resilience are often important.
UNU/IIST pursues this project in order to fulfil its Charter:
In February 2002 Springer-Verlag will publish a book of case studies developed in this project over the past seven years. This book will contain the complete specifications in the RAISE Specification Language, plus the RAISE tools developed at UNU/IIST, also in this project. Please refer to the UNU/IIST ftp website for details. The book is edited by Hung Dang Van, Chris George, Tomasz Janowski and Richard Moore.
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.
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.
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.
Formal techniques have two particular characteristics that allow one to deal successfully with large and complex systems.
At a particular stage in development one can abstract away from some details while concentrating on others.
Formal systems allow one to prove properties of systems, anything from full correctness to particular properties (such as safety properties). Full proof of correctness is beyond the state of the art at present; rigour allows one to use (and document) informal arguments which can be backed up formally if required. The amount of rigour will vary between projects and between parts of a single project; rigour gives flexibility.
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
This project is largely complete, but Myatav Erdenechimeg is completing a demonstrator tool.
There is also a prospect of licensing a Mongolian font, developed as part of this project, to Microsoft.
Myatav Erdenechimeg, previously a Fellow from NUM (September 1995 - August 1996), now working under an SSA agreement.
Software Reuse
Raoudha Beltaifa, Campus Universitaire La Manouba, Tunis, Tunisia, 1 July 2000 - 31 March 2001
Engineering Design Database
Intelligent design support will involve activities like finding suitable design cases to use for the current problem, and checking design rules.
Work on the initial design of the database was done during 1999-2000. In a second phase of the project, running 2000-2001 the emphasis was shifted to supporting interactive, collaborative design using a "whiteboard". The process of concurrent control for collaborative design was defined, together with protocols and locking mechanisms to support version control of shared information. A prototype was implemented to illustrate the locking mechanism.
Wang Yanjie, Southwest Jiaotong University, , 10 September 2000 - 9 April 2001
Wang Zhuo, Southwest Jiaotong University, , 10 September 2000 - 9 April 2001
Enterprise Modelling, Analysis and Implementation
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-in-time production, concepts which are increasingly adopted by manufacturing organisations worldwide to address challenges of global competition and unstable market conditions.
Methods and Tools for Building Software from Components
This practice saves on time and the cost of development and results in products which are easier to upgrade and maintain. But it also creates a host of basic but technically challenging questions and problems: What in essence is a reusable component? What is the semantics of a component? How can we abstract away from the details of the semantics in order to decide suitability of a component for the design? What is the "best" abstraction level for this? Given two descriptions of one component (a specification and an implementation) how can we make sure they are consistent? How do we check consistency if the implementation details are unavailable (because they are proprietary, remote or even non-existent)? How can we formulate a request for a component? How can we choose one? How can we assemble components and calculate the semantics of the composition? To what extent can we adapt a component which fits only partly into our design? How can we obtain components? How can we store them for effective retrieval? How can we postpone "assembly" till run-time, resulting in software which evolves with its environment? What is the semantics of this? And so on.
The goal of the project is to study formally-based methods for software design from pre-existing components, including but not limited to the issues above. In particular, we look for a common ground to use together formal methods (to predict the result of putting components together) and fault-tolerance (to detect and recover from errors of individual components at run-time).
This work is meant as a pilot study for a new project "Specifying XML-Based Enterprise Software" which is going to start in 2002 as a follow-up for both MIICI and CASINO.
George Uzohue Oparah, Broad Bank of Nigeria, Lagos, Nigeria, 25 June 2001 - 26 October 2001
Distance Learning
Distance learning also allows a more student-centred approach, with students able to tailor their own programmes of study from the material available. To support this, there must be a Course Structure Model (CSM) that allows students to plan their own programmes, while fulfilling the requirements for recognised qualifications. The CSM must also satisfy requirements for accessibility, interoperability, reusability and durability.
Wang Jinsong, Information Technology Center, Tianjin Institute of
Technology, P.R. China
Wang Zheming, Information Technology Center, Tianjin Institute of
Technology, P.R. China
Geographical Information Systems
Li Danning, Guizhou Academy of Sciences, Guiyang, Guizhou, P.R.China
There are several aspects of the project:
RAISE Tools
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.
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 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 translators to Standard ML (written by Ke Wei, Chinese Academy of Sciences, Beijing) and to C++ (written by Ahn Yong Jun, Kim Il Sung University, Pyongyang, DPR Korea) were added.
During 2001:
Aristides Dasso, University of San Luis, San Luis, Argentina, 1
September 2001 - 31 May 2002
Ms Ana Funes, , University of San Luis, San Luis, Argentina, 1
September 2001 - 31 May 2002
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
University of San Luis, San Luis, Argentina
All the material, both UNU/IIST's and that developed by Fellows [19] is publicly available on UNU/IIST's ftp site.
Irshad Kamal Khan, Chittagong University, 12
February - 6 October 2001
Gafurov Davrondjon, Technological University of Tajikistan, 1 July - 14 December 2001
Yang Hongli, Xian University of Post and Telecommunications, 27
September - 29 June 2002
Chittagong University, Chittagong, Bangladesh
Technological University of Tajikistan, Dushanbe,
Tajikistan
Xian University of Post and Telecommunications, Xian,
China
The Computer Science Department Development Project aiming to strengthen all aspects of computer science teaching in universities in developing countries is going on well in the year 2001. More and more universities become partners of the projects. Four more universities in the developed countries have agreed to train our fellows. They are Kwangju Institute of Science and Technology, South Korea, the School of Information Technology, Swinburne University of Technology, Swinburne, Australia, University of Calgary, Canada, and National University of Singapore. Each of them is willing to accept three lecturers from developing countries for one semester each time.
In the year 2001, from 7 countries, a total of 10 fellows has been trained in this project, and another two fellows have been accepted to study at the National University of Singapore. They are listed as:
Reports from the fellows when they finish their fellowship in the project reveal that they are happy with the fellowship and think that their department will benefit a lot from the project.
| | | Annual Report 2001 | |