TY - GEN
T1 - Evaluating a Formal Specification Language
AU - Ruiz, F.
AU - van Harmelen, F.A.H.
AU - Aben, M.
AU - van de Plassche, J.
N1 - F. Ruiz and Harmelen, F.A.H. van and M. Aben and J. van de Plassche. Evaluating a Formal Specification Language. In A Future for Knowledge Acquisition, Proc. 8th EKAW. Editors L. Steels and A.Th. Schreiber and W. Van de Velde. Series Lecture Notes in Artificial Intelligence. Pages 26--45. 1994. Springer-Verlag. Number 867.
PY - 1994
Y1 - 1994
N2 - 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.
AB - 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.
M3 - Conference contribution
SP - 26
EP - 45
BT - A Future for Knowledge Acquisition Proc. 8th EKAW
PB - Springer-Verlag
ER -