Publications

Hoare and He's approach to unifying theories of programming, UTP, is a dozen years old. In spite of the importance of its ideas, UTP does not seem to be attracting due interest. The purpose of this article is to discuss why that is the case, and to consider UTP's destiny. To do so it analyses the nature of UTP, focusing primarily on unification, and makes suggestions to expand its use.

The effectiveness of partial order reduction depends on the accuracy of independence and causality relations between transitions of a system. Given a concurrent system that uses synchronous communication, some of the dependency information is of local nature, whereas the rest of the information is non-local and dynamic. Accurate analysis of dependencies in a fully global manner would require traversing an unbounded number of steps into the state graph, and would thus be self-defeating for partial order reduction.

In this paper we explore the approach of using compositionality to cut the cost in analysing non-local dependency information. Non-local dependency analysis is performed only on individual components of the system, which are assumed to be relatively small transition systems. The system-level non-local dependency information of the product system is calculated directly from such information on the components.

Our work is carried out in the framework of the stubborn set method, applied to labelled transition systems. We develop the theory of stubborn sets for constructing a system using synchronisation patterns and compositional dependency relations. We show that the compositional techniques do give extra reduction on top of the more traditional approach, and in some cases this reduction is dramatic.

Component-based development allows one to build software from existing components and promises to improve software reuse and reduce costs. For critical applications, the user of a component must ensure that it fits the requirements of the application. To achieve this, testing is a well-suited means when the source code of the components is not available. Robustness testing is a testing methodology to detect the vulnerabilities of a component under unexpected inputs or in a stressful environment. As components may fail differently in different states, we use a state machine based approach to robustness testing. First, a set of paths is generated to cover transitions of the state machine, and it is used by the test cases to bring the component into a specific control state. Second, method calls with invalid inputs are fed to the component in different states to test the robustness. By traversing the paths, the test cases cover more states and transitions compared to stateless API testing. We apply our approach to several components, including open source software, and compare our results with existing approaches.

The important notion of adaptivity of a distributed information system is formalised, extending Dijkstra’s idea of self stabilisation. The formalisation quantifies the extent to which a system adapts, enabling degrees of adaptivity to be specified and hence assured in an implementation. The ideas are expressed without commitment to any particular formal notation and demonstrated on a cluster formation algorithm for mobile ad hoc networks.

The central role of ICT in development has kept the longstanding discussion on digital divide active in the international development and research community with new perspectives into how to measure and interpret this inequality. In this paper we examine the nature of the digital divide in Maldives. We investigate the digital divide across the nation, between the nation's capital and the rest of the country, the evolution of these divides with time. Finally, we attempt to identify clusters within the country that share similar digital divide concerns to inform more effective policy interventions and the basis for cultivating community of interests for Atolls. Results show significant disparity in penetrations of digital technologies; narrowing of the digital divide with time, but with significant divides remaining between the capital and the rest of the nation. Cluster analysis of Atoll ICT profiles revealed six clusters with membership independent of geographical location. The implications of these results on the ICT development policy of Maldives are finally discussed.

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.

In prime event structures with binary conflicts a branching cell is a subset of events closed under downward causality and immediate conflict relations. This means that no event inside the branching cell can be in conflict with any outside event, and no outside event can enable any inside event. It bears a strong resemblance to stubborn sets - a method used for partial order reduction of transition systems, which says that if a subset T of actions (i.e. labels) is a stubborn set at state s, then, from s on (for any state reachable by a sequence of outside transitions), no inside transition can be in conflict with any outside transition and no outside transition can enable any inside one. 

A rigorous study of the relationship between the two ideas, however, is not straightforward due to the facts that 1) stubborn sets utilise sophisticated causality and conflict relations that are beyond the expressiveness of prime event structures and binary conflicts, and 2) it is challenging how to devise a technique to identify the `right' subsets of transitions as `events' such that the derived event-based system captures exactly the causality and conflict information needed by stubborn sets.

In this paper we give a solution to the problems by providing an unfolding of labelled transition systems into configuration structures, a more general structure supporting or-causality and finite conflict, and show that each branching cell in the unfolding is actually a `long-lived stubborn set', i.e. no matter how the system evolves, the (`residue' of) branching cell is always a stubborn set.

Hoare and He’s approach to unifying theories of programming, UTP, is a dozen years old. In spite of the importance of its ideas, UTP does not seem to be attracting due interest. The purpose of this article is to discuss why that is the case, and to consider UTP’s destiny. To do so it analyses the nature of UTP, focusing primarily on unification, and makes suggestions to expand its use.

In a component-based design, a component interface specification describes the guaranteed ordering in which the component accepts calls to its provided methods and the assumption about the order in which the component calls methods it requires. Automata-based formalism is widely used for interface specification and compatibility checking of components. We extend this idea by introducing the concepts of reactive interface automata (RIA) for reactive components and active interface automata (AIA) for active components. We present a component-based architecture description language for object-oriented and service-based design in which a composite reactive component is built from a number of reactive components and active components through different operators. For the architectural operators, we provide the algorithms for constructing RIA of composite components.

The important notion of adaptivity of a distributed information system is formalised, following Dijkstra’s idea of self stabilisation. Moreover the formalisation quantifies the extent to which a system adapts, enabling degrees of adaptivity to be specified and hence assured of an implementation. The ideas are expressed without commitment to any particular semantic formalism and demonstrated on the cluster-based routing of messages in mobile ad hoc networks.

We present AutoPA, a tool to analyze and validate the consistency and functional correctness of use case designs. The tool directly generates an executable prototype from the requirements. The requirements are captured from different views of the application. Each view is constructed as UML diagram annotated with OCL specifications. Based on a formal semantics, the tool is implemented so that both syntactic and semantic consistency among the provided views can be guaranteed. Afterwards the requirements are analyzed and translated into an executable prototype, allowing the user to interactively validate the functional properties of the requirements model. We illustrate the benefits of the tool using a real-world sized example.

This volume includes abstracts of the two invited contributions and full papers of the eleven peer-reviewed contributions presented at OpenCert 2010.

Process algebras like CSP provide a convenient intermediate-level formalism for the design of concurrent systems by allowing processes to be combined in parallel in such a way that the designer abstracts synchronization mechanisms and simultaneity of events. However some purposes require potential simultaneity to be made explicit. One approach is to produce new semantics models encapsulating that information. The approach taken here is to use the standard models and the CSP tool, FDR, to simulate a process in such a way to reveal potentially-simultaneous events. The simulation is achieved by a construction that splits events into start and end events and monitors the result in a manner faithful to the original process. The method is applied to determine pairs of possibly concurrent events and to compute maximal simultaneity in a CSP design.

Digital libraries (DL) are starting to play a central role in traditional libraries as well as becoming an important tool for publishers to present and sell their products. A lot of research has been carried out to study the usability and data representation in DL and has led to the development of a variety of software packages, both commercial and open source. However, very little research has focused on formal aspects of DL. This paper describes our attempt to formally specify DL using the RAISE Specification Language (RSL). The specification methodology, inspired by the 5S Framework defined by Gonccalves et al. [7], is kept at a fairly abstract level and aims to provide a basic model of the key DL issues (digital objects, collections, users and communities) as well as their relations within the DL framework and the implication of such relations in terms of security and human-computer interactions.

Information sharing is a key capability required for one-stop and networked government. The capability enables sharing service-related information between government agencies involved in the delivery of one-stop seamless services, sharing resource-related information to facilitate whole-of-government response to emergencies, etc. As this capability is not common in traditional public administration and management, information sharing initiatives must overcome a range of technical, organizational, cultural and other barriers, which are generally difficult to overcome by individual agencies. Instead, information sharing is best addressed through the whole-of-government approach, driven by explicit information sharing policies and strategies in government. However, defining such policies is challenging. While information sharing theories identify multiple dimensions of the problem - technical, intra- and inter-organizational and political, the practice of information sharing focuses on principles, barriers, enablers, information lifecycles, organizational roles and other elements of information sharing agreements between agencies, most of which cut across different dimensions of the problem. This paper proposes a conceptual model to describe government information sharing initiatives. By integrating theoretical frameworks (e.g. multiple dimensions) and the information sharing practice (e.g. cross-agency agreements), the model provides a holistic view on the problem and highlights the main areas for policy intervention.

The current dominance of the service-based paradigm reflects the success of specific design and archi- tectural principles embodied in terms like SOA and REST. This paper suggests further principles for the design of services exhibiting long-running transactions, whose characteristic feature is that in the case of failure not all system states can be automatically restored: system compensation is required. The principles are expressed at the level of scope-based compensation and fault handling and ensure the con- sistency of data critical to the business logic by demanding (a) either the commitment of all of the 'scope' or nothing in case of failure, and (b) compensation is assured in case of failure in parent scopes. The notion of scope is expressed algebraically and design guidelines are suggested to ensure transactional processes satisfy those principles. To assist validation, the algebra is translated to Coloured Petri Nets; the principles are expressed as CTL formulae; and their bounded versions are checked with the CPN Tools. A simple but typical case study, 'Batch-ATM', is used throughout to illustrate definitions and finally to demonstrate the approach.