Semantic Issues for Component Technologies
Final rept. 15 Mar 1998-1 Jun 2001
FLORIDA UNIV GAINESVILLE COMPUTER INFORMATION SCIENCE AND ENGINEERING
Pagination or Media Count:
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.
- Computer Programming and Software