Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Aspect-Oriented Ontology Development Read chapter Read first chapter

2018 | OriginalPaper | Chapter

Using the Event-B Formal Method and the Rodin Framework for Verification the Knowledge Base of an Rule-Based Expert System

Authors : Marius Brezovan, Costin Badica

Published in: Synergies Between Knowledge Engineering and Software Engineering

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Verification and validation of a knowledge base of an expert systems are distinct activities that allow to increase the quality and reliability of these systems. While validation ensures the compliance of a developed knowledge base with the initial requirements, the verification ensures that the knowledge base is logically consistent. Our work is focused on the verification activity, which is a difficult task that mainly consists in determination of potential structural errors of the knowledge base. More exactly, we aimed to study the consistency of knowledge bases of rule-based expert systems that use the forward chaining inference, a very important aspect in the verification activity, among others, such as completeness and correctness. We use Event-B as a modelling language because it has a mathematical background that allows to model a dynamic system by specifying its static and dynamic properties. In addition we use the Rodin platform, a support tool for Event-B, which allows to verify the correctness of the specified systems and its properties. For a better understanding of our method, an example written in the CLIPS language is presented in the paper.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Knowledge Engineering of System Refinement What We Learnt from Software Engineering
next chapter Knowledge Engineering for Distributed Case-Based Reasoning Systems
Literature
1.
Adrion, W., Branstad, M., Cherniavsky, J.: Validation, verification and testing of computer software. Comput. Surv. 14(2), 159–192 (1982)CrossRef
2.
Meseguer, P.: Towards a conceptual framework for expert system validation. AI Commun. 5(3), 119–135 (1992)
3.
Laurent, J.P.H.: Proposals for a valid terminology in KBS validation. In: Proceedings of the European Conference on Artificial Intelligence - ECAI, pp. 829–834. Wiley, Vienna, Austria (1992)
4.
Hoppe, T., Meseguer, P.: On the terminology of VVT: a proposal. IEEE Expert 93, 48–55 (1993)CrossRef
5.
Sommerville, I.: Software Engineering. Addison-Wesley, USA (2011)MATH
6.
Meseguer, P., Preece, A.: Verification and validation of knowledge-based systems with formal specifications. Knowl. Eng. Rev. 10(4), 331–343 (1995)CrossRef
7.
Preece, A.: Evaluating verification and validation methods in knowledge engineering. Industrial Knowledge Management, pp. 91–104. Springer, London (2001)CrossRef
8.
O’Keefe, R.M., O’Leary, D.E.: Expert system verification and validation: a survey and tutorial. Artif. Intell. Rev. 7(1), 3–42 (1993)CrossRef
9.
Meseguer, P.: A new method to checking rule bases for inconsistency: a petri net approach. In: Proceedings of ECAI 90, pp. 437–442. Espoo, Finland (1990)
10.
He, X., Yang, W.C.H., Yang, S.: A new approach to verify rule-based systems using petri nets. In: Proceedings of 23th Annual International Computer Software and Applications Conference, pp. 462–467. Los Alamitos, CA, USA (1999)
11.
Wu, C.H., Lee, S.J.: Enhanced high-level petri nets with multiple colors for knowledge verification/validation of rule-based expert systems. IEEE Trans. Syst. Man Cybern. Part B: Cybern. 27(5), 760–773 (1997)CrossRef
12.
Ramaswamy, M., Sarkar, S., Sho, C.Y.: Using directed hypergraphs to verify rule-based expert systems. IEEE Trans. Knowl. Data Eng. 9(2), 221–237 (1997)CrossRef
13.
Gursaran, G., Kanungo, S., Sinha, A.: Rule-base content verification using a digraph-based modelling approach. Artif. Intell. Eng. 13(3), 321–336 (1999)CrossRef
14.
Laita, L., Roanes-Lozano, E., de Ledesma, L., Alonso, J.: A computer algebra approach to verification and deduction in many valued knowledge systems. Soft Comput. 3(1), 7–19 (1999)CrossRef
15.
Pierret-Golbreich, C., Talon, X.: TFL: an algebraic language to specify the dynamic behaviour of knowledge-based systems. Knowl. Eng. Rev. 11, 253–280 (1996)CrossRef
16.
Baumeister, J., Seipel, D.: Anomalies in ontologies with rules. Web Semant. Sci. Serv. Agents World Wide Web 8(1), 55–68 (2010)CrossRef
17.
Krotzsch, M., Rudolph, S., Hitzler, P.: ELP: tractable rules for OWL. In: Proceedings of the 7th International Semantic Web Conference - ISVC, pp. 649–664. Springer (2008)
18.
19.
20.
Woodcock, J., Davies, J.: Using Z: Specification, Refinement and Proof. Prentice Hall, London (1996)MATH
21.
22.
Jones, C.: Systematic Software Development Using VDM. Prentice-Hall International, Englewood Cliffs (1986)MATH
23.
Abrial, J.R.: The B Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)CrossRefMATH
24.
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefMATH
25.
Kropf, T.: Introduction to Formal Hardware Verification. Springer, Berlin (1998)MATH
26.
Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)CrossRef
27.
Hoare, C.: Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs (1985)MATH
28.
Milner, R.: Communication and Concurrency. Prentice-Hall International, New York (1989)MATH
29.
Bidoit, M., Mosses, P.: CASH User Manual: Introduction to Using the Common Algebraic Specification. Lecture Notes in Computer Science, vol. 2900. Springer, Berlin (2004)CrossRefMATH
30.
Goguen, J., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT Press, Cambridge (1996)MATH
31.
32.
33.
Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185–203 (2008)CrossRef
34.
Butler, M., Maamria, I.: Practical theory extension in event-B. Theories of Programming and Formal Methods. Lecture Notes in Computer Science, vol. 8051, pp. 67–81. Springer, Berlin (2013)CrossRef
35.
36.
37.
Chan, W., Anderson, R.J., Beame, P., Burns, S., Modugno, F., Notkin, D., Reese, J.D.: Model checking large software specifications. IEEE Trans. Softw. Eng. 24(7), 498–520 (1998)CrossRef
38.
Nguyen, T., Perkins, W., Pecora, D.: Knowledge base verification. AI Mag. 8(2), 69–75 (1987)
Metadata
Title
Using the Event-B Formal Method and the Rodin Framework for Verification the Knowledge Base of an Rule-Based Expert System
Authors
Marius Brezovan
Costin Badica
Copyright Year
2018
Book
Synergies Between Knowledge Engineering and Software Engineering

Print ISBN: 978-3-319-64160-7

Electronic ISBN: 978-3-319-64161-4

Copyright Year: 2018

DOI
https://doi.org/10.1007/978-3-319-64161-4_6

Premium Partner

    Image Credits