Publications

X2Rel is a new language to express binary relations between XML documents. A wide range of relations can be expressed: between different versions of the same document, between an instance and a schema document, between documents before and after a transformation, and others. The syntax of X2Rel is given in XML and its semantics is defined formally. The language relies on the well-established XML technologies of XML Schema and XSL Transformations. The paper presents the ongoing development of the language.

We study design support for building a virtual organisation, in particular the problem to organise production among the set of distributed cells to meet a given production goal. Each cell has a certain capacity to store, manufacture and deliver products, and it can interact with other cells by means of information and logistics networks. The goal specifies the type of the product and the volume required. We propose a solution to this problem in the form of a distributed coordination protocol. The protocol is based on an algorithm which given a goal and a cell attempts to generate a sequence of operations on the cell to implement this goal. Lacking the resources locally the algorithm generates some auxiliary goals which the protocol then communicates to other cells, involving generating (recursively) more processes and more goals etc. Although this leads generally towards the simpler goals, the protocol may sometimes fail to provide a match between the goals and cells, lacking the resources globally. We provide a formalisation of the problem, propose a solution, offer correctness arguments and discuss an email-based implementation.

 This document provides an abstract model for manufacturing industry, as it appears in the market context. We identify a number of `players' (consumers, suppliers, traders and producers) and formalize the ways they compete for the shared market. Initially abstract, the model becomes more concrete in a sequence of refinements (conceptual rather than formal) naturally evolving to address such aspects of an enterprise like marketing, finances, administration and production. The companion documents will consider these aspects in more detail. To formalize the game of supply and demand is a prerequisite, we believe, for modelling an enterprise that will provide the most effective answer to the demands of the business environment.

Consider a distributed real-time program which is executed on a system with a limited set of hardware resources. Assume the program is required to satisfy some timing constraints, despite the occurrence of anticipated hardware failures. For efficient use of resources, scheduling decisions must be taken at run-time, considering deadlines, the load and hardware failures. The paper demonstrates how to reason about such dynamically scheduled programs in the framework of a timed process algebra and modal logic. The algebra provides a uniform process encoding of programs, hardware and schedulers, with an operational semantics of a process depending on the assumptions about faults. The logic specifies the timing properties of a process and verifies them via this fault-affected semantics, establishing fault-tolerance. The approach lends itself to application of existing tools and results supporting reasoning in process algebras and modal logics.

A distributed real-time program is usually executed on a limited set of hardware resources and is required to satisfy timing constraints, despite anticipated hardware failures. Static analysis of the timing properties of such programs is often infeasible. This paper shows how to formally reason about these programs when scheduling decisions are made on-line and take into account deadlines, load and hardware failures. We use Timed CCS as a process language, define a language to describe anticipated faults and apply a version of a mu-calculus to specify and verify timing properties. This allows the property of schedulability to be the outcome of an equation-solving problem. And unlike conventional reasoning, the logic is fault-monotonic: if correctness is proved for a number of faults, correctness for any subset of these faults is guaranteed.

 A distributed real-time program is usually executed on a limited set of hardware resources and is required to satisfy timing constraints, despite anticipated hardware failures. Static analysis of the timing properties of such programs is often infeasible. This paper shows how to formally reason about these programs when scheduling decisions are made on-line and take into account deadlines, load and hardware failures. We use Timed CCS as a process language, define a language to describe anticipated faults and apply a version of a mu-calculus to specify and verify timing properties. This allows the property of schedulability to be the outcome of an equation-solving problem. And unlike conventional reasoning, the logic is fault-monotonic: if correctness is proved for a number of faults, correctness for any subset of these faults is guaranteed.

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.

We describe an approach to formally specify object-based software components, in order to be able to automatically check their behavior at run-time. The specification is a regular expression built from the propositions about the states (or pairs of states) of a component. Checking is done by a specification-generated wrapper, which produces a fail-stop component from a component which fails in an arbitrary way. The wrapper-generator is implemented for a subset of Java classes. We argue that specification-based error-detection is particularly suitable for the components of open, object-based distributed systems.

We provide three methods of verifying concurrent systems which are tolerant of faults in their operating environment - algebraic, logical and transformational. The first is an extension of the bisimulation equivalence, the second is rooted in the Hennessy-Milner logic, and the third involves transformations of CCS processes. Based on the common semantic model of labelled transition systems, which is also used to model faults, all three methods are proved equivalent for certain classes of faults.

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.

A distributed business process organizes activities by several enterprises to fulfill a given business goal. The purpose of this paper is to formalise what it means for such a process to be feasible (possible to carry out given the resources delegated for its execution) and for a feasible process to be correct (satisfying a given business goal), using customer-driven manufacturing as a particular, although broadly defined business area. Possible applications are: formal analysis of business processes, providing formal semantics to process modelling languages, and specification and rigorous development of business-support software.

We present an experiment in modelling and analysis of an application domain: competitive manufacturing. The result is a unique formal model which combines previously separate models for marketing (competition) and enterprises (coordination). In particular, we capture formally the marketing mix: product, price, place and promotion, and its effect on the sale of the enterprise. The model is built in stages: market without marketing, marketing without limits and marketing under limited resources. Analysis includes justifying abstraction, down to two enterprises competing for a single consumer.

We apply formal description techniques (FDT) to model, compose and give operational meaning to the class of reactive systems representing manufacturing enterprises. The enterprise pursues its activities by means of resources and processes that execute concurrently on the resources, subject to internal (resource) and external (market) constraints. Some modelling techniques are familiar for reactive systems, other are specific to this domain: modelling management decisions, product transfer during one-to-one (one supplier one consumer) synchronisation, marketing and many-to-one (many suppliers one consumer) synchronisation. The paper is a novel application of FDTs, also a contribution to the semantics of enterprise engineering.

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.

We study how composition of enterprise models can represent the behaviour of an extended/virtual enterprise. Each enterprise manufactures discrete-parts products and is modelled with three concepts: product-related resources, processes and business goals (customer and purchase orders). Composition makes possible two forms of interaction between enterprises: matching customer and purchase orders and sharing processes which cross organisational boundaries. Models and their composition are represented in a formal notation.

We show how to build and execute models of concurrent and distributed production systems using some of the Unix tools for text processing (Awk), process management (Bash) and information exchange (Mail). We use plain text files to represent the state of the production cell, implement production operations as text-transformations, compose such operations into one or several processes for their sequential or concurrent execution and allow remote processes (located in different cells) to communicate with each other by sending emails. The models are highly configurable, able to represent assembly lines, flexible manufacturing systems, even virtual organisations. But they are also concrete and implementation-dependent, therefore we also present their abstract formalisation in a specification language RSL.

We introduce a necessary test for the claims about provable fault-tolerance: having proved to tolerate several faults, we must tolerate (provably) any combination of them. One notable failure to pass this test is bisimulation. The paper presents a class of bisimulations which are fault-monotonic and within CCS support compositional design of component specifications by stepwise refinement, each step increasing or at least preserving the current level of fault-tolerance.

 We introduce a necessary test for the claims about provable fault-tolerance: having proved to tolerate several faults, we must tolerate (provably) any combination of them. One notable failure to pass this test is bisimulation. The paper presents a class of bisimulations which are fault-monotonic and within CCS support compositional design of component specifications by stepwise refinement, each step increasing or at least preserving the current level of fault-tolerance.

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.

 We show how to build and execute models of concurrent/distributed production cells using some of the Unix system tools, in particular for text processing (Awk), process management (Bash) and information exchange (Mail). We use text files to represent the state of a cell, implement production operations as text-transformations, compose such operations into one or several processes for their sequential/concurrent execution, and allow remote processes (located in different cells) to communicate with each other by emails. The models are higly configurable, able to represent assembly lines, flexible manufacturing systems, even virtual organizations. We also formalise them in a specification language, to achieve abstraction and implementation-independence. A simple case study illustrates the presentation.