Hostname: page-component-586b7cd67f-2plfb Total loading time: 0 Render date: 2024-11-21T23:01:25.998Z Has data issue: false hasContentIssue false
  • English
  • Français

Formal methods in knowledge engineering

Published online by Cambridge University Press:  07 July 2009

Frank van Harmelen  and
Dieter Fensel
Frank van Harmelen
Affiliation:
Vrije Universiteit Amsterdam, Department of Mathematics and Computer Science, AI Group, De Boelelaan 1080a, 1081 HV Amsterdam, The Netherlands (email: [email protected])
Dieter Fensel
Affiliation:
SWI, University of Amsterdam, Roetersstraat 15, 1018MT Amsterdam, The Netherlands
Get access Rights & Permissions [Opens in a new window]

Abstract

This paper presents a general discussion of the role of formal methods in knowledge engineering. We give an historical account of the development of the field of knowledge engineering towards the use of formal methods. Subsequently, we discuss the pros and cons of formal methods. We do this by summarising the proclaimed advantages, and by arguing against some of the commonly heard objections against formal methods. We briefly summarise the current state of the art and discuss the most important directions that future research in this field should take. This paper presents a general setting for the other contributions in this issue of the journal, which each deal with a specific issue in more detail.

Type
Research Article
Information
The Knowledge Engineering Review , Volume 10 , Issue 4 , December 1995 , pp. 345 - 360
Copyright
Copyright © Cambridge University Press 1995

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Aben, M. 1995, Formal methods in Knowledge Engineering PhD thesis, University of Amsterdam, Faculty of Psychology, 02.Google Scholar
Anderson, S. and Bruns, G., 1995, “The formalization and analysis communication protocol” In: Hinchey, M. and Bowen, J. (eds.), Application of Formal Methods, Prentice Hall.Google Scholar
Angele, J., Fensel, D., Landes, D., Neubert, S. and Studer, R., 1993, “Model-based and incermental knowledge of engineering: The MIKE approach” In: Cuena, J. (ed.), Knowledge oriented software Design, Number A-27, IFIP Transactions, North Holland.Google Scholar
Anegle, J., Fensel, D., Landes, D. and Studer, R., 1995, “The knowledge-based acquisition and representation language KARL” (submitted for publication).CrossRefGoogle Scholar
Aronsson, M, Eriksson, M and Kreuger, P, 1994, “GCLA and a sketch of its use for representing KADS models” In: Proceedings of the ECAI'94 Workshop on Formal Specification Methods for Knowledge-Based Systems Amsterdam, 08.Google Scholar
Ayel, M and Laurent, J-P, editors, 1991, Validation, Verification and Test of Knowledge-Based System Wiley.Google Scholar
Barbuceanu, M, 1993, “Towards integrated knowledge modeling environments” Knowledge Acquisition 5(3).CrossRefGoogle Scholar
Bauer, C and Karbach, W, editors, 1992, Proceedings Second KADS User Meeting ZFE BT SE 21, Otto-Hahn Ring 6, D-8000 Munich83, 17–18 02. Siemens AG.Google Scholar
Bicarregui, J, Fitzgerald, J, Lindsay, P, Moore, R and Ritchie, B, 1994, Proof in VDM: A Practioner's Guide Springer-Verlag.CrossRefGoogle Scholar
Bowen, J and Hinchey, M, 1994, “Seven more myths of formal methods” In: Naftalin, M, Denvir, T and Bertran, M (eds.), Proceedings of the 2nd International Symposium of Formal Methods Europe (FME'94) volume 873 of Lecture Notes in Computer Science pp 105–115, Barcelona, 10.Google Scholar
Breuker, JA and de Greef, P, 1993, “Modelling system-user cooperation in KADS In: ATh, Schreiber, Wielinga, BJ and Breuker, JA (eds.), KADS: A Principled Approach to Knowledge-Based System Development pp 47–70, Academic Press.Google Scholar
Breuker, JA and Van de Velde, W, editors, 1994, The Common KADS Library for Expertise Modelling IOS Press.Google Scholar
Breuker, JA, Wielinga, BJ, van Someren, M, de Hoog, R, Schreiber, ATh, de Greef, P, Bredeweg, B, Wielemaker, J, Billault, JP, Davoodi, M and Hayward, SA, 1987, “Model Driven Knowledge Acquisition: Interpretation Models” ESPRIT Project P1098 Deliverable Dl (task Al), University of Amsterdam and STL Ltd.Google Scholar
Buchanan, BG and Shortliffe, EH, 1984, Rulebased Expert Systems: The Mycin Experiments of the Stanford Heuristic Programming Project Addison-Wesley.Google Scholar
Chandrasekaran, B, 1986, “Generic tasks in knowledge based reasoning: High level building blocks for expert system design” IEEE Expert 1 (3) 23–30.CrossRefGoogle Scholar
Clancey, WJ, 1993, “Heuristic classification” Artificial Intelligence 27 289–350.CrossRefGoogle Scholar
Colburn, TR, Fetzer, JH and Rankin, TL, editors, 1993, Program Verification Kluwer Academic.CrossRefGoogle Scholar
Craig, I, 1991a, The Formal Specification of Advanced AI Architecture: Lecture Notes in Mathematics Ellis Horwood.Google Scholar
Craig, I, 1991b, “The formal specification of ELEKTRA” Technical report, Department of CS, University of Warwick.Google Scholar
Craigen, C, 1995, “Applications of formal methods: Observations and trends” In: Hinchey, M and Bowen, J (eds.), Applications of Formal Methods Prentice Hall.Google Scholar
Craigen, D, Gerhart, S and Ralston, T, 1993, “An international survey of industrial applications of formal methods” Technical report, U.S. Department of Commerce, Technology administration, National Institute of Standards and Technology, Computer Systems Laboratory, Gaithersburg, MD 20899, USA, 03.Google Scholar
Fensel, D, 1994, “Sinn und unsinn formaler spezificationssprachen fuer wissensbasierte systeme” Kuenstliche Intelligenz (4) (in German).Google Scholar
Fensel, D, 1994b, “A case study on assumptions and limitations of a problem solving method”, 9th Banff Knowledge Acquisition for KBS Workshop, Banif, Canada, 02.Google Scholar
Fensel, D, 1995, The Knowledge-Based Acquisition and Representation Language KARL, Kluwer.CrossRefGoogle Scholar
Fensel, D and van Harmelen, F, 1994, “A comparison of languages which operationalise and formalise KADS models of expertise” The Knowledge Engineering Review 9 105–146.CrossRefGoogle Scholar
Fetzer, JH, 1988, “Program verification: The very idea” Communications of the ACM 31 09.CrossRefGoogle Scholar
Fox, J, 1993, “On the soundness and safety of expert systems” Artificial Intelligence in Medicine 5 159–179.CrossRefGoogle ScholarPubMed
Futatsugi, K, Goguen, J, Jouannaud, J and Meseguer, J, 1985, “Principles of OBJ2” In: Reid, BK (ed.) Proceedings of Twelfth Symposium on Principles of Programming Languages pp 52–66. ACM.Google Scholar
Gebhardt, F, 1995, “MoMo: language and case studies” Fabel-Report 36, GMC, Sankt Augustin, 07.Google Scholar
Giunchiglia, E and Traverso, P, 1995, “A multi-context architecture for formalizing complex reasoning” International Journal of Intelligent Systems 10 (5) 501–539, 05.CrossRefGoogle Scholar
Giunchiglia, E, Traverso, P and Giunchiglia, F, 1993, “Multi-context systems as a specification framework for complex reasoning systems” In Treur, J and Th, Wetter (eds.), Formal Specification of Complex Reasoning Systems Ellis Horwood.Google Scholar
Gurevich, Y, 1993, “Evolving algebras, a tutorial introduction” In Rozenberg, EG et al. (eds.), Current Trends in Computer Science World Scientific.Google Scholar
Hall, JA, 1990, “Seven myths of formal methods” IEEE Software 7 (5) 11–19, 09.CrossRefGoogle Scholar
Hard, D, 1984, “Dynamic logic” In Gabbay, D and Guenthner, F (eds.), Handbook of Philosophical Logic, Vol. II. extensions of Classical Logic pp 497–604. Reidel.Google Scholar
Heisel, M, Reif, W and Stephan, W, 1988, “Implementing verification strategies in the KIV-system” In Lusk, R and Overbeek, R (eds.), 9th International Conference on Automated Deduction (CADE'88) Number 310 in Lecture Notes in Computer Science pp 131–140, Argonne, Springer-Verlag.CrossRefGoogle Scholar
Heisel, M, Reif, W and Stephan, W, 1990, “Tactical theorem proving in program verification” In: Proceedings of the 10th International Conference on Automated Deduction (CA DE'90), Volume 449 of Lecture Notes on Computer Science Springer-Verlag.Google Scholar
Hinchey, M and Bowen, J, editors, 1995, Applications of Formal Methods International Series in Computer Science. Prentice-Hall.Google Scholar
Hoare, J, 1995, “Formal development of CICS with B” In: Hinchey, M and Bowen, J (eds.), Applications of Formal Methods Prentice-Hall.Google Scholar
in't Veld, L, Jonker, W and Spee, JW, 1994, “The specification of complex reasoning tasks in KBSSF” In Treur, J and Th, Wetter (eds.), Formal Specification of Computer Reasoning Systems pp 233–256Ellis Horwood.Google Scholar
Jackson, P, 1990, Introduction to Expert Systems Addison Wesley.Google Scholar
Jaurent, JP, Ayel, J, Thome, F and Ziebelin, D, 1986, “Comparative evaluation of three expert system development tools: KEE, knowledge craft, ART” Knowledge Engineering Review 1 (4) 19–29.Google Scholar
Jensen, K, 1987, “Coloured petri nets” In Brauer, W, Reisig, W and Rozenberg, G (eds.), Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986 Part I, volume 254 of Lecture Notes of Computer Science pp 248–299. Springer-Verlag.Google Scholar
Jonker, W, Spec, JW, in't Veld, L and Koopman, M, 1991, “Formal approaches towards design in SE and their role in KBS design” In: Proceedings of the IJCAI'91 Workshop on Software Engineering for Knowledge-Based Systems Sydney, Australia, 08.Google Scholar
Karbach, W, Voβ, A, Schukey, R, and Drouwen, U, 1991, “Model-K: Prototyping at the knowledge level” In: Proceedings Expert Systems-91 pp 501–512, Avignon, France.Google Scholar
Kassel, G and Greboval, C, 1993, “How AIDE succeeds in an example design task” In Treur, H and Th, Wetter (eds.), Formal Specification of Complex Reasoning Systems Ellis Horwood.Google Scholar
Keene, SE, 1984, Object-Oriented Programming in Common Lisp Addison-Wesley.Google Scholar
Krause, P, Fox, J, O'Neill, M and Glowinski, A, 1993, “Can we formally specify a medical decision support system” IEEE Expert 8 (3) 56–61.CrossRefGoogle Scholar
Landes, D and Studer, R, 1995, “The treatment of non-functional requirements in MIKE” In: Proceedings of the 5th European Software Engineering Conference (ESEC'95) Barcelona, Spain.Google Scholar
Linster, M, 1993, “Using the operational modeling language OMOS to represent KADS conceptual models” Knowledge Acquisition.Google Scholar
Löckenhoff, C, Fensel, D and Studer, R, editors, 1993, Proceedings of the Third KADS User Meeting ZFE BT SE 21, Otto-Hahn Ring 6, D-8000 Munich83, 8–9 03 Siemens AG.Google Scholar
Lydiard, T, 1992, “Overview of current practice and research initiatives of the verification and validation of KBS” Knowledge Engineering Review 7 (2) 101–113.CrossRefGoogle Scholar
Marcus, S, editor, 1988, Automatic Knowledge Acquisition for Expert Systems Kluwer.CrossRefGoogle Scholar
Milner, R, 1989, Communication and Concurrency International Series in Computer Science, Prentice-Hall.Google Scholar
Milnes, B, 1992, “A specification of the Soar cognitive architecture in Z”, Technical Report CMU-CS-92–169. Carnegie Mellon University, 08.Google Scholar
Musen, MA, 1989, Automated Generation of Model-Based Knowledge-Acquisition Tools Pitman.Google Scholar
Nakagawa, A, Sakakihara, T and Futatsugi, K, 1993, “Algebraich specification of reasoning systems” In: Treur, J and Wetter, Th (eds.), Formal Specification of Complex Reasoning Systems Ellis Horwood.Google Scholar
Newell, A, 1982, “The knowledge level” Artificial Intelligence 18 87–127.CrossRefGoogle Scholar
Parnas, D, 1995, “Using mathematical descriptions in the inspection of safety-critical software” In: Hinchey, M and Bowen, J (eds.), Applications of Formal Methods Prentice-Hall.Google Scholar
Peleska, J, Hamer, U and Hoercher, H-M, 1995, “The airbus a330/340 cabin communication system— a Z application” In: Hinchey, M and Bowen, J (eds.), Applications of Formal Methods Prentice-Hall.Google Scholar
Pierret-Goldbreich, C and Talon, X, 1995, “An algebraic specification of the dynamic behaviour of knowledge-based systems” The Knowledge Engineering Review (submitted).Google Scholar
Shadbolt, N, Aitken, S and Reichgelt, LH, 1992, “Representing kads models in QIL” Working Paper WP006, Al Group, University of Nottingham.Google Scholar
Schreiber, ATh and Terpstra, P, 1995, “Sisyphus-VT: A Common KADS solution” Internationalfournalof Human-Computer Studies (in press).Google Scholar
Sierra, A and Godo, L, 1993, “Specifying simple scheduling tasks in a reflective and modular architecture” In: Treur, J and Wetter, Th, editors, Formal Specification of Complex Reasoning Systems Ellis Horwood.Google Scholar
Spivey, JM, 1988, Understanding Z: A Specification Language and its Formal Semantics volume 3 of Cambridge Tracts in Theoretical Computer Science Cambridge University Press.Google Scholar
Spivey, JM, 1992, The Z Notation: A Reference Manual Series in Computer Science, Prentice Hall.Google Scholar
Spruit, P, Wieringa, R and Meyer, J-J, 1995, “Axiomatization, declarative semantics and operational semantics of passive and active updates in logic databases” Journal of Logic and Computation 5 (1).CrossRefGoogle Scholar
Todd, B and Stamper, R, 1993, The formal design and evaluation of a variety of medical diagnostic programs” Technical Monograph PRG-109, Oxford University Computing Laboratory, 09.Google Scholar
Treur, J, 1994, “Temporal semantics of meta-level architectures for dynamic control” In: Tribourg, L and Turini, F (eds.), Logic Program Synthesis and Transformation—Meta-Programming in Logic (LOPS TR'94– META'94) volume 883 of Lecture Notes in Computer Science pp 353–376, Springer-Verlag.CrossRefGoogle Scholar
Treur, J and Wetter, Th, editors, 1993, Formal Specification of Complex Reasoning Systems Workshop Series, Ellis Horwood.Google Scholar
Treur, J and Willems, M, 1994, “A logical foundation for verification” In Cohn, T (ed.), Proceedings of the 11th European Conference on AI (ECAI'94) pp 745–749, 08. Wiley.Google Scholar
Ueberreiter, B and Voβ, A, editors, 1991, Materials KADS User Meeting, February 14/15 1991 Siemens AG ZFE IS INF 32, Munich Perlach, Germany (in German).Google Scholar
van Harmelen, F, and Aben, M, 1995, “Structure preserving specification languages for knowledge-based systems” International Journal of Human Computer Studies (formerly Journal of Man Machine Studies).CrossRefGoogle Scholar
van, Harmelen F and Balder, JR, 1992, “(ML)2: a formal language for KADS models of expertise” Knowledge Acquisition 4(1). (Special issue: ‘The KADS approach to knowledge engineering’,Google Scholar
reprinted in KADS: A Principled Approach to Knowledge-Based System Development, 1993, Schreiber, Ath et al. , editors).Google Scholar
van Langevelde, LA, Philipsen, AW and Treur, J, 1992, “Formal specification of compositional architecture” In: Neumann, B (ed.), Proceedings ECAI'92 Vienna, pp 272–276. Wiley. (Longer version available as: Report IR-282, Mathematics and Computer Science, Free University of Amsterdam.)Google Scholar
van Melle, W, 1979, “A domain independent production rule system for consultation programs” In: IJCAI-79 pp 923–925.Google Scholar
Velthuijsen, H, 1992, “The nature and applicability of the blackboard architecture” PhD thesis, University of Limburgh, Maastricht, The Netherlands.Google Scholar
Velthuijsen, H and Braspenning, P, 1991, “A conceptual and formal study of the blackboard architecture” In: Moskilde, E (ed.), Proceedings of the European Simulation Multi-Conference (ESM'91) pp 374–379, Copenhagen. The Society for Computer Simulation.Google Scholar
Voss, H and Voss, A, 1993, “Reuse-oriented knowledge engineering with MoMo” In: Proceedings of the 5th International Conference on Software Engineering and Knowledge Engineering (SEKE'93) San Francisco, 06.Google Scholar
Wetter, J, 1990, “First-order logic foundation of the KADS conceptual model” In: Wielinga, BJ, Boose, J, Gaines, B, Schreiber, G and van Someren, M (eds.), Current Trends in Knowledge Acquisition pp 356–375, Amsterdam, The Netherlands, 05. IOS Press.Google Scholar
Wetter, Th and Schmidt, W, 1991, “Formalization of KADS interpretation models” In: Steels, L and Smith, B, editors, AISB91, Artificial Intelligence and Simulation of Behavior Springer-Verlag.Google Scholar
Wielinga, BJ and Breuker, JA, 1986, “Models of expertise” In: Proceedings ECAI-86, pp 306–318.Google Scholar
Wielinga, BJ, Schreiber, ATh and Breuker, JA, 1992. “KADS: A modelling approach to knowledge engineering” Knowledge Acquisition 4 (1) 5–53. (Special issue ‘The KADS approach to knowledge engineering’.CrossRefGoogle Scholar
Reprinted in: Buchanan, B and Wilkins, D, editors, 1992, Readings in Knowledge Acquisition and Learning Morgan Kaufmann, pp 92–116.)Google Scholar
Wing, JM, 1990, “A specifier's introduction to formal methods” IEEE Computer 23 (9) 10–24, 09.CrossRefGoogle Scholar
Zave, P, 1991, “An insiders evaluation of PAISLey” IEEE Transactions on Software Engineering 18 (3) 212–225.CrossRefGoogle Scholar