Dependability Reading Group:E's Job Talk
From Dependability
| Overview | | Schedule | | Syllabus | | Editing Guidelines |
Elisabeth will present her job talk for us, as a practice before she heads up to GMU. Please come prepared to give her feedback.
Dependability in Embedded System Software Through Assured Reconfiguration
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.