Publications

 A promising strategy to promote good governance is the harnessing of opportunities provided by the use of mobile phones, which are widely accessible to most segments of society. A study recently presented at the International Conference on Theory and Practice of Electronic Governance, of which two authors are from the UNU-IIST Centre for Electronic Governance, investigated the strategic use of mobile technologies by governments to achieve the desired development and social inclusion outcomes. The study focused on the case of migrant head porters – local micro-logistics service providers – from Ghana. Its implications include supporting policy efforts for achieving the Millennium Development Goals on poverty alleviation and gender (specifically, women’s empowerment).

A promising strategy to promote good governance is harnessing the opportunities provided by the use of mobile phones, widely accessible to most segments of the society, for delivering public information and services and for decision-making by government. This paper investigates the design and implementation of mobile governance (MGOV) strategies for development (MGOV4D). Specifically, it presents an MGOV4D strategy framework to
support mobile Information and Communication Technologies (ICT) for development (MICT4D) projects in meeting their development objectives. The paper consists of four parts. First, it
presents a framework for determining the governance and related MGOV requirements for MICT4D initiatives. Second, it applies the framework to determine the MGOV4D requirements for a concrete case study of migrant head porters – local micro-logistic service providers from Ghana, involving the use of mobile phones to meet the porters’ livelihood needs. Third, based on the identified requirements, it presents a set of MICT4D initiatives that could be developed into MGOV4D programs to address the requirements. Fourth, it synthesizes the MGOV4D strategies that can support the inclusion objectives for the head porters and similar vulnerable groups. In the conclusions, the paper discusses how these results can support policy efforts for achieving the Millennium Development Goal 1 – Poverty Alleviation, and 3 –  Gender (specifically Women Empowerment). 

Electronic Government (e-Government) provides a means to good and better government facilitating citizen engagement, effective service delivery and improved efficiency in government functions. E-Government’s potential for contributing to good government is dependent on strong e-Leadership that is formalized in executive IT leaders and Government Chief Information Officers (GCIOs). After presenting the motivation for e-Leadership and GCIOs, the paper introduces the evolving role of GCIOs and discusses main issues for defining a GCIO system, such as readiness assessment, legal and regulatory framework, institutions, and GCIO education and development. The experience of five countries in establishing a GCIO system is presented, analyzing the regulatory framework, capacity-building programs and organizational support defined as part of such systems. Based on country experiences and the importance of national mechanisms and policies to coordinate efforts of CIOs in government through cross agency institutions and programs, the paper proposes a framework for instituting a GCIO system. The main contribution of the paper is a step by step approach for developing a GCIO system in the public sector.

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.

 This chapter gives an overview of the recent advances in GUItesting.Considering the increasing popularity and fast software development cycles (e.g.,desktop and mobile applications), GUI testing gains more importance as it allows us to verify the behavior of a system from the user’s perspective.Thus, it can quickly uncover relevant bugs, which a user could face. Traditional capture-replay GUI testing approaches do not meet the demands of developers anymore. Therefore, there is an increasing research activity in model-based GUI testing, where the user interaction behavior is simulated using a graph-based model.In the following, we outline different graphical notations to describe feasible user interactions, and methods to generate and execute test cases from these models. We discuss the benefits and limitations of the state-of-the-art in GUI testing research and give a brief outlook about new trends and possibilities to improve the GUI testing automation.

 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.

 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.

 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.

 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.

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