Using formal methods, a formally specified system is automatically checked to see if it satisfies a specification given in a formal language. Formal methods provide rigorous guarantees about the correctness of a system in contrast to informal testing. Comprehensive verification of designs must, however, incorporate information from other sources, ranging from engineering insight to simulation studies. An integration mechanism is needed to bring together the results of disparate verification efforts and analysis techniques. We refer to this task of amalgamating heterogeneous analysis results as heterogeneous verification.
In this thesis, we present a formal framework for knowledge management and its application to facilitate the task of managing information from heterogeneous analyses. Our approach is built around a formal knowledge base. We develop tools to support heterogeneous verification that build on and extend recent research on ontologies and logic programming. We give a new logic programming language EOLC, which is the logical foundation of our knowledge management tool and give algorithms for inferencing, i.e., evaluating queries, in EOLC and computing abductive explanations in order to augment the knowledge base.
|School:||Carnegie Mellon University|
|School Location:||United States -- Pennsylvania|
|Source:||DAI-B 68/05, Dissertation Abstracts International|
|Subjects:||Electrical engineering, Computer science|
|Keywords:||Embedded systems, Heterogeneous verification|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
supplemental files is subject to the ProQuest Terms and Conditions of use.