Evaluating a formal KBS specification language

In recent years, the knowledge engineering community has begun to explore formal specification languages as a tool in the development of knowledge-based systems. These 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. (ML)^2 is strongly based on the structure of the knowledge-models used in the KADS KBS development method. We first designed a set of evaluation criteria. We then applied (ML)^2 in two case-studies and scored the language on our evaluation criteria. (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