Evaluating a Formal Specification Language

Formal knowledge modelling languages have a number of advantages over informal languages, such as their precise meaning and the possibility to derive properties through formal proofs. However, these formal languages also suffer from problems which limit their practical usefulness: they are often not expressive enough to deal with real world applications, formal models are complex and hard to read, and constructing a formal model is a difficult, error prone and expensive process. The goal of the study presented in this paper is to investigate the usability of one such formal KBS modelling language, called (ML)^2. In order to analyse the properties of (ML)^2 that influence its usability, we designed a set of evaluation criteria. We then applied (ML)^2 in two case-studies and scored the language on our evaluation criteria. A separate case-study was devoted to analysing the possibilities for reusing formal model fragment. (ML)^2 scored well on most of our criteria. This leads us to conjecture that the close correspondence between the informal KADS models and the formal (ML)^2 models avoids some of the problems that traditionally plague formal specification languages. The case-studies revealed problems with the reuse of formal model fragments. These problems were caused by the (inevitable) ambiguous interpretations of the informal model fragments. Finally, extensive software-support is required when constructing formal specifications. Our case-studies showed that the close correspondence between formal and informal models makes it possible to provide more support (and particularly: different kinds of support) than have traditionally been considered