Publications

 In this paper we study a way to verify real-time systems using untimed model checking tools through an industrial case study with standard SPIN. We introduce a class of Duration Calculus whose formulas correspond to regular expressions over the set of special symbols, each of which is a state occurrence for one time unit or for less than one time unit. The length of a string reflects a time constraints. These regular expressions can easily be translated into untimed automata or a SPIN model. Then, we can verify real-time systems in the same way as for untimed systems with standard SPIN. The case study used in this paper is the well-known Bi-phase Mark Protocol.

consuming part in program debugging. Fault localization techniques can help to automate this task. Particularly promising are static proof-based techniques that rely on an encoding of error traces into trace formulas. By identifying irrelevant portions of the trace formula, the possible causes of the error can be isolated. One limitation of these approaches is that they do not take into account the control flow of the program and therefore miss common causes of errors, such as faulty branching conditions. This limitation is inherent to the way the error traces are encoded. In this paper, we present a new flow-sensitive encoding of error traces into trace formulas. The new encoding enables proof-based techniques to identify irrelevant conditional choices in an error trace and to include a justification for the truth value of branching conditions that are relevant for the localized cause of an error. We apply our new encoding to the fault localization technique based on error invariants and show that it produces more meaningful error explanations than previous approaches.

In recent years, an increasing amount of attention has been placed on improving access to Information and Communication Technology in the United States. With the rapidity at which broadband construction projects are dotting America, it is important to understand the social impacts of these infrastructural projects. One particularly salient issue is whether access to the Internet would decrease the involvement of youth in their home communities since youth and issues of talent retention are crucial to the long-term viability of rural communities. However, findings on this topic have been a mixed bag with some studies suggesting that the use of online social networking decreases community involvement while others have found that it may maintain or even increase community involvement. This study set out to clarify the conflicting findings and in the process, it has found support for both the displacement effect as well as an augmentation effect. The dual processes suggest that merely examining time spent on social networking sites does not provide a complete picture of the effects of Internet use on community  involvement. The nature of the interactions and the participants in the online social networking also play an important role. For rural community leaders working towards the
long-term viability of their communities, the findings suggest that efforts should be directed towards mitigating the displacement effects of Internet use while harnessing popular Internet applications such as social networking sites to augment the involvement that youth have in their home communities.

This article is presented as a response to the increasing need for rigorous impact assessment in ICT4D. The research reported here empirically examines whether ICTs enable microenterprise growth, to what degree, and under what conditions. We created two theoretical models that predict relationships between selected antecedents of ICT access, ICT use, and business growth. Using data collected through a multistage probability survey of women microentrepreneurs in Mumbai, India, we tested the models by structural equation modeling (SEM). Both models predicted a statistically significant, but limited causal relationship between access to ICTs (as the independent variable) and business growth (as the dependent variable). The theoretical model and the analytical techniques suggest that future research should pay greater attention to the specific factors that mediate the impact of ICTs on the growth of very small businesses.

As the fastest diffusing ICT in history, the mobile has attracted substantial scholarly interest. However, the historic penetration rate of the mobile phone in the developing world seems discordant with the paucity of evidence linking mobiles to productivity gains in microenterprises. In this study, we address the dilemma: we are seeing mobile phones everywhere but in the productivity statistics. We believe that there is a disconnect between mobile phone penetration rates and productivity statistics because businesses take time to learn how to exploit the technology for productivity gains. Findings from our study indicate there is latency between the time of mobile phone adoption and the time when this adoption starts to generate economic value. We estimated that it would take approximately three years for the benefits of mobile phone use in business processes to surface in the economic statistics. Practitioners and researchers should take this finding into consideration especially in the planning phase of ICT4D projects.

This paper investigates the impact of information and communication technologies, especially landline and mobile phones, computers, and Internet cafés in facilitating economic growth in the developing world. Data on access to ICTs, as well as business-relevant behaviors and attitudes, was collected by a multi-stage probability sample of women microentrepreneurs in Mumbai, India. Main findings include evidence that in urban microenterprises owned by women, business growth is a function of ICT access and is related to motivation to use ICTs for business purposes; and that the more positive a woman microentrepreneur feels about her status and power because of her business, the more she will be motivated to use ICTs in support of her business. Implications for the study of digital divides and strategies for studies of communication and technology more generally are considered.

Nowadays, governments are adopting Web 2.0 technologies for interacting with citizens, empowering them to share their views, react to issues of their concern and form opinion. In particular, social media play an important role in this context, due to their widespread use. For governments, a major technical challenge is the lack of automated intelligent tools for processing citizens’ opinion in government social media. At the same time, during the last decade, argumentation theory has consolidated itself in Artificial Intelligence as a new paradigm for modeling common sense reasoning, with application in several areas, such as legal reasoning, multi-agent systems, and decision support systems, among others. This paper outlines an argument-based approach for overcoming such challenge, combined with context-based information retrieval. Our ultimate aim is to combine context-based search and argumentation in a collaborative framework for managing (retrieving and publishing) service- and policy-related information in  government-use social media tools.

Any model for sequential programming that contains both (demonic) nondeterminism and probabilism must reveal the difference between these two well-known programs: the first assigns to some variable a fair choice between Booleans, whilst the second reverses the order by making the fair before the nondeterminism one. The interest and subtlety of those programs lies in the fact that without probability, disjoint assignments commute and so those programs might naively have been expected to be indistinguishable. Previous relational models separate them by exploiting a complex definition of sequential composition. This paper provides an alternative approach in which sequential composition is instead standard relational composition. The technical contribution that enables that to be achieved expands the binary (initial-final) state view of computation to incorporate a third state, the 'original' state which checkpoints the most recent nondeterministic choice to be mande on the basis of past probabilistic choices and so facilitates independent nondeterministic combinations to be choses against them. The resulting model has the standard relational model embedded in it by a Galois connection.

Modern software development is complex as it has to deal with many different and yet related aspects of applications. In practical software engineering this is now handled by a UML-like modelling approach in which different aspects are modelled by different notations. Component-based and object-oriented design techniques are found effective in the support of separation of correctness concerns of different aspects. These techniques are practised in a model-driven development process in which models are constructed in each phase of the development. To ensure the correctness of the software system developed, all models constructed in each phase are verifiable. This requires that the modelling notations are formally defined and related in order to have tool support developed for the integration of sophisticated checkers, generators and transformations. This paper summarises our research on the method of Refinement of Component and Object Systems (rCOS) and illustrates it with experiences from the work on the Common Component Modelling Example (CoCoME). This gives evidence that the formal techniques developed in rCOS can be integrated into a model-driven development process and shows where it may be integrated in computer-aided software engineering (CASE) tools for adding formally supported checking, transformation and generation facilities.

Compensating CSP (cCSP) is an extension to CSP for modeling long-running transactions. It can be used to specify programs of service orchestration written in a programming language like WS-BPEL. So far, only an operational semantics and a trace semantics are given to cCSP. In this paper, we extend cCSP with more operators and define for it a stable failures semantics in order to reason about non-determinism and deadlock. We give some important algebraic laws for the new operators. These laws can be justified and understood from the stable failures semantics. A case study is given to demonstrate the extended cCSP.

 Different temporal logics tend to emphasise different aspects of a hybrid system. In this paper, we study the predicative interpretation of Duration Calculus (DC) and Temporal Logic of Actions (TLA) and the link between them. A notation called generic composition is used to simplify the manipulation of predicates. The modalities of possibility and necessity become generic composition and its inverse of converse respectively. The transformation between different temporal logics is also characterised as such modalities. The formalism provides a framework in which human experience about hybrid system development can be formalised as refinement laws. A high-level durational specification can be decomposed to two durational specifications driven by an automaton. In such a stepwise design process, durational features are reduced while automaton features increase gradually. The application of the technique is demonstrated in the case study of the gas burner problem.

 Complexity of software development has to be dealt with by dividing the different aspects and different views of the system and separating different concerns in the design. This implies the need of different modelling notations and tools to support more and more phases of the entire development process. To ensure the correctness of the models produced, the tools therefore need to integrate sophisticated checkers, generators and transformations. A feasible approach to ensure high quality of such add-ins is to base them on sound formal foundations. This paper reports our experience in the work on the Common Component Modelling Example (CoCoME) and shows where such add-ins will fit. In particular, we show how the formal techniques developed in rCOS can be integrated into a component-based development process, and where it can be integrated in and provide extension to an existing successful commercial tool for adding formally supported checking, transformation and generation modules. This is published in Formal Methods and Hybrid Real-Time Systems, Essays in Honour of Dines Bjorner and Zhou Chaochen on the Occasion of Their 70th Birthdays Lecture Notes in Computer Science 4700. Keywords: Software development tool, software process, formal methods, tool design.

 A set-theoretic formalism, AOG, is introduced to support automated verification of pointer programs. AOG targets pointer reasoning for source programs before compilation (i.e. before removal of field names). Pointer structures are represented as object graphs instead of heaps. Each property in AOG is a relation between object graphs and name assignments of program variables, and specifications result from composing properties. AOG extends Separation Logic's compositions of address-disjoint separating conjunction to more restrictive compositions with different disjointness conditions; the extension is shown to be strict when fixpoints are present. A composition that is a "unique decomposition" decomposes any given graph uniquely into two parts. An example is the separation between the non-garbage and garbage parts of memory. Although AOG is in general undecidable, it is used to define the semantics of specific decidable logics that support automated program verification of specific topologies of pointer structure. One logic studied in this paper describes pointer variables located on multiple parallel linked lists. The logic contains quantifiers and fixpoints but is nonetheless decidable; it is applied to the example of in-place list reversal for automated verification. The Schorr-Waite marking algorithm is also considered. The technique of unique decomposition is particularly useful for establishing laws such logics.

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 this paper, we study the predicative semantics of different temporal logics and the relationships between them. We use a notation called generic composition to simplify the manipulation of predicates. The modalities of possibility and necessity become generic composition and its inverse of converse respectively. The relationships between different temporal logics are also characterised as such modalities. Formal reasoning is carried out at the level of predicative semantics and supported by the higher-level laws of generic composition and its inverse. Various temporal domains are unified under a notion called {\em resource cumulation}. Temporal logics based on these temporal domains can be readily defined, and their axioms identified. The formalism provides a framework in which human experience about system development can be formalised as refinement laws. The approach is demonstrated in the transformation from Duration Calculus to Temporal Logic of Actions. A number of common design patterns are studied. The refinement laws identified are then applied to the case study of water pump controlling.

Compensating CSP (cCSP) is an extension to CSP for modeling long-running transactions. It can be used to specify programs of service orchestration written in a programming language like WS-BPEL. So far, only an operational semantics and a trace semantics are given to cCSP. In this paper, we extend cCSP with more operators and define for it a stable failures semantics in order to reason about non-determinism and deadlock. We give some important algebraic laws for the new operators. These laws can be justified and understood from the stable failures semantics. A case study is given to demonstrate the extended cCSP.