Semantic Issues for Component Technologies
Abstract
The availability of components that can be assembled together to build customized system promises to decrease software development costs and, one hopes, also increase the reliability of the resulting system. Clearly, this promise can only be realized when a system designer has adequate information about the components that will be used to predict how systems containing them will behave. This project explored approaches to specifying components using formal techniques that allow a component developer to verify that the component itself satisfies its specification, and also allow the system builder who uses the component to reason about the behavior of systems containing that component. A general theory guarantees properties for components was developed. A guarantees property of a component describes the behavior of systems containing that component. In order to use the general theory, it must be instantiated as and extension of a more complete programming logic. Case studies were performed with two programming logics: UNITY, and CTL. In the latter case, model checking tools for mechanized reasoning about closed systems specified in CTL were used along with assertional techniques to reason about composite systems.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 2001
- Accession Number
- ADA399737
Entities
People
- Beverly A. Sanders
Organizations
- University of Florida