Registration is open. Early registration deadline July 26, 2009

Abstracts:

Shinichi Kikuchi

"Robustness and differentiation of signal transduction networks"

To understand emerging properties of complex signaling networks in cellular events, we investigate a phase-specific network model that corresponds to gene expressions which differentiate a myriad of biological functions. We showed no significant differences between fetal- and adult-phase networks for conventional statistical tests on network features, such as degree distribution and clustering coefficients, however, k-shortest paths revealed the difference on typical phase-specific pathways. These k-shortest paths were found highly optimized, which indicates evolutional network optimization might occur to acquire such phase-dependent responses.

Carolyn Talcott

"Fault Tolerance From a Cellular Biology Perspective"

We will survey a wide range of phenomena and mechanisms at the cellular level of biological systems include microbial organisms, immune systems, metabolic and signaling network. We will consider questions such as what are the perceived `goals' of a system, what does fault tolerance mean in this setting, and how we might abstract the `strategies' used in the biological systems as design principals for achieving the desired behavior in the presence of `faults'.

Joe Fitzsimons

"Quantum Fault Tolerance in Systems with Restricted Control"

In many proposed architectures for quantum computing the physics of the system prevent qubits from being individually controlled. In this talk I will introduce some of the main hurdles facing implementation of fault-tolerant quantum computation in systems with limited control. In particular I will focus on local models, in which qubits interact only with neighbours on a low dimensional lattice and which must be addressed globally. While recent results have shown that fault-tolerance thresholds do exist for such systems, current thresholds are extremely low. I shall discuss how fault-tolerance can be achieved in such systems and attempt to identify the main hurdles to higher thresholds and how they might be overcome.

Anish Arora

"Gray-Box Component-Based Fault-Tolerance"

This talk describes early work on using detector and corrector components as a necessary and sufficient basis for designing fault-tolerance, and more recent work in the use of these components in the context of specification based design. We will use a sensor network protocol as a example to illustrate the ideas.

Fuad Abujarad and Sandeep S. Kulkarni

"Weakest Invariant Generation for Automated Addition of Fault-Tolerance"

One of the important tasks in evolving a fault-intolerant program into a fault-tolerant one is to identify the legitimate states (its invariant) from where the original program satisfies its specification. This allows us to ensure that the fault-tolerant program recovers to these legitimate states from where it satisfies its specification. It is desired that the invariant be the weakest possible so as to provide maximal options to the algorithm for adding fault-tolerance. Requiring the designer to specify such weak invariant increases the burden on the designer. In this paper, we present a novel approach for automating the generation of the weakest invariant from the program actions and specifications. Our algorithm is efficient and manages the state explosion problem with the use of BDDs. We demonstrate our approach through three case studies and we show that generating such invariants is extremely fast. For example, for a mutual exclusion program with a state space of size 1084 states, it took 0.9 of a second.

Sandeep Kulkarni

"Automated Model Revision"

We focus on the problem of automated model revision where an existing model/program is to be modified to meet a new property (e.g., fault-tolerance property, timing constraints, safety property) to an existing program. This problem occurs during model evolution when equirements change or when the existing model is found to be noncompliant with an existing requirement. One of the requirements for such revision is that the existing properties continue to be preserved. In this talk, I will present complexity issues with such model revision as well as introduce the tool SYCRAFT. SYCRAFT is a BDD-based tool for automated addition of fault-tolerance to distributed programs and has been successfully used for synthesizing programs with state space of 10^100.

Tom Maibaum and Pablo Castro

"Deontic Logic, Contrary to Duty Reasoning and Fault Tolerance"

Deontic Logic was introduced in the first half of the last century to formalise aspects of legal reasoning. Since then a lot of effort has gone into improving the formalism(s) and widening their applicability, including in Computer Science and Software Engineering. One strand of work has focused on the use of an action based approach to deontic operators, rather than the traditional property focused operations. We propose a new version of this kind of deontic logic that has very nice metalogical properties, avoids many of the traditional problems of deontic logics and has a nice treatment of contrary to duty reasoning. This kind of reasoning provides a kind of conditional reasoning about having violated deontic constraints and describing the resulting consequences. We show how to apply this formalism to characterise fault tolerance mechanisms and to then reason about the properties of the mechanisms.