| | | Annual Report 1996 | |
UNU/IIST views its six major lines of programmatic activities as one "Programme". This Programme is decomposed into a number of individually managed and staffed projects:
All projects are designed to serve the public and private sector institutions of developing countries by increasing self-reliance in the following three areas:
These projects are closely interlinked. All UNU/IIST research, as well as advanced development projects, have a training component and involve one or more fellows.
Likewise, the post-graduate courses and the seminars and events sponsored or organized by UNU/IIST fit into UNU/IIST's research and advanced development agenda.
UNU/IIST's emphasis is on research into, advanced development of and training in methods for the development of Real-time, Reactive, Hybrid and Safety Critical Systems and in 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.
Real-time and reactive systems (including safety criticality) form an important class of today's computer controlled systems. The DeTfoRS research project is concerned with formal design of safety critical, real-time, reactive and hybrid systems. Such research has been rapidly expanding in the 1990s. UNU/IIST -- as one of the main research forces in developing and applying Duration Calculus (abbreviated as DC) -- has become an acknowledged leader in this field.
100% funded by UNU/IIST. Expenditures until end 1996 were:
The following UNU/IIST staff, Fellows and visitors have been working on the project in 1996:
Staff
Fellows
During all of 1996, UNU/IIST staff and fellows, with visitors and collaborators, have studied DC-based techniques for specification, refinement and verification of real-time, reactive and hybrid systems, and also tools to support the techniques. The achievements include:
The research achievements in this period resulted in 15 papers. Among them 9 papers have been presented (two as invited lectures) or accepted by professional conferences. (In this period, one earlier UNU/IIST report has been presented in a conference as an invited lecture, and two have been published or accepted by journals.)
The UNU/IIST DeTfoRS research in the area of real-time systems has trained 18 fellows. The impact is high. Some of the seconding institutions have taken up the UNU/IIST research agenda, e.g. in India and in China. UNU/IIST will therefore continue this research.
The main DeTfoRS research topics in future would be:
This research tries to develop and integrate existing techniques for specification, refinement and verification of real-time programs, and hence to provide real-time programming with methodology as well as platforms. The specification language is Duration Calculus or a subset of it, and the implementation languages can be communication oriented or shared variable oriented. Intermediate languages can be real-time automata or an executable subset of DC. Both deduction tools and model checking tools will be investigated. Case studies will be carried out, for instance, in the area of resource scheduling and circuit design.
We intend to use the formal notation, proposed in [4], to describe various components of hybrid systems and their interfaces, such as actuator, sensor, holder, A/D and D/A 2 converters, and conventional as well as hybrid controls, e.g. PID 3 control, controlled switch, controlled jump and autonomous jump. Since the semantics of the formal notation is given as DC formulas, verification laws for hybrid systems can be developed with DC. Tools for assisting proofs involving continuous mathematics has existed (see Bruno Dutertre [13]), and can also be built on the top of the proof tool for the first order interval logic [12], which supports formalization of continuous mathematics.
We will pursue research on fundamental issues of interval logics and DC, such as expressiveness, completeness, decidability etc. That research can strengthen power of the DC logic, and provide algorithms for building tools.
It is time to write a text book for DC and its applications in the design of the real-time systems. This book can help UNU/IIST's training objective in this area. Springer-Verlag has approached Zhou Chaochen and his collaborator, Michael R. Hansen at the Technical University of Denmark, with this in mind.
We refer, in general, to section 6.4 and appendix A.
As UNU/IIST has trained 18 Fellows in this area, and some of the seconding institutions in developing countries have taken up UNU/IIST's DeTfoRS research agenda, UNU/IIST will conduct off-shore research in the DeTfoRS area. In other words, UNU/IIST will support former Fellows and visitors to organize, in their home countries, groups, which do research according to the UNU/IIST agenda. UNU/IIST could subsidize their research resources, to the order of typically US$5,000 annually for say two groups of 2-5 persons, and also finance visits to/from UNU/IIST. In this way, UNU/IIST can pursue technical dissemination to more people via its visitors trained Fellows.
Staff: Kees Middelburg
Fellows:
It is planned that some of the promising participants of the second part are offered UNU/IIST sponsored PhD fellowships at Utrecht University after the return of Kees Middelburg to The Netherlands at the end of 1997.
Until recently, the field of telecommunications has focused on technology relevant to switching and transmission. This technology was used to provide the only telecommunication service offered, namely the "Plain Old Telephone Service" (POTS). Fast technological developments have made it possible to provide many new services with all kinds of additional features. Higher level services are realized by protocols using lower level services, and telecommunications systems have become rather extensive and complex. Therefore the focus is now changing over to the telecommunication services.
In telecommunications, SDL [17] is by far the most widely used specification language. The first version of SDL became a recommendation of the International Telecommunications Union (ITU) in 1976. It originated from an informal graphical description technique already commonly used in the telecommunications field at the time of the first computer controlled telephone switches. Since then it has been extended several times, and the recent revised version of SDL became a recommendation in 1992. In the telecommunications field, SDL has survived Estelle [18] and LOTOS [19], and it will presumably still be used for a long time.
The UNU/IIST research project DesCaRTeS, is focusing attention on formal techniques, and tools in support of them, to complement SDL for more rigorous approaches to software development in telecommunications.
Initial specification of telecommunication services is usually done with the intention to analyze the behavioural properties of these services and thus to validate the initial specifications. During their design, telecommunication services are increasingly described at different levels of abstraction. This gives rise to a growing need to verify that the properties represented by one specification are preserved in another, more concrete, specification and thus to justify design steps. The current situation is that there are only means for limited analysis and no means at all for formal verification. Prerequisites for advanced analysis and formal verification is a somewhat simplified version of SDL and an adequate semantics for it. Only after that, possibilities for advanced analysis can be elaborated and proof rules for formal verification devised.
DesCaRTeS aims at solving basic technical problems which telecommunications manufacturers and operators encounter in their current practice as developers and providers of telecommunication services. It does so by enhancing the possibilities for advanced analysis of the behavioural properties of services described in SDL, including time related properties. It thus adds rules of reasoning to SDL and turns it into a fully-fledged design calculus. This enables design steps to be justified by formal verification if appropriate.
The Advanced Development Projects of UNU/IIST are all loosely grouped by the idea of `Software for Infrastructures', and we first need to clarify this notion.
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). We take a more technical view, and see 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. The Software for Infrastructures orientation represents a major, novel and very effective research and advanced development initiative. UNU/IIST is very proud of its contributions so far!
UNU/IIST pursues advanced development projects in order to fulfill its Charter:
UNU/IIST is thereby contributing to the UNU's Medium Term Programme III.
So why do we consider infrastructure software to be a suitable area for UNU/IIST to be engaged in?
There is a further research element in that we would look to characterize the notion of "infrastructure" more precisely. Certainly, there are aspects which such systems share. Transportation systems share notions of "network", "traffic" and "schedule". There is scope for generalization and reuse of descriptions of these notions. Systems such as those being developed in the manufacturing project MIICI share notions of a software "bus" with which various packages may be integrated. This last has led us into the area of Open Distributed Processing (ODP) and we are starting a separate research project CASINO (Categories for System Integration) that is investigating the formal description of ODP and OMG (Object Management Group) in terms of Category Theory [20].
Since the results of the initial and prototype stages are wholly or partly funded by UNU/IIST they are therefore in the public domain.
There are two aspects of our technical approach that are critical.
Formal techniques have two particular characteristics that allow us 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 us flexibility.
Domain analysis is the exploration and formal description of the domain in which the system will operate. For example, in the RaCoSy project, concerned with train rescheduling for the Chinese Railways, we start 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 us a formal model of the domain. Only when we have elaborated such a model can we go on to do the requirements capture of the actual system being developed.
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; we might say that the result of domain analysis provides an "infrastructure" for software package development.
The particular formal method we use 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, we also make sure that our partners receive the tools (free of charge for research and education) for their continued work.
The following is a brief description of current advanced development projects with indication as to budget and the staff, fellows and visitors involved:
This research and development project is concerned with an overall determination of a normative software architecture that will allow co-existence of, data exchange between and mutual invocation among arbitrary Railway Computing Systems (hence RaCoSy) software packages.
Work so far done has concentrated on the scheduling and rescheduling of trains.
Staff:
During 1994 four Fellows joint with UNU/IIST staff and visiting experts developed a set of domain analysis, requirements capture, software architecture and design descriptions for an operational single standing (i.e. non-distributed) Running Map train rescheduling system.
During mid-94 to mid-95 one Fellow did the domain analysis, requirements capture software architecture and partial implementation of a Station Management system.
During mid-95 to early-96 two new Fellows together with UNU/IIST staff further developed the running map specification, in particular to make it more flexible and handle a variety of train types. It was intended to deal also with distributed train dispatching but the Fellows had to return to China before schedule and before this was completed.
During mid-95 to mid-96 there was a collaborative project between UNU/IIST and the Chinese University of Hong Kong (CUHK). Students and staff from CUHK created a functional extension of the running map tool that used constraint propagation techniques to provide more active support for rescheduling by suggesting possible schedule changes to deal with problems.[24]
A General Theory of Transport has been researched [25].
The project is studying the day to day operation of an airline, including financing, scheduling and timetabling of flights, ticketing and reservations, maintenance and availability of aircraft, passenger and cargo services, air traffic control, etc. Domain analysis and requirements capture documents have been produced.
31 August 1995 to 30 September 1996. Work on the project will be continued if further Fellows are found.
Staff:
1996 Fellow:
The project performs a broad study of the issues pertinent to the manufacturing industry. The high-level goal is to investigate how information technology can be best applied to support the development of manufacturing enterprises in developing countries, able to respond quickly and intelligently to changing market demands. The emphasis is on creating mathematical models of enterprises (in all aspects of marketing, administration, finance and especially production), supply-chains and products, as a prerequisite for the systematic development of software for information and command infrastructure. In particular, the project will study applicability of the emerging ODP (Open Distributed Processing) and OMG (Object Management Group) Reference Models as the underlying computational structure for agile manufacturing, perhaps allowing to share production services and resources across the Internet.
Staff:
1996 Fellows:
Four UNU/IIST Research Reports which document different phases of the project: informal domain analysis [31], development of the formal models for competing [32] and cooperating enterprises [34] and design of the simulation software for education and training (the business game) [33]. The third document was presented at the Workshop on Theoretical Problems in Manufacturing Systems Design and Control, Lisbon, June 1996 and will appear in the formal proceedings.
To show how the two formal models, for competing enterprises ("Towards the Formal Model ..") and for cooperating enterprises ("Virtual Enterprise: On Refinement ..") can be put together and how existing techniques for marketing (Parker's model) and decision-making can be captured within this model.
The MultiScript project is studying the creation and presentation of documents in which more than one language is used, for example a dictionary from one language to another. Particular emphasis is being placed on preserving the natural reading/writing direction of each of the languages in the document, so that, for example, in a document containing both English and Mongolian text the English text would appear exactly like that you are currently reading whereas the Mongolian text would be written vertically in columns, the columns progressing from left to right.
The project is also contributing to the definition of an international standard encoding system for the Mongolian language which will form part of the UNICODE/ISO international standard, a coding system which covers the majority of the world's languages.
Staff: Richard Moore
1996-1997 Fellows:
Ms. M. Erdenechimeg gave an open seminar on the project, entitled "Multi-Lingual Script Processing", at Hong Kong University in April 1996.
A paper describing the domain analysis and the requirements capture for the MultiScript system has been submitted to the 1997 International Conference on the Computer Processing of Oriental Languages, to be held in Hong Kong in April 1997.
As part of the standardization effort Ms. M. Erdenechimeg attended an International UNICODE/ISO Working Group in Copenhagen, Denmark, in April 1996, as well as a smaller meeting, attended only by the subgroup responsible specifically for the Mongolian language, in Beijing, China in August 1996.
Based on these meetings a draft proposal for the standard encoding of the traditional Mongolian script has been prepared for submission to the International UNICODE/ISO working group (Singapore January 1997).
The Vietnamese Ministry of Finance is undertaking, with World Bank support, the development and installation of a Financial Information System. Key functions include synthesis of state budget plans, management of fund allocations, formulation and review of tax policies, exchange of data between various levels and ministries.
This project will study appropriate infrastructures to support the accurate, timely and secure collection and analysis of data.
Expenditures until end 1996 were:
Staff: Chris George
1996-1997 Fellows:
Partner: Vietnam Ministry of Finance.
Exploratory talks are
currently underway with interested institutions in Belarus and the
Russian Federation on External Debt Management computing system.
UNU/IIST is technically preparing for an EDMaCS sub-project
of MoFIT.
During the period March -- September 1996 a number of documents were produced:
Future outputs will include development of the formal model of the tax system, both in detail and outwards into a description of a full financial information system.
The project began with a planning meeting in Hanoi in September 1995.
In January 1996 a two-week course on formal development was presented by UNU/IIST at the Ministry of Finance (MoF) in Hanoi, attended by software engineers from the MoF and from the Institute of Information Technology (IoIT), long time partners with the MoF in developing financial software.
In March 1996 four software engineers from the MoF and one from IoIT came to UNU/IIST as Fellows for six months. Work in this period concentrated on the tax system, the part of Vietnam's financial structure that the Fellows knew best. The work done included both an informal description and a formal model of the tax system, an informal description and a formal model of the security system of the tax system, an analysis of likely future tax policy changes, and the creation of a prototype of the accounting part of the formal model for testing and optimization investigations.
Work in the next period will develop the tax system model in more detail, in order to explore the requirements for the (distributed) implementation and will also create a wider specification of the full national financial information system encompassing, in particular, spending ministries and the role of the Treasury.
This research, advanced development and training project is initially concerned with basic telecommunications protocol aspects, in particular for a special, new Digital Multiplexed Radio Telephone System currently being researched and developed by The Philippine Government's Advanced Science and Technology Institute (ASTI).
The system being developed in The Philippines is designed for particular circumstances common in Developing Countries: dispersed small population centres with difficult intervening terrain. Hence the project contributes to the areas of both self reliance and infra-structural development.
Staff: Chris George
1996 Fellow:
Two research reports were produced [45][44] and [44] was presented at a "Refinement Workshop" in Australia.
Mr. Durmiendo spent 9 months at UNU/IIST working on the problem. Much of this time was spent a possible development route for what proved to be a very difficult problem. But by the end very substantial progress was made, and the work forms the basis of development of the actual system in The Philippines.
In February 1996 the Director of ASTI, Prof. R. Solis, visited UNU/IIST and discussed the project.
Mr. Durmiendo may return to UNU/IIST for a brief spell, 2-4 months, during the next 12 months. Another Philippine fellow may also be identified to continue the work.
The project will conduct a thorough analysis of the whole air traffic control domain, including the support technology used and the rules and regulations governing it, and on the basis of this will formulate requirements on possible software support systems. A prototype of one such support system will be designed and built.
Staff: Dines Bjørner, Richard Moore, Bo Stig Hansen
1996-1997 Fellows:
Karl Leung has performed some preliminary study of the air traffic domain as part of his work towards a Ph.D. thesis at the University of Hong Kong (two 3 months' stay at UNU/IIST).
This project concerns domain analysis and requirements formulation for a financial management system. The purpose is firstly to record the users description of the problem domain in their own terms and in every detail. Secondly, to formulate a domain model based on concepts which on the one hand are intuitive and directly understandable by the professionals in the domain and on the other hand are general enough and have sufficiently precise definitions that they can be used for formulating the requirements to a computer based accounting system. And thirdly, to extract the requirements from the users problem description and express them unambiguously and clearly using the concepts of the domain model.
The requirements will form basis for the actual systems development carried out by Tata Consultancy Services in Pune, India.
100% funded by UNU: UNU Headquarters.
Staff: Bo Stig Hansen, Prashant S. Gajjar
Staff: Richard Moore
Fellow: Hoang Thi Tung Lam, 1 September 1996 to 31 May 1997, Vietnam
This research project examines the problem of integrating heterogeneous applications: written in different languages, running on incompatible machines, using protocols that cannot talk to each other. It also looks at how the problems created in this environment are tackled within increasingly accepted distributed platforms like e.g. the Common Object Request Broker Architecture (CORBA) and how the new problems arise due to the lack of any semantic constraints in CORBA's (and any other we know) Interface Definition Language (IDL).
Staff: Tomasz Janowski, Chris George
1996 Fellows:
Activities have been initiated which correspond to the study of:
1. Distribution transparencies - common features of the distributed platforms that aim to free application designers from the difficulties of writing software for distributed, heterogeneous environments. We want to show how to specify transparencies and how to use syntactic transformations to formally verify them. This is to allow for the common treatment of different transparencies, for the use of standard techniques for provable correctness (with their tool support) and for the composition of transparencies.
2. Extending the IDL descriptions by the axioms of two kinds: representing the effects of one-step invocations of interface functions (as equations) and representing the properties that need to hold between the invocations (as modal or temporal properties). We see the promise of using the first for the formal verification (off-line) and the second, especially useful for the legacy systems, for on-line `safety' checks. Such on-line checks would be performed by the model-checking engine, generated as part of the IDL translation. We also want to study the use of model-checking for automatic discovery of services, via interface repositories or white (naming) or yellow (trading) pages.
3. ODP (Open Distributed Processing) and how category theory can provide the `neutral' and most abstract formalization of its viewpoint languages and modeling concepts allowing e.g. to formally address the issue of conformance. This conformance would allow for interoperability between, not only within distributed platforms.
Staff: Dang Van Hung and Tomasz Janowski
1996 Fellow:
Staff: Dines Bjørner
1996 Fellows:
In all of the projects of section 2.2 UNU/IIST deploys and, in a sense enlarges upon the RAISE Method. In addition the Director is currently trying to put together a compendium on the "enlargement" [51] LSD: Logical Systems Development. A synopsis of this compendium can be found in [52] which gives a personal account of UNU/IIST's R&D projects.
| | | Annual Report 1996 | |