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.

 This document provides an informal and conceptual presentation of what is a manufacturing enterprise. As this domain is vast, the native adopts a certain level of abstraction. It discusses the enterprise in terms of its four main function; namely: marketing, administration, finance, and especially, production. Each stage elaborates on the purpose (what the system is intended for), behaviour (what the system does), and structure (what makes it do what it does) of the systems in question. It aims to be a starting point for more extensive and detailed domain analysis of a manufacturing enterprise.

 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 present a method for systematic examination and reduction of the state space of distributed systems. The approach exploits properties of distributed systems to partition processes into atomic transitions and uses observations about partial orders among the distributed components to perform dynamic partial order reduction for state space reduction. This paper concentrates on preserving reachability checks and deadlock detection for a fixed input of the system. We present a search algorithm with a succinct representation of the search stack that requires only the current state in memory. We furthermore define characteristics to determine independent blocks of processes and propose and evaluate heuristics to guide the search to further state space reduction. In combination with dynamic symbolic execution (also known as concolic execution), the approach also allows the generalization of a concrete run and gives rise to examination of the full input state space of a distributed system.

 This technical report contains the papers presented at Refine 2006, the International Refinement Workshop. This compendium is the preliminary proceedings for the workshop for the convenience of the workshop participants; the official proceedings will be published after the workshop in Electronic Notes on Theoretical Computer Science

 One of the fundamental problem in concurrency and synchronisation study is the wait-free construction of atomic registers. Atomicity simplifies programming by conjuring up an illusion of exclusive use of shared registers by concurrent processes; whereas wait-freedom improves the efficiency by guaranteeing that every process can proceed at its own speed, i.e. without being blocked by or needing to wait for other processes, even when they are accessing the same register simultaneously.

Much research work has been devoted to the study of the problem since Lamport and Peterson first posed it in the 70s. A plethora of ingenious algorithms has been discovered in the 80s and 90s, along with the invention of some of the classic techniques for concurrency and synchronisation, e.g. bounded timestamping techniques. Nowadays these algorithms and techniques become the foundation of scalable synchronisation research for modern multicore programming.

Despite the importance of the problem there is few substantial survey work done to summarise the field. Vitanyi published a very well-written note recently to retrace some of the history and recall some of the major results and steps to its solution [48]. Inspired by his work, we attempt in this report to give a more in-depth survey by 1) compiling a more comprehensive list of algorithms for atomic register construction, 2) organising and classifying the algorithms in a cube-like structure, and 3) providing a more accessible analysis on the classic techniques of bounded timestamping.

 Design with reuse typicaly accepts only those components in the repository which succesfully match a given query specification, otherwise tries to obtain the needed components by adaptation, composition or programming. The purpose of this paper is to describe how it is possible to formalise design which can also accept imperfect components - satisfying one in a chain of increasingly weak specifications. We also capture the effect using such imperfect components has on the overall design, its controlled degradation, and discuss how the approach can support a design method based on the incremental upgrading of imperfect components.

 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.

 We present Joogie, a tool that detects infeasible code in Java programs. Infeasible code is code that does not occur on feasible control-flow paths and thus has no feasible execution. Infeasible code comprises many errors detected by static analysis in modern IDEs such as guaranteed null-pointer dereference or unreachable code. Unlike existing techniques, Joogie identifies infeasible code by proving that a particular statement cannot occur on a terminating execution using techniques from static verification. Thus, Joogie is able to detect infeasible code which is overlooked by existing tools. Joogie works fully automatic, it does not require user- provided specifications and (almost) never produces false warnings.

 Graphical user interfaces (GUIs) are a common way to interact with software. To ensure the quality of such software it is important to test the possible interactions with its user interface. GUI testing is a challenging task as they can allow, in general, infinitely many different sequences of interactions with the software. As it is only possible to test a limited amount of possible user interactions, it is crucial for the quality of GUI testing to identify relevant sequences and avoid improper ones. In this paper we propose a model for better GUI testing. Our model is created based on two observations. It is a common case that different user interactions result in the execution of the same code fragments. That is, it is sufficient to test only interactions that execute different code fragments. Our second observation is that user interactions are context-sensitive. That is, the control flow that is taken in a program fragment handling a user interaction depends on the order of some preceding user interactions. We show that these observations are relevant in practice. We present a preliminary implementation that utilizes these observations for test case generation.

Recently, software verification is being used to prove the presence of contradictions in source code and thus reveal potential weaknesses in the code or provide assistance to the compiler optimization. Compared to verification of correctness properties, the translation from source code to logic can be very simple and thus easy to solve by automated theorem provers. In this paper, we present a translation of Java into logic that is suitable for proving the presence of contradictions in code. We show that the translation, which is based on the Jimple language, can be used to analyze real-world programs, and discuss some issues that arise from differences between Java code and its bytecode

Graphical user interfaces (GUIs) are a common way to interact with software. To ensure the quality of such software it is important to test the possible interactions with its user interface. GUI testing is a challenging task as they can allow, in general, infinitely many different sequences of interactions with the software. As it is only possible to test a limited amount of possible user interactions, it is crucial for the quality of GUI testing to identify relevant sequences and avoid improper ones. In this paper we propose a model for better GUI testing. Our model is created based on two observations. It is a common case that different user interactions result in the execution of the same code fragments. That is, it is sufficient to test only interactions that execute different code fragments. Our second observation is that user interactions are contextsensitive. That is, the control flow that is taken in a program fragment handling a user interaction depends on the order of some preceding user interactions. We show that these observations are relevant in practice. We present a preliminary implementation that utilizes these observations for test case generation.