Technical Program for DCCA-7
The assignment to sessions and sessions to times is tentative.
Wednesday January 6, 1999
8:45am: Welcome etc.
9 am: Assessment of COTS Components
There is increasing pressure to use COTS (commercial off-the-shelf)
components in critical systems. How dependable are these components?
These two papers respectively examine design faults in a commercial
processor (Pentium II), and the reliability of a commercial
microkernel (Chorus ClassiX).
- The Taxonomy of Design Faults in COTS Microprocessors by
Algirdas Avizienis and Yutao He of UCLA, USA
- Assessment of COTS Microkernels by Fault Injection by
J.-C. Fabre, F. Salles, M. Rodriguez-Moreno, and J. Arlat of LAAS, France
10:30am Break
11am: Coping with COTS
These two papers respectively describe how to construct a reliable spacecraft
controller and fault-tolerant clocks from COTS components.
- Minimalist Recovery Techniques for Single Event Effects in
Spaceborne Microcontrollers by Douglas W. Caldwell and David
A. Rennels of UCLA, USA
- Building Fault-Tolerant Hardware Clocks from COTS Components
by Christof Fetzer and Flaviu Cristian of UCSD, USA
12:30pm Lunch
2pm: Formal Methods
Formal methods can help develop verified systems, and can also be used
to examine requirements and designs for bugs. The first of these papers
uses theorem proving to develop verified controllers, while the other
two use model checking in the validation of complex requirements.
- A Methodology for Proving Control Systems with Lustre and PVS
by S. Bensalem, P. Caspi, C. Parent-Vigouroux, C. Dumas, and
D. Pilaud, VERIMAG, France
- Prototyping and Formal Requirement Validation of GPRS: A Mobile
Data Packet Radio Service for GSM by Luigi Logrippo, Laurent
Andriantsiferana, and Brahim Ghribi of University of Ottawa, Canada
- Formal Description and Validation for an Integrity Policy
Supporting Multiple Levels of Criticality by A. Fantechi,
S. Gnesi, and L. Semini of Universitŕ di Firenze, Italy
4pm Break
4:30pm: Distributed Systems
The first of these papers develops an infrastructure for
fault-tolerance on top of CORBA; the second considers how to improve
performance of one of the protocols used in such infrastructures.
- Proteus: A Flexible Infrastructure to Implement Adaptive Fault
Tolerance in AQuA by Chetan Sabnis, Michel Cukier, Jennifer Ren,
William H. Sanders, David E. Bakken, and David Karr of University of
Illinois and BBN, USA
- Improving Performance of Atomic Broadcast Protocols Using the
Newsmonger Technique by Shivakant Mishra and Sudha M. Kuntur of
University of Wyoming, USA
Thursday January 7, 1999
9am: Time-Triggered Architecture
The time-triggered architecture (TTA) provides a robust foundation for
critical control applications such as drive-by-wire. The first paper
describes how fault-tolerant applications can be supported in this
architecture, while the second describes formal verification of the
clock-synchronization protocol used in TTA.
- The Transparent Implementation of Fault Tolerance in
the Time-Triggered Architecture by Hermann Kopetz and Dietmar
Millinger of TU Vienna, Austria
- Formal Verification for Time-Triggered Clock Synchronization
by Holger Pfeifer, Detlef Schwier, and Friedrich W. von Henke of
University of Ulm, Germany
10:30am Break
11am: Fault Tolerance and Safety
The redundancy added to provide fault tolerance can introduce new
failure modes that may compromise safety. The first paper describes
such a situation and presents a protocol that overcomes it. The
second paper describes validation of fault tolerant systems by fault
injection.
- PADRE: A Protocol For Asymmetric Duplex Redundancy by Didier
Essame, Jean Arlat, and David Powell of LAAS, France
- Experimental Validation of High-Speed Fault-Tolerant Systems Using
Physical Fault Injection by R. J. Martínez, P. J. Gil,
G. Martín, C. Pérez, and J.J. Serrano of the University and
Politecnica of Valencia, Spain
12:30pm Lunch
2pm: Models of Partitioning for Integrated Modular Avionics
Integrated Modular Avionics (IMA) bring together several airplane
control functions that were previously performed by separate computer
systems. This creates new opportunities for fault propagation that
must be eliminated by partitioning. But what exactly are the
requirements for safe partitioning? These three papers attempt to
answer this question using models that have their roots in computer
security.
- A Model of Cooperative Noninterference for Integrated Modular
Avionics by Ben L. Di Vito of ViGYAN/NASA Langley, USA
- Invariant Performance: A Statement of Task Isolation Useful for
Embedded Application Integration by Matthew M. Wilding, David
S. Hardin, and David A. Greve of Collins Commercial Avionics, USA
- A Model of Non-Interference for Integrating Mixed-Criticality
Software Components by Bruno Dutertre and Victoria Stavridou of
SRI International, USA
4 pm Break
4:30pm: Dependability Evaluation
For some, dependability is closely related to reliability; for others,
it is a more complex mix of properties. The first paper applies
classical reliability modeling to phased missions, while the second
proposes a method for evaluating a system against multiple criteria.
- Dependability Modeling and Evaluation of Phased Mission Systems: a
DSPN Approach by Ivan Mura, Andrea Bondavalli, Xinyu Zang, and
Kishor Trivedi of University of Pisa and CNUCE/CNR, Italy, and Duke
University, USA
- Dependability Evaluation using a Multi-Criteria Decision Analysis
Procedure by Divya Prasad and John McDermid of the University of
York, UK
Later: Banquet
Friday January 8, 1999
9am: Panel: Certification and Assessment of Critical Systems
It is difficult or impossible to measure some important attributes of
critical systems (e.g., experimental quantification of failure rates
in the 10-9 range is infeasible). Therefore, many of the standards
for critical software development (e.g., DO-178B, IEC1508, the Common
Security Criteria) focus on the development process: "we cannot
measure how well you did, so we measure how hard you tried." Some
criticise these standards for having requirements whose compliance
cannot be objectively determined, or for requiring use of techniques
whose efficacy has not been established. Others note that multiple
sources of evidence are required in assessing a critical systems, and
ask how best to combine these different sources.
This panel will comprise experts representing a range of opinion
who will examine the topic of certification and assessment of critical
systems from several perspectives.
11am Break
11:30am: Probabilistic Guarantees
The first paper considers scheduling in the presence of faults, while
the second considers detection of faulty components. Both papers
employ statistical methods.
- Probabilistic Scheduling Guarantees for Fault-Tolerant
Real-Time Systems by A. Burns, S. Punnekkat, L. Strigini and
D. R. Wright of the University of York and City University, UK
- Fault Detection for Byzantine Quorum Systems by Evelyn
Pierce, Lorenzo Alvisi, Dahlia Malkhi, and Michael Reiter of
University of Texas at Austin, and Bell Laboratories, USA
1 pm Adjourn
Last changed 12 October 1998 by John Rushby: Rushby@csl.sri.com