TitleFormalizing lightweight verification of software component composition
Publication TypeConference Paper
Year of Publication2004
AuthorsMcCamant S, Ernst MD
Conference NameSAVCBS 2004: Specification and Verification of Component-Based Systems
Pagination47–54
Date or Month PublishedOctober
Conference LocationNewport Beach, CA, USA
AbstractSoftware errors often occur at the interfaces between separately developed components. Incompatibilities are an especially acute problem when upgrading software components, as new versions may be accidentally incompatible with old ones. As an inexpensive mechanism to detect many such problems, previous work proposed a technique that adapts methods from formal verification to use component abstractions that can be automatically generated from implementations. The technique reports, before performing the replacement or integrating the new component into a system, whether the upgrade might be problematic for that particular system. The technique is based on a rich model of components that support internal state, callbacks, and simultaneous upgrades of multiple components, and component abstractions may contain arbitrary logical properties including unbounded-state ones. \par This paper motivates this (somewhat non-standard) approach to component verification. The paper also refines the formal model of components, provides a formal model of software system safety, gives an algorithm for constructing a consistency condition, proves that the algorithm's result guarantees system safety in the case of a single-component upgrade, and gives a proof outline of the algorithm's correctness in the case of an arbitrary upgrade.
Downloadshttps://homes.cs.washington.edu/~mernst/pubs/upgrades-savcbs2004.pdf PDF
Citation KeyMcCamantE2004:formalizing-upgrades