Publications

In the last two decades, hand-in-hand with strong economic growth, Southeast Asia has experienced a strengthened academic community as well as an increase in public and private research and development. But, because the level of research activity and maturity of the research environment in Southeast Asian countries is varied and has been changing rapidly in recent years, public perceptions of the amount and relevance of the research output can often be inaccurate. This gives particular emphasis to the need for data to support decisions concerning collaborative research programmes.

The recent intense two-week meeting on trade in endangered species has been described as a failure in many newspapers and blogs, principally because member countries could not reach an agreement on new trade measures to protect certain marine species.

The fifteenth Conference of the Parties (COP15) to the Convention on International Trade in Endangered Species of Wild Fauna and Flora ( CITES) held in Doha, Qatar, included an unprecedented number of proposals regarding commercially exploited aquatic species... 

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

In the area of concurrent, communicating systems, a common approach to verify the absence of design faults is in terms of an equivalence relation between a high-level and a low-level process. One such relation is bisimulation and this holds if two processes cannot be distinguished by observing them for a finite interval of time. However, the absence of design faults does not guarantee that the process will behave correctly in practice as it depends on various hardware devices which may be subject to physical faults themselves. Such faults cannot be avoided; they must be tolerated. The purpose of this thesis is to provide a formal framework, based on bisimulations and using the Calculus of Communicating Systems, by which we can specify, design and verify concurrent, fault-tolerant systems, with emphasis placed on reasoning and design under weak assumptions about faults. The framework is described below. As the formalmodel we use labelled transition systems and we introduce additional ‘faulty transitions’ to represent the effects of faults. This leads to a semantic theory of fault tolerant bisimulations under which faulty transitions are possible for a low-level process but not for the high-level one. Corresponding to faults being unpredictable, the theory is fault-monotonic: after verifying correctness for a number of faults, correctness for some, or even none of them is guaranteed. As a process description language we use a version of CCS where recursion involves locally declared constants. The language is assigned different semantics, each taking an additional declaration, as part of the fault description language, to specify effects of faults. It is then possible to verify fault-tolerance by using process transformations and ‘normal’ bisimulations, and to verify correctness in the presence of multiple faults (specified by several declarations) using composition of faults. The more faults are anticipated, the more difficult is to ensure that they are all tolerated. This and the fault-monotonic property suggests to establish fault-tolerance by incremental refinement, for an increasing variety of faults. We also show how to apply this refinement compositionally and provide a number of fault-tolerance-preserving transformations. The framework is illustrated by a few examples, including communication protocols, stable storage, distributed consensus and a distributed database service which supports atomic transactions despite faults in the underlying storage and communication devices.

Seamless Government is a new paradigm for public administration that promotes collaboration and networking between government agencies and between public, private and voluntary sectors as a way to better respond to the needs of citizens, businesses and other arms of government. There are many benefits of collaboration in government. One is the delivery of Seamless Public Services, made available through one-stop access points, both electronic and traditional, according to the needs of customers and not the internal structure of government. Another is improved efficiency in government, aiming at eliminating duplicate efforts and making better use of scarce public resources. However, the paradigm presents numerous implementation challenges: (1) Legal - recognizing electronic processes as equivalent to paper-based processes; (2) Financial - funding multi-annual, cross-agency projects; (3) Social – building human capacity able to utilize new technologies; (4) Organizational - establishing processes that seamlessly cross organizational boundaries; and (5) Technological – building solutions that integrate software and processes across organizational and administrative boundaries, able to adapt to changing legal and organizational requirements.

This thesis presents the concept and foundations of Programmable Messaging – a paradigm for automated exchange of messages between collaborating entities to respond to diverse communication needs of complex and dynamic collaborative environments, such as the environments characterizing Seamless Government. It also presents a concrete realization of Programmable Messaging – Government-Enterprise Ecosystem Gateway (G-EEG). G-EEG is a high-level communication and coordination platform to support collaboration across multi-organizational processes and applications. The requirements for G-EEG were identified following two studies: on the nature of collaborations between agencies, following a survey of public administration system in Macao, and on available technical solutions to enable such collaborations. In order to implement these requirements, G-EEG comprises three components:

1) G-EEG-CORE - a run-time messaging framework that enables asynchronous exchange of messages between registered members along dynamically created and subscribed channels;

2) G-EEG-EXTEND - a repository of horizontal (process-independent) and vertical (process-dependent) extensions and a mechanism to dynamically enable such extensions on top of G-EEG-CORE; and

3) G-EEG-DEVELOP - a development framework to rigorously specify, design and verify messaging extensions, from the scratch or from existing extensions.

G-EEG was designed to be: minimalist – based on the smallest possible number of concepts; extensible – the rich functionality required by applications is available through extensions in the G-EEG-EXTEND repository or through the G-EEG-DEVELOP development framework; dynamic - communication structures can be dynamically created and modified at run-time; and reliable – parts of the framework are based on a formal model, enabling rigorous development of new extensions. G-EEG can be used by government agencies to exchange messages through carefully managed logical communication channels, with necessary extensions enabled over them. Based on G-EEG concepts, a research prototype was built through rigorous use of modelling and analysis in various development stages.

The main contributions of the thesis are: (1) the concept of Programmable Messaging, (2) the definition, formalization and implementation of G-EEG as a concrete realization of Programmable Messaging, (3) a formal model for XML and XML family of technologies resulting from the formalization effort; (4) a comprehensive survey of the concepts and challenges of Seamless Government, (5) rigorous assessment of G-EEG with respect to Seamless Government, and (6) a framework for assessing organizational, technological and foundational solutions to Seamless Government. 

 Reports on the status of UNU-IIST and its activities after the first 6 months of operation 

 The programme and project mission of {\sf UNU/IIST}\ is reviewed, as are the policies according to which {\sf UNU/IIST}\ offers fellowships and engages in joint research projects and in advanced development projects with institutions in developing (and other) countries. We then detail all the programmatic activities that took place during 1995 --- with this review forming a major part of this report. A special emphasis is paid to Macau\--oriented actions. The ongoing relations between {\sf UNU/IIST}\ and the {\sf UN}\ System (\&c.) as such are briefly reviewed, as is the status of personnel, finances \& budget. Extensive reference is made both to internal {\sf UNU/IIST}\ documents and to {\sf UNU/IIST}\ reports and research and technical notes. Programmatic activity, staffing, budget and other plans for the 1996\--1997 Biennium are covered throughout

 Over the last decade, the importance of Free/Libre/Open Source Software (FLOSS) has increased dramatically and the size and scope of the OSS conference within which this workshop takes place is testament to that reality. This volume contains the proceedings of the joint workshop: the first International Workshop on Foundations and Techniques bringing together Free/Libre/Open Source Software and Formal Methods (FLOSS-FM 2008) and the second International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2008). All submitted papers have been reviewed by at least 3 Program Committee members. The aim of the workshop has been to bring together researchers from academia and industry, firstly, to study the question of FLOSS certification and, secondly, to explore in the largest possible sense the question of how formal methods can be brought more successfully to bear on the open source phenomenon, and also how FLOSS can be brought more fully into the formal methods community. The organisers would like to take this opportunity to thank the contributors, the programme committee and all the referees for their interest and hard work. We leave to the reader the seeds the participants have sown.

 Preliminary proceedings of the papers presented at the TTSS'08 workshop for the convenience of the workshop participants. A selection of revised papers will be published in Electronic Notes in Theoretical Computer Science by Elsevier.

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.

 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.

 The research on hybrid control systems attracts many scientists both in computer science and control theories and applications. The study should be carried out on a general framework abstracted from various hybrid control systems. This paper analyses the drawbacks of the present frameworks used by most researchers and proposes a new framework to overcome these shortcomes. The new framework consists of a discrete time box, a discrete event box and a digital-symbol interface. The new framework shows the crucial nature of the hybridity of time envolving variables and event driven variables in hybrid control systems. The new framework is easy to integrate the knowledges of computer science and control theories and applications. Two examples, a gas burner and an inverse pendulum are given to show the fitness of the new framework. The design and analysis aspects of hybrid control systems related to the new framework are also discussed.