Software engineering implications for formal refinement

Abstract

Formal methods are widely proposed as an important part of the software design process, but the design of large systems imposes software engineering constraints on the refinement of these specifications into coded modules. The need to separate the role of system building from the refinement of particular components means that relationships between specification units during the refinement process must be reified (that is made into objects) in the software development data-base. The traditional quasi-independent development of system modules can be applied more strongly in the presence of formal specifications, but care must be taken in order to retain the goal of proportionate effort between requirements changes and redevelopment cost. Two ways of addressing these requirements are proposed, the presence of semantic interfaces between specification components as database objects and the use of shared parameters to generic specifications to represent shared sub-specification. In both these cases the interface specification forms the focus of negotiation for shared design decisions. In addition a higher level structuring concept is introduced, the collection which describes the requirements for a set of modules and their inter-relationship.