Publications

The book describes 12 case studies which use RAISE (Rigorous Approach to Industrial Software Engineering) to con- struct, analyse, develop and apply formal specifications. The case studies present a wide range of application areas: authentication of communications protocols, error detection in programs, geographic information systems, library management, multi-lingual documents, production planning, run-time verification, software design patterns, software reuse, taxation management, telephony, and travel planning. Most have little or nothing to do with safety-critical systems, traditionally considered as the area in which formal methods are most applicable, and many of them do not involve verification. The cases studies illustrate diverse uses of formal specifications: to capture requirements for new software, to carry out software development from requirements, to formalise algorithms in order to prove their correctness, to check if software behaves correctly at run-time, to build models of application domains, to relate descriptive and prescriptive models, to formalise notations for software development, and various other uses. They also try to put the task of creating formal specifications into perspective, asking questions about the purpose, scope and use of the formal models before the models are built.

The case study chapters have each been written by one of this book's editors. Each case study describes work done at the United Nations University's International Institute for Software Technology (UNU-IIST) in Macau by that editor in collaboration with fellows (lecturers or post-graduate students from developing countries). Each case study chapter concludes with information about the fellows involved, the relevant UNU-IIST technical report(s), and other related work.

The goal of implementation verification is to prove that a given program behaves correctly under all possible executions, for instance that it produces correct output for all legal inputs. There are several conditions on carrying out such verification in practice: (1) the implementation is available in a form suitable for analysis; (2) the implementation “size” is such that the proof remains feasible; (3) it is written in a language which supports specification and proof; and (4) there is enough human expertise to guide the proof. Such conditions are often not satisfied in practice. Result verification is a possible alternative. It relies not on the implementation of the program but on its execution record. This record may be a sequence of inputs and the corresponding outputs from the program when it computes a certain function, or a sequence of values observed about the changing state of the program as it interacts with its environment, or perhaps such values augmented with time-stamps. Whatever the form, the goal is to decide if this record describes a correct execution of the program. A positive answer does not mean that the program is fault-free, only that this execution did not exhibit any errors. On the other hand, finding an error is like constructing a counter-example for claims of correctness about the program. Due to its modest goals, result verification has several advantages over implementation verification: (1) It can be carried out off-line, after the execution terminates, or on-line, as the execution unfolds; (2) Its application scope includes both off-the-shelf components (binary files) and remote service providers (distributed objects); (3) Due to the simple structure involved (a sequence of states), it is easier to automate; and (4) Based solely on the execution record, its complexity is largely independent of the “size” of the implementation and the language used, which makes it particularly suitable for complex, heterogeneous systems. In this chapter we propose a technical framework for carrying out automated result verification in practice: 1. The execution record is a simple text file. Many programs produce such files during their normal operations, for administrative purposes. A general technique for recording exactly the information needed for verification, is to introduce a program monitor by wrapping. 2. The execution record is given as input to the verifier program, which does the actual verification. Given the execution record in a text file, we consider result verification as a text-processing task. Accordingly, the verifier is written in AWK, which is a special-purpose language for text processing [121]. Verification is done by the AWK interpreter, given the execution record and the verifier program as inputs. 3. The verifier program is not written by hand but specification-generated. The generator takes the property the verifier should check, called result specification, as input and produces the code of the verifier program as output. The specification-to-verifier generator is itself written in AWK. 4. A result specification is a first-order property built with two kinds of variables, state and record variables, using the functions and predicates over their respective types. A record variable refers to the contents of the record file. A state variable allows the calculation of the values that are not written in the record file but are derived from it. For each state variable we define its type, initial value and how this value changes for different operations invoked. We also allow specifications to be combined. The rest of the chapter is as follows. Section 12.2 shows how to model the behaviour of a program. Section 12.3 describes how to wrap a program to record the relevant observations during its execution. Result verification, using a hand-written verifier program, is the subject of Section 12.4. Section 12.5 defines a result specification. Section 12.6 describes various ways such specifications can be combined. Section 12.7 describes the generator which produces the code of the verifier program given the specification. Section 12.8 contains an example and Section 12.9 presents some conclusions.

Object-based distributed systems challenge the traditional ways of applying formal methods via specification and proof. One of the problems is the large number of the components involved, partly decided at compile time (static invocation) and partly at run-time (dynamic invocation). Another problem is having to rely on the vendor’s claims about correctness of individual components, without being able (lacking implementation details) to verify such claims ourselves. Yet another is expressing component specifications in interface definition languages, which describe how to communicate with a component (syntax), but not the expected results of such communication (semantics). Such problems make static verification difficult, at best. On the other hand, the structuring of the whole system in terms of the independent, distributed components, is particularly suitable for making such a system fault-tolerant [85]. The goal is to ensure that failures of individual components (violation of their specifications) will not cause the whole system to fail (violation of the system’s specification). The latter specification can be used at design-time to prove if the system is indeed fault-tolerant. The former specifications can be used at run-time to detect if components have failed. This chapter describes an approach to formally specify software components in order to make such error detection possible. Defining such specifications is not without problems. Specifications may contain infinite constructs like quantifiers (for all values of a type), liveness properties (for all states in a sequence) or modal properties of branching time (for all transitions from a state). Such constructs are generally non-executable and non-checkable. This means we cannot execute them directly on the machine and we cannot check effectively at run-time that they indeed hold. On the other hand, specifications based on propositional logic which can be checked at run-time, are insufficiently expressive in practice. Also, checking specifications which use equality of states is not possible when the state can be only accessed via defined operations; the best we can do is checking observational equivalence [97]. Such problems require a different kind of specification to carry out effective run-time checking from those to support static verification. In this chapter we propose an approach to define and check such specifications at run-time. Technically, the approach is as follows: 1. Specifications are formally-based. They are defined as logic-based regular expressions built from the propositions about the states or pairs of states of a component, via its observer operations. 2. Specifications are checkable at run-time, based on the recorded history of the component’s execution. This history is a sequence of values observed about individual states and the operations, with arguments, whose invocation caused state-changes. 3. Checking is carried out by a wrapper which is generated from the component and its specification. The wrapper takes over all communication between the component and its environment. It remains transparent to the clients except being able to detect (as it carries out run-time checking after every state-change) and announce (via the additional boolean observer error) the occurrence of an error. 4. The required effect of run-time checking is described formally as the fail-stop property. The wrapper generator is to transform a given component, which may fail in an arbitrary way, into a component which only fails by refusing to operate, which fact is also announced by the observer error. The rest of this chapter is as follows. Section 13.2 explains and illustrates the concept of a ‘component’. Section 13.3 discusses and compares ‘fault-free’ and ‘fail-stop’ behaviours of components. Section 13.4 shows how to ensure fail-stop behaviour by pattern matching. Section 13.5 presents an example, a line editor. Sections 13.6 and 13.7 describe how pattern matching can become part of an automatically generated wrapper. Section 13.6 specifies the wrapper generator and Section 13.7 describes a prototype implementation. Section 13.8 provides some conclusions.

Business process modelling can have many applications. It can be used to: understand the flow of work in an organisation; monitor and control progress of work; measure and optimise work performance; predict the effects of changes in management and operations; plan for implementation of changes; design interaction patterns between processes running in different organisations; and specify, develop and deploy software to further organisational/business goals, etc. Formal analysis is a particularly good reason to carry out such modelling, as it can disclose problems long before the process is actually deployed in an organisation. This early detection is especially important for processes that cross organisational boundaries where errors, as in all distributed systems, are inherently hard to detect and expensive to correct. One approach to model a business process is to describe its concrete execution in an enterprise, using enterprise resources to produce tangible results like products or services. Typically, such descriptive modelling would be carried out to explore the analogy between business and computing and would concentrate on the mechanics of a process. A prescriptive model, in contrast, aims to express the intended purpose of each process. The challenge for business process modelling is, we believe, finding suitable abstractions that can be applied at both levels. By formally relating such descriptive and prescriptive models, we could verify if a process is correct (satisfies its intended purpose) and further develop an engineering approach to design such processes in a rigorous way. This chapter is set to contribute to this general goal. We consider a particular, although broadly defined, business domain: customer-driven production. Production refers to the process of creating goods – tangible products like cars, phones or shovels. Products are produced by assembly from sub-products, carried out within independent business entities called production cells. Each cell contains the resources to store, manufacture and deliver products to its customers. On a certain level, a cell represents formally what is a manufacturing enterprise with its resources like a warehouse, shop-floor and product stocks. The behaviour of a cell is driven by the orders received from the customers and how such orders are implemented. The customers include other production cells. The implementation of a customer order is described by a production process. The aim of this chapter is to define formally what it means for such a process to be feasible (possible to carry out given the resources delegated for its execution) and correct (satisfying a customer order, if feasible). We adopt the following business model, explained for sequential, concurrent and distributed production: 1. Sequential production (one process, one cell). Each process responds to a customer order which specifies the product to deliver, the number of items and possibly the latest time of delivery. The process operates within a production cell which offers the resources for its execution, in terms of product stocks, storage space, and capacity to carry out manufacturing and transportation. It describes in detail what operations should be performed on the cell and in which sequence. The process is feasible if the cell has enough resources for its execution. A feasible process is correct if its execution satisfies the order: the stocks for the products reach the required volumes within the deadline. 2. Concurrent production (many processes, one cell). A cell may contain several processes, each created in response to a particular customer order and all executed concurrently. In order to resolve conflicts for the shared resources (such as product stocks, manufacturing workstations or a transportation system), processes are assigned priorities to represent their importance. Feasibility means the cell has enough resources for all such processes, executed concurrently. Correctness means all processes satisfy their corresponding customer orders, when executed concurrently under a priority-based scheduler. 3. Distributed production (many processes, many cells). Several processes running in different cells may satisfy an order in a cooperative way. Trying to utilise the resources that one cell lacks and another has available, they form customer-supplier relations dynamically, by receiving customer orders and implementing with their own processes, perhaps sending more orders at the same time. As a result, each cell may be running several processes, each contributing part of the original order. This mechanism leads to the distribution of production activities. Feasibility means each cell has enough resources for its processes executed concurrently. Correctness means a process satisfies its customer order provided all supplier processes satisfy their own. Moreover, when several such processes run in the same cell, they must satisfy their orders concurrently. The rest of this chapter is as follows. Section 7.2 is about product modelling. Section 7.3 presents a descriptive production model, including the concepts like production cells, operations and processes, and defines what it means for a process to be feasible. Section 7.4 presents a corresponding prescriptive model. Section 7.5 defines what it means for a feasible process to be correct, by relating such descriptive and prescriptive models. It starts with sequential production, then introduces concurrency, distribution, and real-time constraints. Section 7.6 describes related work and provides some conclusions.

Electronic Government leads to technology-enabled transformation of government organizations, and consequently of their relationships with citizens, businesses and other arms of government. Developing countries can greatly benefit from Electronic Government development, in terms of increasing the capacity of government organizations to meet tremendous socio-economic needs. However, they also face common challenges: weak implementation, delivery and coordination; policy-strategy and strategy-implementation gaps; insufficient human capacity; lack of research to precede project implementations; etc. This paper proposes a rigorous Electronic Government Development Framework (EGOV.*) to address some of these challenges. The framework enables systematic construction of Electronic Government for a given Public Administration (PA) in terms of: (1) establishing the readiness of the PA for ICT-enabled transformation; (2) determining state-of-the-art in Electronic Government practices and solutions around the world, as relevant to the PA; (3) building a PA-wide vision and strategy towards the development of high-quality Electronic Government; (4) constructing a government program to implement this strategy; (5) building human capacity within the PA, covering leadership, management and technical skills, to be able to execute and benefit from this program; and (6) establishing a Resource Center for Electronic Government on the basis of existing institutions, particularly government and academia, and raising the capacity of this Center to execute the program. The framework has been applied in three countries - one completed, one ongoing, and one to start.

Information sharing (IS) is a key capability required for one-stop and networked government, responding to a variety of intra-organizational, inter-organizational, or cross-national needs like sharing service-related information between parties involved in the delivery of seamless services, sharing information on available resources to enable whole-of-government response to emergencies, etc. Despite its importance, the IS capability is not common for governments due to various technical, organizational, cultural, and other barriers which are generally difficult to address by individual agencies. However, developing such capabilities is a challenging task which requires government-wide coordination, explicit policies and strategies, and concrete implementation frameworks. At the same time, reconciling existing theoretical frameworks with the IS practice can be difficult due to the differences in conceptions and abstraction levels. In order to address such difficulties, this chapter proposes a conceptual framework to guide the development of Government Information Sharing (GIS) policies, strategies, and implementations. By integrating theoretical frameworks and the GIS practice, the framework adopts a holistic view on the GIS problem, highlights the main areas for policy intervention, and provides policy makers and government managers with conceptual clarity on the GIS problem.

Better integration of Electronic Government (EGOV) and Public Administration Reform (PAR) strategies has been identified by global EGOV benchmark reports as one of the contemporary issues to address in improving the outcomes of EGOV programs. This chapter presents a technique for aligning EGOV and PAR strategies based on the Strategic Alignment Model (SAM) of Henderson and Venkatraman. By treating EGOV and PAR strategies as two different alignment domains, similar to organizational and technological domains respectively, we re-frame the original SAM to address our specific alignment needs. Our model provides a procedure and metrics for analyzing: (1) alignment between a pair of EGOV and PAR strategies and (2) the internal coherency of an EGOV strategy. We discuss our experience in applying this approach in Macao and conclude with how it may be used in aligning EGOV with other strategies such as those related to governance and development.

This paper presents a Minitrack on Development Methods for Electronic Government, organized as part of the Electronic Government Track at the 42nd Hawaii International Conference on System Sciences (HICSS-42), 5-8 January 2009, Big Island, Hawaii. The minitrack focused on development methods, including technical, managerial and organizational dimensions, to address various challenges facing Electronic Government development: dependability and accessibility, evolving requirements, adherence to law and regulations, multi-channel service delivery, technical and organizational complexity, dependence on ever-changing legal and operational environments, etc. Of particular interest are contributions that can make Electronic Government development more measurable, predictable, replicable and scalable, contributing to the establishment of theoretical foundations and engineering practices for the domain.

The three papers accepted by the minitrack were: (1) “Government Enterprise Architecture Grid Adaptation in Finland” co-authored by Katariina Valtonen, Ville Seppänen, and Mauri Leppänen; (2) “Developing User Requirements for Transnational Government Information Systems” co-authored by Philip Seltsikas and Nikolaos Papas; and (3) “(Semantic) Model-driven Development for Electronic Government Applications” co-authored by Aadya Shukla, Charles Crichton, Jim Davies, Steve Harris, and Andrew Tsui.

This paper presents a Minitrack on Development Methods for Electronic Government, organized as part of the Electronic Government Track at HICCS43 - 43rd Hawaii International Conference on System Sciences (HICSS-43), 5-8 January 2010, Koloa, Hawaii. The minitrack focused on development methods, including technical, managerial and organizational dimensions, to address various challenges facing Electronic Government development: dependability and accessibility, evolving requirements, adherence to law and regulations, multi-channel service delivery, technical and organizational complexity, dependence on ever-changing legal and operational environments, etc. Of particular interest are contributions that can make Electronic Government development more measurable, predictable, replicable and scalable, contributing to the establishment of theoretical foundations and engineering practices for the domain.

The six papers accepted by the Minitrack were: (1) “A Goal Oriented and Knowledge Based e-Government Project Management Platform” by Demetrios Sarantis, Yannis Charalabidis and Dimitris Askounis; (2) “Simulation Games for the Collaborative Development of Multichannel Public Service Delivery” by Bram Klievink and Marijn Janssen; (3) “Can e-Government Adopters Benefit from a Technology-First Approach? The Case of Egypt Embarking on Service-Oriented Architecture” by Ralf Klischewski and Ranwa Abubakr; (4) “EA as a Tool for Strategic Planning – a Case Study of a Local Government” by Katariina Valtonen, Ismo Korhonen and Riku Rekonen; (5) “On Mapping Business Document Models to Core Components” by Michael Strommer, Christian Pichler and Philipp Liegl; and (6) “Semantic Interoperability in Practice” by Aadya Shukla, Steve Harris and Jim Davies.

Travel planning can be a challenge these days. There is an abundance of travel-related information in the magazines, newspapers, guides, brochures, on the internet. The information covers all imaginable aspects of travel including flights, hotels, cars, restaurants, maps, events and others. Travel is offered in the form of individual products or complete packages, its contents predefined or customised to individual needs, definite or based on waiting lists, sold for a regular price or as special deals (under different restrictions when, where and for whom the deal applies). With so many options available and so many constraints involved, there is a great deal of uncertainty how to carry out the process of travel planning. Internet contributes significantly to making this information available for individual travellers, including on-line availability-checking, reservations and sale. However, internet-based travel agents tend to focus more on the presentation of information and less on its actual contents. Moreover, they implement little in the way of a method for the process of systematic travel planning – formulating the requirements and then moving gradually toward the solution. Here are some observations when visiting such agents: (1) a visitor has to know in detail what service he looks for before he can learn this for himself; (2) when presented with an offer a visitor can only accept or reject it, but cannot explore the alternatives; (3) an error message communicates to the visitor the presence of an error but not the reasons for it or how to avoid it; (4) there is no recollection of previous interactions with a visitor – the system always returns to its pre-defined state; (5) when a little amount of automation is possible in support of visitors’ decisions it is not implemented. This chapter is about methods and tools in support of travel planning. We show how to approach travel planning as essentially an engineering problem. We define precisely what constitutes travel requirements, what is a travel plan, and in what sense the plan correctly implements the requirements. The approach is model-based, with models representing all stages of travel planning, from abstract requirements to concrete itineraries. Such models are designed, analysed and redesigned to represent decisions made by the travel engineer (the person who designs the travel plan). The models are minimal – expressed with the minimum number of modelling concepts – but also open-ended – new concepts can be added when needed. They are also formally-based – their syntax is well-defined and their semantics is expressed in precise mathematical terms, using numbers, sets, maps, functions, abstract and concrete types. The formal machinery used for semantic definitions is basic set theory and logic. Formality makes it possible to prove correctness of a travel plan with respect to travel requirements, and also to justify the soundness of the design rules that allow travel plans to be made more concrete. Such rules are applied during a development process, leading gradually from the abstract travel requirements to concrete solutions. We present such rules and discuss their soundness. In presenting such models we have four goals in mind. First, we want to formalise some of the travel-related concepts in a way which is independent of the current technology, providing the basis for an engineering approach. The latter means that the models must capture different levels of abstraction as well as relate those levels by the concept of correctness. Second, we want to apply such models to define a formally-based method for systematic travel planning, including definitions of the design rules and justification of why they are sound. Third, we want to explore the opportunities and limitations for automation in support of travel-related decision-making. The models will be used to formulate precise problems and seek possibly automated solutions. Fourth, we would like to seek an implementation of a prototype travel assistant, based on the models, in support of the method. The rest of this chapter is as follows. Section 8.2 introduces the basic concepts. Section 8.3 describes the models for travel planning, with definitions and examples. As the models capture different levels of abstraction, Section 8.4 defines what it means for a concrete travel plan to correctly implement an abstract plan. Section 8.5 presents a method for systematic travel planning, based on the models in Section 8.3 and the notion of correctness in Section 8.4. Section 8.6 describes the ideas for a travel assistant, a software system to support travel development. Finally, Section 8.7 contains some conclusions.

Formal methods have grown out of their infancy: firm foundations are established, a variety of languages are available to describe specifications at different levels of abstraction, and methods and calculi exist to guide development of specifications into correct programs, supported by a wide range of tools. There is also a growing number of well-documented experience reports and case studies which present stories and analyses of both successful and less successful applications. A further evidence for maturing of formal methods is their increasing presence in industrial, large-scale software development. Faced with realistic expectations, they become integrated into the industrial software development process in such a way as to complement, not replace, traditional methods of software design and analysis. The purpose of this book is to present our experience in developing and applying formal specifications. The book describes 12 case studies which use RAISE – Rigorous Approach to Industrial Software Engineering – to construct, analyse, develop and apply formal specifications. The case studies present a wide range of application areas: authentication of communications protocols, error detection in programs, geographic information systems, library management, multi-lingual documents, production planning, run-time verification, software design patterns, software reuse, taxation management, telephony, and travel planning. Most have little or nothing to do with safety-critical systems, traditionally considered as the area in which formal methods are most applicable, and many of them do not involve verification. The case studies illustrate diverse uses of formal specifications: to capture requirements for new software, to carry out software development from requirements, to formalise algorithms in order to prove their correctness, to check if software behaves correctly at run-time, to build models of application domains, to relate descriptive and prescriptive models, to formalise notations for software development, and various other uses. They also try to put the task of creating formal specifications into perspective, asking questions about the purpose, scope and use of the formal models before the models are built. The case study chapters have each been written by one of this book’s editors. Each case study describes work done at the United Nations University’s International Institute for Software Technology (UNU/IIST) in Macau by that editor in collaboration with “fellows” – lecturers or post-graduate students – from developing countries. Each case study chapter concludes with information about the fellows involved, the relevant UNU-IIST technical report(s), and other related work. This introduction consists of six sections. Section 1.1 describes some factors promoting the application of formal specifications in industry. Section 1.2 presents some paradigms for software development which require the use of formal or semi-formal specifications. Section 1.3 gives a high-level overview of specification languages, development methods and tools. It concludes with a summary description of RAISE. Sections 1.4 and 1.5 contain respectively an overview of the case studies in the book and a discussion of several themes recurring throughout these case studies. Finally, Section 1.6 describes the lessons learned from the case studies. A more detailed technical introduction to the RAISE language and method is given in Chapter 2.

The success of the electronic governance (EGOV) benchmarking has been limited so far. Lacking a theory to integrate existing conceptualizations has made the acquisition and sharing of knowledge produced by different benchmarking exercises difficult. In order to address this problem, this paper: 1) explains the nature of the EGOV benchmarking activity though a well-established theoretical framework - Activity Theory, 2) applies the framework to carry out a mapping between a number of existing EGOV benchmarking conceptualizations, 3) develops an unified conceptualization based on these mappings and 4) validates the resulting model though a real-life national EGOV strategy development project. The use of the Activity Theory in the paper has enabled defining and relating initial dimensions of the EGOV benchmarking activity, and mapping the dimensions present in existing conceptualizations. This not only created a unifying theoretical basis for conceptualizing the EGOV benchmarking activity but allowed learning from and integrating existing conceptualizations. The work impacts on the EGOV benchmarking practice by enabling a logical design of the activity, and contextually correct understanding of existing EGOV benchmarking results with respect to their intended usage.

This document presents the mini-track on Development Methods for Electronic Government, organized for the third time under the Electronic Government Track at HICSS - Hawaii International Conference on System Sciences. The document introduces the rationale and the papers presented as part of the mini-track.

This volume contains the papers presented at the 1st International Conference on Theory and Practice of Electronic Governance (ICEGOV2007) which took place in Macao during 10-13 December 2007. ICEGOV2007 was co-organized by the Center for Electronic Governance at United Nations University - International Institute for Software Technology (UNU-IIST-EGOV), and the Center for Technology in Government, University of Albany, State University of New York, USA (CTG), and the United Nations Asian and Pacific Training Centre for Information and Communication Technology for Development (APCICT), Incheon, Republic of Korea.

This volume comprises the proceedings of the 2nd International Conference on Theory and Practice of Electronic Governance, ICEGOV2008, which took place in Cairo, Egypt during 1-4 December 2008. The conference was organized jointly by the Center for Electronic Governance at United Nations University - International Institute for Software Technology, and German University in Cairo.

The 3rd International Conference on Theory and Practice of Electronic Governance, ICEGOV2009, was organized in Bogota, Colombia during 10-13 November 2009. The conference took place under the patronage of the Ministry of Information and Communication Technology, Government of Colombia, and was co-organized by: (1) Electronic Governance Programme at United Nations University - International Institute for Software Technology, (2) Observatorio de Sociedad, Gobierno y Tecnologías de Información, Universidad Externado de Colombia, and (3) Programa Gobierno en Línea, Government of Colombia.

The ICEGOV conference series focuses on the use of technology to transform relationships between government and its customers – citizens, businesses, civil society and other arms of government (Electronic Governance), beyond the traditional focus on technology-enabled transformation within government (Electronic Government). After the first two editions – ICEGOV2007 in Macao and ICEGOV2008 in Cairo, ICEGOV2009 helped to further strengthen the features of the ICEGOV conference series as global, multi-stakeholder, networking, research and practice, capacity building, development and UN conferences. Notably, the conference enjoyed a strong representation from developing and transition countries, with contributions to research and practice of Electronic Governance, and offered a strong capacity- and network-building program with invited talks, invited sessions, tutorials, workshops, panel discussions, round-table discussions, papers sessions, and the demo and poster session. For the first time, the conference featured invited sessions to present experiences and lessons learnt in Electronic Governance development by various government organizations responsible for such development at the national or sub-national levels, as well as three round-table discussions aimed at consensus-building.

ICEGOV2009 benefited from invited talks by three distinguished experts and practitioners in the area: (1) Her Excellency Ms. María del Rosario Guerra, Minister of Information and Communication Technology, Government of Colombia - government perspective, (2) Prof. Matthias Finger, Ecole Polytechnique Fédérale de Lausanne, Switzerland - academic perspective, and (3) Dr. Saleem Zoughbi, Regional Advisor, Information and Communication Technology, United Nations Social and Economic Commission for Western Asia, Lebanon - international perspective. The talks took place on 11, 10 and 13 November 2009 respectively.

ICEGOV2009 also featured 12 invited sessions to present experiences and lessons learnt in Electronic Governance development at the national or sub-national levels: (1) Colombia - Programa Gobierno en Línea, Ministry of Information and Communication Technology; (2) Argentina - Officina Nacional de Tecnologias de la Informacion, Subsecretaria de Tecnologias de Gestion; (3) Dominican Republic - Centro de Estudios e Investigación de Gobierno Electrónico, Oficina Presidencial de Tecnologías de la Información y Comunicación; (4) Chile – Estrategia Digital; (5) Mexico - Secretaría de la Función Pública; (6) Korea - National Information Technology Industry Promotion Agency; (7) Rio Negre Province, Argentina – Ministerio de Hacienda, Obras y Servicios Publicos, Provincia de Rio Negro; (8) Costa Rica - Gobierno Digital; (9) China – National School of Administration; (10) Macao SAR – Government of Macao SAR, China; (11) Mongolia – ICT and Post Authority; and (12) Cameroon – National Agency for ICT; and three invited sessions on the topical areas by the international or multi-national organizations specializing in them: Technology Leadership by International Academy of CIO; Interoperability and Open Standards by Microsoft Corporation; and e-Governance and Development by United Nations Development Programme. The invited sessions took place on 11 November 2009 (countries and regions) and 12 November 2009 (topical areas).

ICEGOV2009 also featured a capacity building program comprising a series of six tutorials - three on domain-independent aspects of Electronic Governance and three on e-applications: (1) Technology by Jim Davies, University of Oxford, UK; (2) Transformation by Pallab Saha, National University of Singapore, Singapore; (3) Policy by Sharon S. Dawes and Theresa A. Pardo, Center for Technology in Government, University at Albany, State University of New York, USA; (4) e-Health by Jennifer Zelmer, International Health Terminology Standards Development Organisation, Denmark; (5) e-Economy by Wojciech Cellary, Poznan University of Economics, Poland; and (6) e-Leadership by Jean-Pierre Auffret, International Academy of CIO, USA and Elsa Estevez, United Nations University, Macao. The tutorials, held on 10 November 2009 provided the audience with the foundation and general understanding of the area.

The program also included three round-table discussions aimed at the national, regional and international consensus-building on specific topics of interest to the community, respectively: (1) How to Achieve High Take-up of Government Online organized by María Isabel Mejía Jaramillo, Programa Gobierno en Línea; (2) Towards Regional Dialogue to Promote Alliances co-organized by Florencia Ferrer, e-Stratégia Pública, Brazil and Miguel Porrua, Organization of American States, USA; and (3) Innovation Transfer Frameworks for Global Electronic Governance organized by Tomasz Janowski, United Nations University, Macao.

ICEGOV2009 received 102 submissions – papers, case studies, demos and posters from 39 countries and economies: Argentina, Azerbaijan, Bangladesh, Brazil, China, Colombia, Dominican Republic, Ethiopia, Finland, France, Germany, Ghana, Greece, India, Iran, Italy, Kenya, Korea, Macao SAR, Malaysia, Mongolia, Nepal, Netherlands, Nigeria, Pakistan, Palestine Territory, Peru, Portugal, Russia, Saudi Arabia, South Africa, Spain, Sri Lanka, Sweden, Switzerland, Tunisia, UK, Uruguay and USA. After a review process by the 57-member international Program Committee, the conference accepted 24 papers (8 pages), 29 case studies (6 pages), 6 demos (4 pages) and 17 posters (2 pages). Accepted demos and posters were presented as part of the demo and poster session on 10 November 2009, while accepted papers and case studies were presented as part of 12 regular paper sessions on 11 and 12 November 2009, and presented and discussed as part of 6 synchronized workshops and panel discussions on 13 November.

The current volume comprises all invited as well as submitted and accepted contributions to the ICEGOV2009 conference. The volume is organized into 21 sections: one for invited contributions, 6 for workshops, 12 for regular paper sessions, one for demos and one for posters. The 6 workshops cover the topics of: Architecture and Interoperability, Collaboration and Information Sharing, Knowledge Management, e-Policy, e-Participation and e-Taxation, while 12 regular paper sessions address the topics of: e-Diffusion, e-Democracy, Methodologies, Models and Frameworks, Implementation Planning, Implementation Strategies, Social Applications, Other Applications, Standards and Guidelines, Legal and Regulatory Issues, Infrastructure and Maturity Models. 

This volume contains the papers presented at the 4th International Conference on Distributed Computing and Internet Technology (ICDCIT2007) held during 17-20 December 2007 in Bangalore, India. The conference was organized by Kalinga Institute of Industrial Technology (KIIT), Bhubaneshwar, India, www.kiit.org, and co-organized by the Center for Electronic Governance at United Nations University International Institute for Software Technology (UNU-IIST-EGOV), Macao, www.egov.iist.unu.edu.

This book constitutes the proceedings of the 6th International Conference on Distributed Computing and Internet Technology, ICDCIT 2010, held in Bhubaneswar, India, in February 2010. The 26 papers presented consists of 12 long papers, 9 short papers and 5 extended abstracts. They were carefully reviewed and selected from 91 submissions. In addition the volume contains 4 invited talks. The topics covered are networking, grid computing and Web services, internet technology and distributed computing, software engineering of secured systems, and societal applications.

A major issue in organizations including public organizations is how to ensure that investments in Information Technology (IT) optimally deliver the expected value for stakeholders. Since most organizational transformation agenda in the government are articulated and implemented under the Public Administration Reform programs, and IT projects in government are increasingly associated with e-governance initiatives, the need to align reform and e-government programs arises. This paper shows how the Strategic Alignment Model (SAM) may be adapted for aligning public administration reform and e-government strategies. It shows how to partition strategies into domains equivalent to the four classical SAM domains and presents: (i) metrics for evaluating current level of alignment between the reform and e-government program, (ii) a process or sequence of steps to achieve desired alignments between the four domains, (iii) our experience in the application of the process in project involving the alignment of the e-government program and the reform roadmap of a city state in South-East Asia, and (iv) some features of the tool that has been developed to support the alignment process. Finally, the paper highlights our ongoing work in this area.

The goal of result-verification is to prove that one execution run of a program satisfies its specification. Compared with implementation-verification, result-verification has a larger scope for applications in practice, gives more opportunities for automation and, based on the execution record not the implementation, is particularly suitable for complex systems. This paper proposes a technical framework to apply this technique in practice. We show how to write formal result-based specifications, how to generate a verifier program to check a given specification and to carry out result -verification according to the generated program. The execution result is written as a text file, the verifier is written in AWK (special-purpose language for text processing) and verification is done automatically by the AWK interpreter, given the verifier and the execution result as inputs.