Semi-Automated Component-Based Development of Formally Verified Software

A number of formal approaches to component-based software development have been proposed, based on the idea of using formal specifications as a basis for retrieval. These approaches provide good recall and precision when searching for components. More recently, the problem of component adaptation has begun to be addressed, in recognition of the fact that a library component will rarely meet the needs of the user exactly. However the main weakness of the current approaches is they only cater for a single adaptation step.In reality, we typically need to apply some combination of adaptation steps. In this paper we present a collection of search tactics, which allow us to combine a sequence of matching and adaptation commands into a single step. The tactics are presented in a general manner, with the intention that they could be applied to a variety of different formal-based approaches to CBSD. We illustrate the use of the search tactics using a simple example.