Dependability in Embedded System Software Through Assured Reconfiguration

Elisabeth Strunk, University of Virginia

Friday, March 16
10:15am - SENSQ 5317
Students meet the speaker at 11:30 a.m.

Refreshments at 10:00am

Hosted by Bruce Childers

Abstract

As software systems continually become larger and more complex, assurance of their critical properties becomes correspondingly more difficult. Problems of verification, validation, and reliability all multiply with complexity. In many software systems, however, critical properties are only a small subset of all desirable system properties. In these systems, assurance of dependability can be reduced to a guarantee that either the system will function correctly, or the non-critical function will do nothing to interfere with critical system properties.

This work provides a method for constructing systems to be dependably reconfigurable. A system with reconfiguration at the center of its assurance argument can allow its primary function to fail and then reconfigure to some simpler function, mitigating any unacceptable failure consequences. Reconfiguration thus controls the effective complexity of the system without forcing that system to sacrifice desired, but unassurable, capabilities.

Focusing a system's dependability argument on reconfiguration means that reconfiguration must proceed correctly with very high assurance. In this work, we: (1) introduce a formal definition of reconfiguration and an associated set of high-level, general properties; (2) construct an architecture to support the high-level reconfiguration properties; and (3) formally prove that the architecture has the high-level properties using the PVS theorem-proving system. To illustrate the ideas in this work, we have specified part of a hypothetical avionics system that is typical of what might be found on a modern general-aviation aircraft or an unmanned aerial vehicle, and we have formally proven that it satisfies the architecture's requirements.

Biography of Speaker

Elisabeth Strunk received her Ph.D. from the University of Virginia in 2005 and is currently a research scientist there. She works in the Dependability Research Group, studying the use of formal methods in the construction of safety-critical software systems. Her major projects are architecting embedded software systems to be survivable, verifying that an implementation has properties set out in a system's formal specification, clarifying the role of natural language in software development, and exploring new technologies for accident investigation and analysis.