Dynamics of gene expression in an artificial genome

Complex systems techniques provide a powerful tool to study the emergent properties of networks of interacting genes. In this study we extract models of genetic regulatory networks from an artificial genome, represented by a sequence of nucleotides, and analyse how variations in the connectivity and degree of inhibition of the extracted networks affects the resulting classes of behaviours. For low connectivity systems were found to be very stable. Only with higher connectivity was a significant occurrence of chaos found. Most interestingly, the peak in occurrence of chaos occurs perched on the edge of a phase transition in the occurrence of attractors.

Superstring: A scalable service discovery protocol for the wide-area pervasive environment

Arguably, the world has become one large pervasive computing environment. Our planet is growing a digital skin of a wide array of sensors, hand-held computers, mobile phones, laptops, web services and publicly accessible web-cams. Often, these devices and services are deployed in groups, forming small communities of interacting devices. Service discovery protocols allow processes executing on each device to discover services offered by other devices within the community. These communities can be linked together to form a wide-area pervasive environment, allowing processes in one p u p tu interact with services in another. However, the costs of communication and the protocols by which this communication is mediated in the wide-area differ from those of intra-group, or local-area, communication. Communication is an expensive operation for small, battery powered devices, but it is less expensive for servem and workstations, which have a constant power supply and 81'e connected to high bandwidth networks. This paper introduces Superstring, a peer to-peer service discovery protocol optimised fur use in the wide-area. Its goals are to minimise computation and memory overhead in the face of large numbers of resources. It achieves this memory and computation scalability by distributing the storage cost of service descriptions and the computation cost of queries over multiple resolvers.

A classification of concurrency failures in java components

The Java programming language supports concurrency. Concurrent programs are hard to test due to their inherent non-determinism. This paper presents a classification of concurrency failures that is based on a model of Java concurrency. The model and failure classification is used to justify coverage of synchronization primitives of concurrent components. This is achieved by constructing concurrency flow graphs for each method call. A producer-consumer monitor is used to demonstrate how the approach can be used to measure coverage of concurrency primitives and thereby assist in determining test sequences for deterministic execution.

Tool support for generating passive C++ test oracles from object-z specifications

A test oracle provides a means for determining whether an implementation behaves according to its specification. A passive test oracle checks that the correct behaviour has been implemented, but does not implement the behaviour itself. In previous work, we have presented a method that allows us to derive passive C++ test oracles from formal specifications written in Object-Z. We describe the "Warlock" prototype tool that supports the method. Warlock is built on top of an existing Object-Z type checker and generates oracle code for a substantial subset of the Object-Z language. We describe the architecture of Warlock and its application to a number of Object-Z specifications. We also discuss its current limitations.

Refinement of higher-order logic programs

A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we extend the refinement calculus for logic programs to include higher-order programming capabilities in specifications and programs, such as procedures as terms and lambda abstraction. We use a higher-order type and term system to describe programs, and provide a semantics for the higher-order language and refinement. The calculus is illustrated by refinement examples.

Mutation analysis to verify feature matrices for isolating errors in simulation models

Software simulation models are computer programs that need to be verified and debugged like any other software. In previous work, a method for error isolation in simulation models has been proposed. The method relies on a set of feature matrices that can be used to determine which part of the model implementation is responsible for deviations in the output of the model. Currrently these feature matrices have to be generated by hand from the model implementation, which is a tedious and error-prone task. In this paper, a method based on mutation analysis, as well as prototype tool support for the verification of the manually generated feature matrices is presented. The application of the method and tool to a model for wastewater treatment shows that the feature matrices can be verified effectively using a minimal number of mutants.

Animation of object-z specifications using a Z animator

We discuss a methodology for animating the Object-Z specification language using a Z animation environment. Central to the process is the introduction of a framework to handle dynamic instantiation of objects and management of object references. Particular focus is placed upon building the animation environment through pre-existing tools, and a case study is presented that implements the proposed framework using a shallow encoding in the Possum Z animator. The animation of Object-Z using Z is both automated and made transparent to the user through the use of a software tool named O-zone.