Publications

 This document covers UNU-IIST's activities in 2008. It describes the implementation of UNU-IIST's research, development, and training projects, its reports and its publications.

 Our aim is to exploit the FDR model checker for descriptions of concurrent systems written in the RAISE Specification Language (RSL). To do this we define a translation from RSL to CSPM, show that the translation is a strong bisimulation, and then that various properties are preserved by strong bisimulation. This allows us to infer properties of the RSL description from the results of running FDR.

 This Report shows the application of model checking techniques over formal specifications expressed in RSL using the FRD2 refinement checker, for which we have developed a first version of a translator from RSL to CSPM. We give an overview of the semantic and syntactic differences between these two languages, then we define a translation subset and finally we show the strategy used to find the respective equivalences in order to make the translation possible; we also briefly describe the development of the translator and show the use of this translator with some typical concurrent examples.

 This document covers UNU-IIST's activities in 2007. It describes the implementation of UNU-IIST's research, development, and training projects, its reports and its publications

 The success of model-based testing, in automating the testing of an implementation given its state-based (or model-based) specification, raises the question of how best the specification can be tweaked in order to facilitate that process. This paper discusses several answers. Motivated by an example from web-based systems, and taking account of the restriction imposed by the testing interface, it considers both functional and non-functional properties. The former include laws, implicit system invariants and other consistency conditions whilst the latter include security leaks. It concludes that because of the importance of the link between specification and implementation in the testing process, there is a trade-off between genuinely useful testing information and the incorporation of some degree of information about the link, not normally regarded as part of the specification.

 In this work, we study about formal design and verification of protocols using CSP(Communicating Sequential Processes) formalism. The protocols concern multicast communications; we develop formal models of multicast communication protocols with CSP and then verify the models using FDR which is the model checking tool of CSP.

 This paper describes how the communication protocol of Mondex electronic purses can be specified and verified against desired security properties. The specification is developed by stepwise refinement using the RAISE formal specification language, RSL, and the proofs are made by translation to PVS and SAL. The work is part of a year-long project contributing to the international grand challenge in verified software engineering. Keywords: Formal methods, RAISE, PVS, SAL, verification, Mondex

 This document covers UNU-IIST activities in 2006. It describes the implementation of UNU-IIST's research, development, and training projects, its reports, and its publications.

 An on-line survey of former UNU-IIST fellows was made in June-August 2006. 82 former fellows answered the questions in the on-line questionnaire. This report summarises the results from the survey.

 In this report, we present the specification for a reliable banking system, concentrating on opening an account, depositing, transferring and withdrawing. In order to specify the operations of banking system we deal with head-office, branches, accounts, customers, clerks, and reciprocal actions between them. We also specify other requirements in the banking system such as printing a statement, overdrawn reporting and database management. The specification is presented using the RAISE Specification Language.

 This report presents the basic foundations for the verification by means of model checking techniques of formal specifications expressed in RAISE. During this work, third party model checkers are briefly discussed and analysed for suitability under two main criteria: (a) syntactic/semantic restrictions imposed by the model checker's language and (b) the applied representation technique for the system (i.e. symbolic or explicit). Then, the selection of Symbolic Analysis Laboratory (SAL) as the model checking tool is justified and all RAISE syntactic constructions are analysed for transformation into SAL. Foundations for the semantic preservation during the translation are provided in the cases where the justification is not a trivial one. Finally, the design of extensions to RAISE to define transition systems and to support temporal logic formulas is described and the tool that implements the first version of the described translation procedure is also reported

 This document covers UNU-IIST activities in 2004. It describes the implementation of UNU-IIST's research, development, and training projects, its reports, and its publications

 Mobile computing shares many features with distributed computing, but it also extends the latter because of the need to deal with the mobility and occasional disconnections of both devices and applications. In this report we give the RSL specifications to describe the behavior of applications in a mobile computing environment. Specifically, we give the specification for describing the migration, hoarding and cloning behavior of mobile applications. Keywords: Mobile Computing; Graphical Notation; Mobicharts; Formal Specification; RAISE; Consistency Conditions; Testing.

 In this report we propose an approach for translating RSL specifications which describe data-intensive applications into relational database implementations. The aim of the work is to automate the translation of an RSL variable of map type into a database table.

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.

 In this report we present the basic specification for a management system for a university library, concentrating on the loaning service of the library. For identifing and specifing the university library's activity we deal with resources, borrowers, librarians, regulations and the reciprocal actions between them. We also take into consideration the extension of this specification covering other requirements in the university library's activity. The specification is presented using the RAISE Specification Language.

 The present document covers UNU/IIST's activities in 1999. A brief overview is followed by a description of the status of ongoing research, advanced development, curriculum development and university development projects. This is followed by reports on UNU/IIST's Fellowship programme, advanced courses, events and academic meetings, Off-Shore R\&D projects, and administrative matters. UNU/IIST's Macau-oriented activities are reported, as are its linkages to UNU and other UN organisations. The last section gives an outline of planned activities for 2000.

 In this document we continue the work started in ``Developing a Financial Information System'', UNU/IIST Research Report 81. That document concentrated on the taxation system and on its detailed development. Here we take a broader view, sketching the taxation system and also the budget, treasury and external aid and loan systems. Then we show how these may all be combined, allowing not only ``vertical'' communication within each system but also ``horizontal'' communication between components of different systems. We thus provide a top-level specification of a national financial information system.

 This document describes the work done in the UNU/IIST MoFIT project during the period April--September 1996 by five Fellows from Vietnam (four from the Ministry of Finance, one from the Institute of Information Technology). The eventual aim of the project is to describe a complete financial information system. The first part of the project concentrated on the taxation system, the Vietnamese Government's main revenue collecting system. It includes a domain analysis in two parts, an informal narrative and a formal model; a prototype of part of that system developed from the formal specification and used to test it; a description of the security aspects of the system; an extension of the formal model describing the security aspects; and a description of taxation policies, particularly those likely to change in the immediate future. The formal components are written in the RAISE specification language, RSL using the RAISE development method.

 This paper presents a formal development of a Radio Telephone System by a sequence of correctness-preserving refinements. We follow several steps of refinement from an abstract applicative specification which is validated against the properties and behavior of a basic telephone service, to a specification involving a central station and a number of remote stations communicating synchronously by means of radio channels. Particular features of the development are the decomposition of the basic telephone service into separate layers for the phones and the communication network, and the introduction of finite communication resources. We verify that the decompositions preserve correctness and that the resources are allocated and released correctly. The work was carried out with the RAISE specification language and its associated method, using the RAISE tools.