A Perspective on Formal Verification

Rose F. Gamble

Formal methods employ mathematical techniques to prove a program satisfies its specifications. Many have stated that the use of these methods provides the only means to truly guarantee a program is dependable [4,8]. Though the use of these methods can be susceptible to human error, they will still increase the dependability of a program. Additionally, using formal methods can uncover design problems or inefficiencies in a program. If knowledge base system (KBS) dependability is a goal, formal methods must become as integral a part of system development as software testing. However, we must overcome many obstacles before realizing this goal. The main objective of our research is to address the verification of knowledge based systems using formal methods. For the remainder of this paper, we outline (i) how formal methods can be used to verify KBSs that rely on rule-based programs, (ii) how these methods address issues of efficiency and concurrency, (iii) the lessons learned, and (iv) the future directions the research.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.