Integrating formal methods with domain analysis

The use of formal methods should help to achieve a high degree of confidence that a system will conform to its specification, enhancing in consequence software quality and reliability. However, a general acceptance of formal methods among software engineers is still some way off because formal methods are usually only accessible to specialists and they do not have developed in depth strategies for the first stages of development. This is also valid to Domain Analysis, because its first stage is to capture the knowledge of a particular domain, making necessary to have a model comprehensible by software engineers and domain experts. In order to address this problem and take advantage of formal methods, we suggest integrating the phase reusable Domain Analysis into the RAISE Method, combining Domain Analysis notions with a formal language in the early steps of software development process. In this paper, we present a set of heuristics to fruitfully use knowledge represented in a Domain Analysis model to derive a formal specification in the RAISE Specification Language.