This thesis presents an approach to reusing components which alleviates some of the main problems encountered in component-based reuse; in particular modifying components to suit user's specific needs, and locating suitable components within a library. The focus of the thesis is on components described using a formal language (in other words components with a formal interface specification). The main reason for this is the concise and precise nature of formal languages, which can be exploited in developing more sophisticated methods and tools which take advantage of the semantics of the component. The solution is presented in two main stages: firstly a framework for adapting components is defined; secondly a framework for retrieving components based on matching component interfaces is defined. Both of these frameworks take advantage of the formal nature of the component interfaces, as a result more sophisticated tools can be developed. For generality it is proposed that formal languages used to represent interfaces are partitioned into three separate levels of granularity - expressions, units and modules - and solutions to adaptation and retrieval are developed separately at each level. An important consideration in developing these frameworks is to ensure that certain component properties are preserved when adapting and retrieving components. Having proposed these general frameworks, algorithms for adapting and retrieving components are defined in a more concrete and detailed sense within the CARE system. CARE was chosen because the language is relatively simple and compact, yet contains many of the features found in other formal languages, including: variables; functions; predicates; binders; application; typing; parameters; inputs and outputs (and their types); preconditions and postconditions; textual and formal parameters; separation of specification and implementation; case statements; modules; applicability conditions; encapsulation; and information hiding. These techniques for adapting and retrieving components have been prototyped as extensions to existing CARE tools. As a means of illustrating the value that these extensions have added to the overall CARE system, several example developments using the extended tools are presented at the end of the thesis. The approach to component reuse presented in this thesis represents a significant advance on other similar approaches. The approach given here is far more general than other approaches, particularly with respect to the scope of components and their interfaces that are considered. Also the adaptation framework goes beyond other approaches which have typically been restricted to parameter instantiation.

The use of predicate transformers to model the action of sequential programs has allowed the construction of a refinement calculus for expressing the formal verification of the top-down development of sequential programs. It is shown that predicate transformers may also be used to model real-time processes. The notions of precondition and postcondition in the sequential refinement calculus are replaced by the notions of assumption and effect. In this way the formal development of real-time processes may also be expressed within the refinement calculus. Notations are developed for the specification and implementation of real-time processes within the framework of the refinement calculus. Several case-studies are presented to demonstrate the utility of this approach.

This thesis investigates the process of designing software from formal specifications, in particular, specifications expressed in the Z notation. The initial phases of software design have significant impact on software quality and the transition from formal specification to design is not clearly understood. There is often no visible or obvious connection between the specification and the finished design. It is possible to add traceability with either verification or refinement, but I wish to understand and guide the design process. Investigating the design of software from formal specifications highlighted possible relationships between parts of the specification and parts of the design. A design strategy is introduced, that combines software architectural styles and formal specifications to influence the generated design. The design process is architecturally-specific, but a template for instantiating the design process to a chosen architectural style is presented. Specializations of the template are presented for the ADT-based architectural style and the event-based architectural style. These specializations of the template produce an architecturally-constrained, specification-influenced design process. Providing an architecturally-constrained, specification-influenced design process enables the software designer to produce better quality software. The constrained design process allows the designer to focus on the difficult aspects of design: understanding the problem, choosing the best abstractions, and finding a suitable solution.

Diss. Linköping : Univ., 2002.

Diss. Uppsala : Univ., 2005.

Diss. Uppsala : Uppsala universitet, 2005.

Thesis (D. Min.)--Trinity Evangelical Divinity School, 2006. / Abstract. Includes bibliographical references (leaves 202-211).

Thesis (Ph. D.)--State University of New York at Binghamton, Mathematical Sciences Department, 2007. / Includes bibliographical references.

Thesis (D. Min.)--Trinity Evangelical Divinity School, 2006. / Abstract. Includes bibliographical references (leaves 202-211).

Thesis (Ed. D.)--Teachers College, Columbia University, 1994. / Includes tables. Typescript; issued also on microfilm. Sponsor: William T. Vericker. Dissertation Committee: Professor Matthias Finger. Includes bibliographical references (leaves 191-202, 314-320) and index.