Publications

 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.

 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.

 We describe work done at \unuiist\ involving staff from the Chinese railways. The immediate aim is to develop software that can improve the efficiency of the Chinese railway system, particularly in the scheduling of trains. In the longer term we hope to develop the capacity of the Chinese railways to produce and even market their own software. The part of the project described here includes the development of formal models of some basic components of railways (networks of stations and lines and timetables) and the activities needed to schedule and reschedule trains using a \emph{running map}. This part finished with the delivery of a prototype running map tool, and some conclusions are drawn about the formal development of this tool.

 Before an architecture for a software system (or package) --- that is: a definition of concepts and facilities of the software system (resp.\ package) to be developed --- can be given, one first establishes proper requirements expected of that software, that is: we base software development on requirements specifications. These requirements are captured from understanding first the domain in which the software is to serve and then from understanding the expectations of the new software as an operational part of the thus extended domain. Thus understanding the domain seems to be a very first order of `business'! In this paper we present an example of the collection of (informal) procedures and (formal) techniques that are being applied in understanding the Railway System domain --- as part of a large scale technology transfer project joint with various software development and computer centers of the Chinese Railways in researching and developing proper software eventually for all aspects of railway operation in China.

 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.

 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 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.

 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 is a contribution to the PRaCoSy (Peoples Republic of China Railway Computing System) project, a collaboration between the Chinese Ministry of Railways and UNU/IIST. It builds on previous work that formalized the notions of railway networks, timetables and scheduling. It aims to deal with two problems: (i) how to reschedule as well as schedule trains (ii) how to distribute these tasks.

 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.

 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

 We outline the formal modelling of a software system to support the scheduling and rescheduling of trains. The current (prototype) system supports only centralized rescheduling, but in practice rescheduling is done on an area basis, and a distributed system is required. Developing a distributed system involves the notions of \emph{delegability} of functions to adjust schedules and \emph{distributability} of functions to analyse them for conformance to regulations. We formalize these notions in terms of a more abstract, generic specification and then instantiate this to generate a specification of the distributed system.

 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 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.

 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.

 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's activities in 2007. It describes the implementation of UNU-IIST's research, development, and training projects, its reports and its 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.

 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.

 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.