Publications

The book describes 12 case studies which use RAISE (Rigorous Approach to Industrial Software Engineering) to con- struct, analyse, develop and apply formal specifications. The case studies present a wide range of application areas: authentication of communications protocols, error detection in programs, geographic information systems, library management, multi-lingual documents, production planning, run-time verification, software design patterns, software reuse, taxation management, telephony, and travel planning. Most have little or nothing to do with safety-critical systems, traditionally considered as the area in which formal methods are most applicable, and many of them do not involve verification. The cases studies illustrate diverse uses of formal specifications: to capture requirements for new software, to carry out software development from requirements, to formalise algorithms in order to prove their correctness, to check if software behaves correctly at run-time, to build models of application domains, to relate descriptive and prescriptive models, to formalise notations for software development, and various other uses. They also try to put the task of creating formal specifications into perspective, asking questions about the purpose, scope and use of the formal models before the models are built.

The case study chapters have each been written by one of this book's editors. Each case study describes work done at the United Nations University's International Institute for Software Technology (UNU-IIST) in Macau by that editor in collaboration with fellows (lecturers or post-graduate students from developing countries). Each case study chapter concludes with information about the fellows involved, the relevant UNU-IIST technical report(s), and other related work.

 There are many examples of the use of the technique of domain analysis for modelling software systems in the initial stages of their development, although the case studies chosen are often of small systems or of small parts of large systems. In this paper we show that the techniques can be as readily applied to very large domains and how a manageable formal model of the domain can be obtained by abstracting appropriately. We illustrate this with a case study based on the airline business domain. We also discuss how this formal model can be developed towards software support systems for the airline industry which capture a wide range of different requirements, and how it might be applied more generally.

 Although there are increasingly many text processing systems which support multiple languages, the majority of these do not allow the different languages to retain their traditional writing direction, instead imposing either that of the European families of languages (each line of text read left to right; lines ordered top to bottom) or that of the language of the country in which the software was written. In this paper we present a model of documents which not only allows the writing direction of a document as a whole to be defined but also describes multi-lingual documents in which different pieces of text have different writing directions. We also discuss the design of a software system based on this model which allows text in different languages which has been generated using existing text processing tools to be combined into a single multi-lingual document.

 This document is the first of a series of three recording the output of the second phase of UNU/IIST's MultiScript project. It explains the basic structure of multi-directional, multi-lingual documents and some related auxiliary concepts (including how locations within such a document can be determined) and gives a formal specification of this in the RAISE specification language, RSL. This modifies and extends the preliminary specification in the UNU/IIST report No 75. The other documents in this series cover the display and printing, UNU/IIST report No 112, and the creation and editing, UNU/IIST report No 113, of such documents.

 This document is the second of a series of three recording the output of the second phase of UNU/IIST's MultiScript project. It extends the description and the formal specification of multi-directional, multi-lingual documents presented in the UNU/IIST report 105 to cover the display and printing of such documents. The third document in the series, UNU/IIST report 113, covers the creation and editing of multi-directional, multi-lingual documents.

 This document is the third of a series of three recording the output of the second phase of UNU/IIST's MultiScript project. It extends the description and the formal specification of multi-directional, multi-lingual documents presented in the UNU/IIST report No 105 to cover the creation and editing of such documents. The second document in the series, UNUIIST report No 112 covers the display and printing of multi-directional, multi-lingual documents.

 Nowadays electrical communications systems are being used more and more widely to provide global connections between very large numbers of people. In order for such systems to operate efficiently and effectively, control must be distributed to local sub-networks, with each sub-network being responsible only for a small part of the system and passing on the responsibility to some adjacent part of the system whenever it is unable to perform the whole of a requested task itself. In this paper we describe a generic hierarchic communications system which is structured in this way and we give a formal specification in RSL of its structure and of the message-passing mechanism by which responsibility is delegated.

 This report contains four example RSL specifications which have been developed for use as case studies in courses on RAISE. All four examples are built around the general idea of a ``Public Service System''. The first three deal with specific examples of public service systems: a supermarket, a petrol station, and a bank. Each is self-contained, and so is suitable to be used individually, for example on a short course. The fourth example deals with a general public service system which incorporates all the features of the first three examples. This is primarily intended to be used together with the specific examples as an extended case study on longer courses.

 Traditional Mongolian script has recently been the subject of an international standardisation process within the scope of ISO/IEC 10646, which specifies an encoding scheme covering the set of characters occurring in the written forms of all the world's languages together with more general symbols~(punctuation marks, mathematical symbols, and so on). This paper gives an overview of this encoding and the principles on which it is based and explains how the full range of positional variants of characters and of ligatures are obtained from it.