Peer-Reviewed Journal Details
Mandatory Fields
Sharon Flynn and Dick Hamlet
Theoretical Computer Science
On Formal Specification of Software Components and Systems
Optional Fields
Formal Specification
Abstract Reasoning about software systems developed using components begins with component-level specifications, from which system-level specifications are derived. While sound compositional reasoning is a strength of formal specification methods, practical experience with systems construction leads us to expect surprises when two components that were never intended to be combined are composed. Component specifications, like any other human artifact, are likely to be in error. Composition throws the mistakes in one component against those in another, leading to unexpected and often bizarre behavior. We review the theory of formal software specification and apply it to the combination of component specifica- tions into system-level properties, where deficiencies in component specifications can be strangely reflected. We conclude that desirable properties of system specifications do not always arise from those same properties at the component level. Keywords: Formal specification, software component, composition 1Introduction Although elementary formal descriptions of program semantics, specifications, and the correctness relationship between them have long been used, applying these de- scriptions to software components and their combination into systems has been little explored. Furthermore, the role played by persistent state in software has not been singled out for formal analysis. State plays a central role in component-based system development (CBSD), so CBSD is a good setting for a theoretical treatment.
Grant Details
Publication Themes