Publications

 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.

Two new performance estimation algorithms are presented in this report. One is an optimal lower-bound prediction for the Resource Constrained Problem, and we propose a branch-and-bound algorithm to obtain the exact solution by means of some novel bounding techniques. Experimental results show the efficiency and effect of this algorithm. The other is an approximate predication technique which is applicable to the hardware compiler for fast performance estimation. As the hardware compiler adopts the software compilation techniques, but is different from the traditional synthesis approach, the second algorithm we propose here could easily be embedded into this kind of hardware compiler to obtain results quickly.

We present an approach to elicitation of user preference models in which assumptions can be used to guide but not constrain the elicitation process. We show how to encode assumptions concerning preferential independence and monotonicity in a Knowledge-Based Artificial Neural Network. We quantify the degree to which user preferences violate a set of assumptions. We empirically compare the KBANN network with an unbiased ANN in terms of learning rate and accuracy for preferences consistent and inconsistent with the assumptions. We go on to demonstrate how the technique can be used to learn a fine-grained preference structure from simple binary classification data.

In this paper we propose a new partial order reduction method that preserves deadlocks, and is strictly weaker than any other known method. We prove that all terminating states of the original state graph remain reachable in the reduced version. We give an example of a situation, where the method provides more reduction than established methods.

In this paper we propose a new partial order reduction method that preserves deadlocks, and is strictly weaker than any other known method. We prove that all terminating states of the original state graph remain reachable in the reduced version. We give an example of a situation, where the method provides more reduction than established methods.

 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

 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.

 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

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

In this report, we extend dynamic symbolic execution to distributed and concurrent systems. Dynamic symbolic execution can be used in software testing to systematically identify equivalence classes of input values and has been shown to scale well to large systems. Although usually restricted to sequential programs, this scalability makes it interesting to consider the technique in the distributed and concurrent setting as well. In order to extend the technique to concurrent systems, it is necessary to obtain sufficient control over the scheduling of concurrent activities to avoid race conditions. Creol, a modeling language for distributed concurrent objects, solves this problem by abstracting from a particular scheduling policy but explicitly defining scheduling points. This provides sufficient control to apply the technique of dynamic symbolic execution for model based testing of interleaved processes. The technique has been formalized in rewriting logic, executes in Maude, and applied to non-trivial examples, including an industrial case study.

The refinement calculus provides a methodology for transforming an abstract specification into a concrete implementation, by following a succession of refinement rules. These rules have been mechanized in theorem-provers, thus providing a formal and rigorous way to prove that a given program refines another one. In a previous work, we have extended this mechanization for object-oriented programs, where the memory is represented as a graph, and we have integrated our approach within the rCOS tool, a model-driven software development tool providing a refinement language. Hence, for any refinement step, the tool automatically generates the corresponding proof obligations and the user can manually discharge them, using a provided library of refinement lemmas. In this work, we propose an approach to automate the search of possible refinement rules from a program to another, using the rewriting tool Maude. Each refinement rule in Maude is associated with the corresponding lemma in Isabelle, thus allowing the tool to automatically generate the Isabelle proof when a refinement rule can be automatically found. The user can add a new refinement rule by providing the corresponding Maude rule and Isabelle lemma.

 The notion of contract was introduced to component-based software development in order to facilitate the semantically correct composition of components. We extend the form of this notion which is based on designs to capture probabilistic requirements on execution time. We show how reasoning about such requirements can be done in an infinite-interval-based system of probabilistic duration calculus.