聯合國大學國際軟件研究所(UNU/IIST)
Dines Bjφrner Chris George 徐啓文
摘要
聯合國大學國際軟件研究所(UNU/IIST)設在澳門，它是由澳門，葡萄牙和中華人民共和國三個政府聯合出資建立的。
UNU/IIST是聯合國大學的一個研究及培訓中心。它致力於幫肋發展中國家形成獨立的軟件技術；具體說，UNU/IIST幫助發展中國家建立他們自己的軟件工業，更新大學計算機敎育課程以及參加國際性研究。
為了達到這些目的，UUN/IIST參與及提供高級軟件開發，研究，研究生及博士後課程，專題活動和信息傳播。通過高級軟件開發和研究，UNU/IIST培訓了一大批工程科研人員。大多數高級開發項目是基礎結構的軟件支持，而研究項目主要是關於交互系統，實時系統和混合系統的形式化方法。
UNU/IIST
Dines Bjorner Chris George Xu QiWen
Resumo
O Instituto Internacional de Tecnologia de Software das Nações Unidas (UNU/IIST) está sediado em Macau foi fundado conjuntamente pelos governos de Macau, Portugal e República Popular da China. A UNU/IIST é um Centro de Formação eInvestigação da Universidade das Naçöes Unidas. destina-se a cooperar com países em vias de desenvolvimento a fim de adquirirem autosuficiência em tecnologia de software. Em particular, a UNU/IIST ajuda os países em vias de desenvolvimento a determinarem as suas necessidades e fortalecerem as suas capacidades não só de software próprio como também para exportação, modernização dos curricula do ensino universitário e a participação em investigação internacional. Para alcançar estes objectivos, a UNU/IIST está envolvida em projectos avançados de desenvolvimento, projectos de investigação, cursos de pós-gradução e pós-doutoramento, actividades e divulgação. Através de projectos de desenvolvimento e investigação conjuntos, a UNU/IIST tem formado um grande número de engenheiros e cientistas. Projectos de desenvolvimento avançado centrado em software de apoio a infraestruturas e, por outro lado, a investigação concentra-se em métodos formais para Sistemas Reactivos, Sistemas em Tempo Real e Sistemas Híbridos
1 Introduction
The United Nations University International Institute for Software Technology (UNU/IIST) is based in Macau. UNU/ IIST is fundamentally concerned with assisting developing countries with the development and procurement of software technology. Although the growth of computer usage in such c ountries is high, most of them urgently need the establishment or expansion of both basic and advanced training, development and research facilities. Thus there is both a lack of available software professionals for industrial growth and a chronic shortage of educators and trainers of the professionals of the future.
Moreover, most developing countries have few software companies and littlie experience in industrial software development. Local software development is essential in developing countries, not only to establish and strengthen local industry, but also to provide software in local languages and with cultural features adapted to the specific needs and conditinos of each country.
Although the knowledge and competence gaps between the industrialized and developing countries may be substantial, UNU/IIST can help specialists in developing countries to reach state-ofthe-art levels in software technology.
UNU/IIST is a Research and Training Centre (RTC) of the UNU. It was founded in 1991 and is jointly funded by the governments of Macau, Portugal and the People's Republic of China. As well as providing two-thirds of the endowment fund, the Macau government also supplies UNU/IIST with its office premises and furniture without charge and subsidizes fellow accommodation.
1.1 Aims and objectives
UNU/IIST assists developing countries in meeting needs and in strengthening capabilities in three areas:
·development of their own and exportable software,
·university education curriculum development, and
·participation in international research.
In particular:
1. UNU/IIST is a cradle for educating young computing professionals, both university scientists and industry software engineers, beyond post-graduate level.
2. UNU/IIST offers a showroom for demonstrating paradigmatic approaches to application modelling,requirements engineering, programming, software engineering, and software technology management techniques and tools.
3. UNU/IIST serves as a bridge for enhancing co-operation between industrialized and developing countries in the area of software technology.
4. And UNU/IIST constitutes a channel for bringing to international attention achievements of developing countries in software research and technology.
1.2 Activities
UNU/IIST is involved in a nurmber of activities:
1. Advanced development projects
2. Research projects
3. Post-graduate and post-doctoral courses
4. Events
5. Dissemination
The first two of these are dealt with in detail in sections 2 and 3 respectively.
Courses are provided both in Macau (in liaison with the Faculty of Science and Technology at the University of Macau) and also in developing countries. To date courses have been given in China, India, Thailand, Vietnam, DPR Korea, The Philippines, Indonesia and Mongolia. Current plans include Argentina and Brazil;the Southeast Asia dominance is only a temporary feature. The courses centre around formal software development, in particular RAISE and the Duration Calculus.
Events include panels, task forces, workshops and symposia. Task forces and workshops explore such issues as university curricula [1], professional accreditation [2], and software product and process standards. Workshops and symposia involvescientists, lecturers, technologists, businessmen and policy planners, from the developing world together with UNU/IIST staff and visiting experts. A two-week event, Decision Support Systems for Sustainable Development is planned for early 1996. Other one-week events on Computing System Procurement Principles, Computing System Facilities Management, and Software Accreditation and Certification are planned for later in 1996. A one-day event on Trading over the Internet was held in December 1995.
Dissemination is currently based around the extensive library that UNU/IIST has in Macau;it is hoped in future to extend this to include public domain software.
1.3 Mode of working
The advanced development projects and the research projects are carried out jointly with other institutions-industrial companies, government departments, universities or research institutes from developing countries. Much of the work is located at UNU/IIST and involves Fellows from the partner institutions spending, typically, 9-12 months at UNU/IIST. Fellows work closely with UNU/IIST staff and with visiting experts in “Master Class” style.
UNU/IIST is not large-currently there are seven academic and technologist staff, eight administrative and technical staff, and fourteen Fellows. UNU/IIST (like the rest of the UNU) does not award degrees, though many Fellows arrange for their work at UNU/IIST to be part of work for post-graduate degrees.
1.4 Formal software development
Developing industrial, large scale software involves severaldisciplines: application domain modelling and requirements capture, programming, software engineering management, and computation science. Although UNU/IIST is also engaged in other, non-developmental issues, the above disciplines are a major focus. As is well established in other branches of engineering, the use of mathematical modelling and reasoning about contemplated designs is at the center of any of the development activities that UNU/IIST propagates.
The main technology used in the advanced development projects is RAISE [3, 4] - Rigorous Approach to Industrial Software Engineering. RAISE was developed by European collaborative projects during 1985 - 1995. It includes a formal specification language, a method for developing software and a set of tools. The language provides the mathematical basis for expressing the properties of software; the method provides guidelines and techniques for demonstrating correctness and developing a specification into a final, executable implementation; the tools support these activities.
UNU/IIST is dedicated to the professionalization of software development. Professionals are developers, scientists, or managers who are scientifically and technically interested in the theory as well as the practice of their discipline. They know whether a product can be developed in a trustworthy manner, and will develop software in such a manner, performing as a natural part of development calculations which reveal properties of application domain models, abstract functional and behavioural specifications, and of designs-long before costly implementation has taken place. They also continuously know whether they are up-to-date with the forefront of the field and are able to stay abreast through their own work, and are interested in further developing the theory and practice themselves.
1.4.1 Domain analysis
In order to ensure that the software created is fit for its intended purpose, a careful study must be made of the domain in which the software is to serve. Domain analysis involves the mathematical expression of the component entities of the domain and their properties. Such expressions are commonly termed (mathematical) models.
This process of modelling the domain is exemplified by Maxwell's equations (figure 1). A huge range of modern technology depends on the adequacy of these equations as a mathematical model of electromagnetic radiation.
Another example is a simplified version of part of the domain for railway computing systems PRaCoSy project (see the PRaCoSy project in section 2). As shown in figure 2, the Network consists of Lines and Stations. Lines connect two stations and may normally be used in either one direction (up or down) or in both directions.
Having defined these concepts we can also express the consistency requirements for a network (figure 3):the stations at the ends of lines must exist and every station must have at least one line leading to it or from it.
1.4.2 Requirements capture
Once the domain is modelled, i. e. its essential aspects are formally described and understood, the requirements for the system to be developed can also be expressed, again precisely and formally using mathematics, and in terms of the concepts from the domain analysis. Having, for instance, described the components of a lift system, a safety property that the doors are open at a floor if (and only if) the lift is halted at this floor, is captured in RAISE in figure 4.
Models may be very abstract or morc concrete. Abstract models express only the most general and intrinsic functionalproperties of the system, such as safety properties (nothing bad will ever happen ) and liveness properties (progress will ev entually be made). More concrete models allow non-functional properties such as dependability, performance and humancomputer-interface facets to be captured. Concrete models can slao support experimental model executions early in development, before design decisions are made.
1.4.3 Development
Having established a formal description of the properties of the system, it is possible to develop it rigorously into an implementation that is both executable and efficient. That is, we can preserve the properties of the original specification during development. If these properties are the ones actually required, then we have assurance that the developed software will be correct.
In practice there are a number of possible styles of development of varying degrees of formality. Sometimes we code directly from the first specification; sometimes we do some development into more efficient data structures and/or algorithms before coding,and in this case we may either prove formally that the development is correct or we may “inspect” or “review” the development for correctness. Ideally we would like to prove all properties automatically, but in practice there are inherent limitations in doing things automatically and so theorem provingrequires human interaction and is therefore expensive because of the time it takes. Less formal, yet still rigorous, approaches to showing correctness are then preferred.
1.4.4 Software engineering
While formal methods emphasize particular aspects of software development they do not obviate the need for other aspects of software engineering, including testing,① version and configuration management, requirements and design decision tracking, documentation, and project management.
2 Advanced development projects
Advanced development projects are one of the main activities of UNU/IIST. They usually involve one to three phases, each lasting for 9 to 12 months, involving one to four Fellows and one or more UNU/IIST staff. They generally focus on software support for infrastructures and aim to
1. train Fellows,
2. develop (prototypes of) advanced software, following the development stages of domain analysis, requirements capture and software development, and
3. contribute to scientific research on the application domain, the applied development method, and the socio-economic notion of infrastructures.
Some of the derivative research is of cross-, inter-, and multidisciplinary nature in bringing the discipline of computing science together with the disciplines of operations research, control theory, business administration and industrial engineering. Examples of current advanced development projects are:
1.PRaCoSy: People's Republic of China Railway Computing System
A country's railways are an important resource and part of the country's economic infrastructure. Efficient railway utilization is the main goal of this project.
Initially software is being researched and developed for distributed train dispatch (between Wuhan and Zhengzhou) [5]. Long range aims are to provide an overall software architecture suited as a framework (providing "sockets")for a wide variety of software packages covering:
(a) strategic railway systems development: planning, design and development of new lines, stations and services;
(b) tactical resource allocation and scheduling; timetablcs,trains, staff, etc.;
(c) operational activities: passenger and freight reservation and handling; train dispatch and control; passenger and freight services; etc.;
(d) statistics gathering-feeding back to item la
Five Fellows from the Chinese Railways worked on the first phase at UNU/IIST and two more are presently contributing to the research and development of PRaCoSy.
2. MI2CI: Manufacturing Industry Information and Command Infrastructure
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) Reference Model as the underlying computational architecture for agile manufacturing, perhaps allowing the sharing of production services and resources across the Internet. Based on the formal model and using the underlying computational structure, the project will ultimately approach an implementation of the prototype software for education and training-computerized business game simulating decisionmaking in real-life manufacturing.
As an example of formalizing a production process, suppose that we described the state s of the manufacturing enterprise, its warehouse, shopfloor, employees and a bill of products. Then the capacity of the enterprise to produce a product p, either by p begin already available in stock, or by assembly (humansupervised) from subproducts on the shopfloor, can be described by a predicate can-produce(p, s) in figure 5. Note that if p is not in stock, can-product (p, s) calls itself recursively, for all subproducts q of p. And to do so is legal since no product is a component of itself, and if p is component of q and q of r then p is a component of r, as specified by the additional axiom in figure 5.
Two Fellows from De La Salle University, Manila, The Philippines are presently working on MI2CI.
UNU/IIST is planning follow-up research on MI2CI with the Faculty of Science & Technology of the University of Macau and with The New University of Lisbon, Portugal, as part of a larger collaborative framework.
3. ABC'2000: Airline Business Computing
This project researches computable aspects of strategic, tactical and operational issues of airlines. The aim is to develop software support for:
(a) the strategic planning, evaluation and management of resources-aircraft, route networks, staff, facilities (ticket agencies etc.) and finances-and the support of market planning;
(b) the tactical allocation and scheduling of all resources,including timetables; and
(c) the daily operations: ticketing, passenger and freight check-in, gate control, flight dispatch, etc.
One Fellow from Vietnam Airlines is currently working on ABC'2000.
4. DiMuITS: Digital Multiplexed radio Telephone System
A telephone system is being developed and installed in ThePhilippines based on microwave links between local telephone exchanges serving distributed communities. Multiplexing protocols are used between the exchanges. The DiMuITS project aims to
(a) formally describe the properties of the multiplexing protocols being used; and
(b) formally specify the complete system and show that it satisfies the requirements for a telephone system.
In this case, rather than develop the software at UNU/IIST the emphasis is on the early stages of specification and development, proving the system properties and ensuring the development maintains them. A typical telephone system property (which has been proved for the specification) is illustrated in figure 6: if phone not′ is waiting for phone no′, which is ringing, and no no is picked up, then each of the phones is connected to the other.
One Fellow from The Philippine Government' s Advanced Science and Technology Institute (ASTI) is currenty working at UNU/IIST while his colleagues at ASTI are developing the software.
5. MultiScript: European and Asian Script Text System
In Asia alone all four directions of presenting text are represented:
Figure6 : A basic property of a telephone system .
(a) Mongolian (or Manchu) traditional script, now revived, has vertical columms which proceed left to right.
(b) Chinese and Japanese traditional presentations have columns proceeding right to left.
(c) Arabic and Hebrew have lines read right to left and text proceeding top to bottom.
(d) Many other languages are like English, in which lines are read left to right while text also proceeds top to bottom.
Increasing international communication generates the need for commerical contracts and other documents in pairs (or even triples) of different direction texts, and requires dramatically new forms of text systems.
The MultiScript project studies such text systems and is prototyping a common software architecture that allows (reasonably) arbitrary word processing systems to co-operate for the purposes of the input, formatting and communication of texts in any combination of scripts.
MultiScript also studies varieties of document classes: newspapers, text books, inter-office letters and memoranda, business contracts, legal texts,② etc.
A Mongolian Fellow is being trained in the latest software technology and development methods while contributing actively to the study, research and development of MultiScript.
6. ATC'2000: Air Traffic Control
Asian air traffic is booming. In China alone we may speak of an “explosion” in air traffic. In the Pearl River Delta five airports compete for air space: GuangZhou, Hong Kong, Macau, Shenzhen and Zhuhai. Over the next decade billions of dollars will be spent on acquiring high technology equipment and software for air traffic control in the region.
The ATC'2000 project aims at developing a computer platform for the training of air traffic controllers. Therefore the ATC' 2000 project includes studies, formalizations and "implementations" of civil viation air traffic rules and regulations, air traffic controller behaviour, safety criticality issues, etc.
Beyond this ATC'2000 is expected to help bring such skills to its partners that will enable them to better select, and on more advantageous conditions, the necessary high-technology software involved in air traffic.
Initial work on ATC'2000 has begun, but the project is only expected to start if and when a Fellow from Thailand's air traffic control authority Aero Thai arrives in Macau. This is expected early in 1996. The project is joint with AIT, the Asia Institure of Technology. Zhuhai's Science and Technology Commission has expressed interest, as has the leading relevant, high technology company in Zhuhai: Asia Simulation and Control Corporation-a potential future developer of highest technology air traffic control subsystems, including “trainers”
7. MoFIT:Vietnam Ministry of Finance IT Study
Effective economic management can make a big difference to a country's economic performance, and computerized information systems are an important useful management tool, ensuring information is accurate, comprehensive and up-to-date.
The Vietnamese Government's Ministry of Finance(MoF) has asked UNU/IIST to assist in the architectural design of its computerization.
Initially UNU/IIST, together with two Fellows from the MoF, will design a comprehensive Budget Planning and Execution System.
Concurrenty the MoF will use UNU/IIST as a consultant in formulating tenders for bids for the acquisition of hardware and software for its overall computerization.
As well as the projects listed above there are others thatalthough aimed widely-serve primarily as the basis for Macau student M.Sc. Thesis projects. These are concerned with
1. Libraries-linking libraries with each other and with publishers, distributors etc. as well as borrowers.
2.Visitor information, routing and reservations - for citizens and visitors to interactively find information, navigate around Macau, book tickets, hotel rooms, restaurant tables, etc.
3.University management-linking all the departments with their variety of information system needs.
4.Geo-and demographic information-for planning purposes and also as a basis for the visitor information system (item 2 above).
3.Research
While advanced development is mainly concerned with engineering aspects of system construction, the research at UNU/ IIST aims at understanding foundational matters of more sophisticated software technology. UNU/IIST has chosen the area of Real-time, Hybrid, and Reactive Systems as its main field of research, as this is one of the most active research area of formal methods for software construction. The objective are
1. to train Fellows in research techniques,
2. to introduce Fellows to front-of-the-wave research topics and ensure that returning Fellows propagate the techniques to developing countries,
3. to contribute to the field.
Reactive Systems are those which maintain on-going interactions with their environments; Real-time Systems exhibit non-trivial and critical timing properties and are executed with resources that are limited in number and speed; Hybrid Systems include both continuous and discrete components. During execution, Real-time Systems and Hybrid Systems usually interact with their environments and are therefore typically Reactive Systems; Hybrid Systems evolve over time and hence are typically Real-time Systems.
Figure 7: Segments of Fisher's real-times mutual exclusion protocol. There is a mxcimum delay between the first and second statements, and a minimum delay between the second and the third statements. Under suitable conditions on these delays, the protocol guarantees that at most one process can enter its critical section .
Representative examples of Hybrid Systems are control systems where computers are used to decide control policies. Due to rapid development of processor and circuit technology, many modern systems, even consumer electronics, use software to control physical components. How are these systems to be analysed? How are they to be designed? How can they be verified? There are many possible approaches, and more questions than answers.
The major formal tools that UNU/IIST uses are Durational Calculi [6, 7, 8] which form a family of real-time logics based on the Interval Temporal Logic. They were first inverstigated in the European ESPRIT project ProCoS (Provably Correct Systems) by Zhou Chaochen and his colleagues at the beginning of the 1990s. During 1992 to 1995, Prof Zhou successfully built at UNU/IIST a strong group on Durational Calculi and its applications to Real-time Systems and Hybrid Systems. In the past there years, methodological issues have been studied alongwith representative case studies such as inverted pendulum [9], steam boiler[10], water tank [11] and chemical concentration systems [12]. More than 15 papers have been presented in international journals and at conferences.
So far, UNU/IIST has trained about 10 Fellows from four developing countries. As another effort to bring the research results to scientists in developing countries, UNU/IIST frequently provides offshore intensive courses. UNU/IIST is also pleased to be able to help The University of Macau to build its research programme, by conducting joint research, organizing nesearch seminars, supervising graduate students, and supporting the participation of international events.
Besides Duration Calculi, other theories of reactive systems, such as compositional verifiaction and refinement calculi, are also being investigated.
4 Acknowledgements
UNU/IIST could not have made the achievements it has without the substantial and continuing support of the Governor of Macau, General Vasco Rocha Vieira, his staff and his Government (in particular Dr. Jorge Rangel). We are also grateful for the assistance we have received from the Macau Foundation, in particular the President, Dr. António Rodrigues Júnior and his staff, and from many people at the University of Macau, in particular Professors Ferreira, Zhou Li-Gao, Rui Martins, and Li YiPing.
We also wish to thank the numerous other institutions and people in Macau who have made our new institute and supported it in various ways.
References
(1)Dines Bjorner. University Curricula in Software Technology. Technical Report, UNU/IIST Rept. No. 7, UNU/IIST, P. O.Box 3058, Macau, March 15 1993.
Keynote address: IFIP TC3 WG3.4/SRIG-ET (SEARCC) Internation Working Conf. 1993: Software Engineering Education, Hong Kong, Sept, 28 - October 2, 1993.
(2) Dines Bjφner. Accreditation, licensing and Certification; Curricula, Engineers and Software. Technical Report, UNU/IIST Rept. No. 14, UNU/IIST, P. O. Box 3058, Macau, 7. Nov. 1993, Revised 8. December 1993. Presented at the UNIDO/COGIT Meeting, Vienna, Austria Nov. 23, 1993.
(3) The RAISE Language Group. The RAISE Specification Language. BCS Practitioner Series. Prentice Hall, 1992.
(4) The RAISE Method Group. The RAISE Development Method. BCS Practitioner Series. Prentice Hall, 1995.
(5) Dong Yulin and Dines Bjφner. PRaCoSy: Document Deliverables. Technical Report dyl/deliv/1, UNU/IIST, P. O. Box 3058, Macau, December 1994.
(6) Zhou Chaochen, C. A.R. Hoare, and A. P. Ravn. A calculus of durations. Information Processing Letters, 40(5): 269-276, 1991.
(7) Zhou Chaochen, A.P. Ravn, and M.R. Hansen. An extended duration calculus for hybrid systems. In Hybrid Systems, R. L. Grossman. A. Nerode, A. P. Ravn, H. Rischel (Eds.). LNCS 736, Springer-Verlag, 1993.
(8) Zhou Chaochen and Li Xiaoshen. A mean value calculus of durations. In A. W. Roscoe, cditor, A Chassical Mind (Essays in Honour of C. A. R. Hoare), Pages 431 - 451.Prentice-Hall, 1994.
(9) Belawait Widjaja, Chen Zongji, He Weidong, and Zhou Chaochen. A cooperative design for hybrid systems. In 2nd European Workshop on Real-time and Hybrid Systems, 1995.
(10) Wang Juan, Li Xiaoshan, and Zhou Chaochen. A duration calcuius approaoh to specifying the steam-boiler system. In The Daghstuhl International Workshop, 1995.
(11) He Weidong and Zhou Chaochen. A case study of optimization. BCS Computer Journal, to appear.
(12) Xu Qiwen and He Weidong. Hierarchical design of a chemical concentration control system. In R. Alur, T.Henzinger, and E. Sontag, editors, Verification and Control of Hybrid Systems. Springer-Verlag, 1995.
Note:
① Even if we prove everything, the relation between the specification and the actual desires of the user is subject to interpretation, and the relation between the formal model the formal model and the components of the real world domain is merely an assumption: it is still necessary to test software by executing it and checking that it behaves according to its requirements.
② In Macau, legal texts need to be represented in both Chinese and Portuguese; in Hong Kong, in both Chinese and English.
