Edge-coloured cube decompositions

An edge-colored graph is a graph H together with a function f:E(H) → C where C is a set of colors. Given an edge-colored graph H, the graph induced by the edges of color c C is denoted by H(c). Let G, H, and J be graphs and let μ be a positive integer. A (J, H, G, μ) edge-colored graph decomposition is a set S = {H 1,H 2,...,H t} of edge-colored graphs with color set C = {c 1, c 2,..., c k} such that Hi ≅ H for 1 ≤ i ≤ t; Hi (cj) ≅ G for 1 ≤ i ≤ t and ≤ j ≤ k; and for j = 1, 2,..., k, each edge of J occurs in exactly μ of the graphs H 1(c j ), H 2(c j ),..., H t (c j ). Let Q 3 denote the 3-dimensional cube. In this paper, we find necessary and sufficient conditions on n, μ and G for the existence of a (K n ,Q 3,G, μ) edge-colored graph decomposition. © Birkhäuser Verlag, Basel 2007.

Architectural design in object-z

We present a process for introducing an object-oriented architecture into an abstract functional specification written in Object-Z. Since the design is derived from the specification, correctness concerns are addressed as pan of the design process. We base our approach on refactoring rules that apply to class structure, and use the rules to implement design patterns. As a motivating example, we introduce a user-interface design that follows the model-view-controller paradigm into an existing specification.

Refactoring object-z specifications

Object-Z offers an object-oriented means for structuring formal specifications. We investigate the application of refactoring rules to add and remove structure from such specifications to forge object-oriented designs. This allows us to tractably move from an abstract functional description of a system toward a lower-level design suitable for implementation on an object-oriented platform.

Formal analysis of human-computer interaction using model checking

Experiments with simulators allow psychologists to better understand the causes of human errors and build models of cognitive processes to be used in human reliability assessment (HRA). This paper investigates an approach to task failure analysis based on patterns of behaviour, by contrast to more traditional event-based approaches. It considers, as a case study, a formal model of an air traffic control (ATC) system which incorporates controller behaviour. The cognitive model is formalised in the CSP process algebra. Patterns of behaviour are expressed as temporal logic properties. Then a model-checking technique is used to verify whether the decomposition of the operator's behaviour into patterns is sound and complete with respect to the cognitive model. The decomposition is shown to be incomplete and a new behavioural pattern is identified, which appears to have been overlooked in the analysis of the data provided by the experiments with the simulator. This illustrates how formal analysis of operator models can yield fresh insights into how failures may arise in interactive systems.