An ontology-based knowledge management framework for heterogeneous verification

Please download to get full document.

View again

of 191
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Information Report
Category:

Computer Science

Published:

Views: 3 | Pages: 191

Extension: PDF | Download: 0

Share
Related documents
Description
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.
Tags
Transcript
CARNEGIE MELLON UNIVERSITY CARNEGIE INSTITUTE OF TECHNOLOGY THESIS SU BM ITTED IN P A R T IA L FULFILLM ENT’ O F T H E R E Q U IR E M E N T S FO R T H E D E G R E E O F D O C T O R O F P H IL O S O P H Y TITLE ______ An Ontology-based Knowledge Management Framework_____ ________________________For Heterogeneous Verification_________________ PR ESEN TED B Y ____________________ Raiesh Kumar______________________ A C CEPTED BY TH E D EP A R T M E N T OF Electrical and Computer Engineering M AJOR PROFESSOR DATE DEPARTME1 DATE APPROVED BY THE COLLEGE COUNCIL &l~l l'ZJDO'7 C _ _ _ D jbXn DATE Reproduced with permission of the copyright owner. Further reproduction prohibited without permission. Reproduced with permission of the copyright owner. Further reproduction prohibited without permission. A n O n to lo g y -b a sed K n o w led g e M a n a g em en t F ram ew ork for H e te r o g e n e o u s V erification by R ajesh Kumar D issertation Presented to the Faculty of the Graduate School of the Department of Electrical and Computer Engineering at Carnegie Mellon University in P artial Fulfillment of the Requirements for the Degree of D octor o f Philosophy C arn egie M ello n U n iv ersity April 2007 Reproduced with permission of the copyright owner. Further reproduction prohibited without permission. UMI Number: 3264769 Copyright 2007 by Kumar, Rajesh All rights reserved. INFORMATION TO USERS The quality of this reproduction is dependent upon the quality of the copy submitted. Broken or indistinct print, colored or poor quality illustrations and photographs, print bleed-through, substandard margins, and improper alignment can adversely affect reproduction. In the unlikely event that the author did not send a complete manuscript and there are missing pages, these will be noted. Also, if unauthorized copyright material had to be removed, a note will indicate the deletion. ® UMI UMI Microform 3264769 Copyright 2007 by ProQuest Information and Learning Company. All rights reserved. This microform edition is protected against unauthorized copying under Title 17, United States Code. ProQuest Information and Learning Company 300 North Zeeb Road P.O. Box 1346 Ann Arbor, Ml 48106-1346 Reproduced with permission of the copyright owner. Further reproduction prohibited without permission. sit m%ifRfft fcfr, U sstw l wiT-swot % in , •SRPKnmm m wrt m f- 1w *86? ^ ^ snspf ,?^n?ir i" -^aFr Reproduced with permission of the copyright owner. Further reproduction prohibited without permission. Acknowledgm ents Standing at this exciting point to conclude my PhD dissertation, I recognize th a t I owe so much to so many people. I know th a t without their extremely helpful support and guidance, I would not have been able to finish my dissertation. First and foremost, I would like to express my deepest gratitude to my advisor Prof. Bruce Krogh, who guided me for the last 5 years in my research. Under his guidance I learnt w hat research is, how to do research, how to maintain a long term vision for my work while simultaneously working on immediate problems. He gave me complete freedom to pursue my research which started out with hybrid system model checking and evolved to this thesis. He encouraged me to seek guidance at different points of my work from other people, and not to be disappointed by temporary setbacks. At times he seemed to believe in me more than I did myself. I would like to express my very special thanks to Dr. Ashish Tiwari who has been a most helpful collaborator over the last couple of years. W ithout his very precious time and help on this research, this dissertation might have taken much more time and possible a very different form. He has been very approachable and responsive even with the geographical distance and three hour time difference. He convinced us th a t e-mail collaboration can work. I would also like to thank the other people I met during the course of my stay at CMU, most notably, Frank Pfenning, Peter Feiler, Phil Koopman and colleagues in the SVM project with whom I had interesting discussions. iii Reproduced with permission of the copyright owner. Further reproduction prohibited without permission. I would like to say a thank you to the staff in the ECE Departm ent as well, especially Lynn Philibin and Elaine Lawrence, for their help with all the paper work related to graduate requirements and project research. I would like to thank my office mates and colleagues at Carnegie Mellon whom I had the privilege to work with - Jim Kapinski, Dong Jia, and Zhi Han in particular with whom I shared my office for many years. I would like to thank my brother who has been my best friend and a source of support. And last, b u t not the least, I want to thank Paula Moreci without whose help the thesis might not have been completed. R a je s h K um ar Carnegie Mellon University April 2007 IV Reproduced with permission of the copyright owner. Further reproduction prohibited without permission. A bstract 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 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 th a t build on and extend recent research on ontologies and logic programming. We give a new logic programming language E O LC , which is the logical foundation of our knowledge management tool and give algorithms for inferencing, i.e., evaluating queries, in E O L C and computing abductive explanations in order to augment the knowledge base. v Reproduced with permission of the copyright owner. Further reproduction prohibited without permission. C ontents A cknow ledgm ents iii A bstract v List o f Figures x List o f Tables x iv C hapter 1 In trod u ction 1 C hapter 2 B ackground and R ela ted W ork 9 2.1 O ntologies...................................................................................................... 9 2.2 Logic Programming .................................................................................. 12 2.3 Abduction in L o g ic ...................................................................................... 14 2.4 Logic Programming T erm in o lo g y............................................................ 16 2.5 Verification of Embedded Control S y stem s............................................ 19 C hapter 3 A P relim inary C ase S tu d y 21 3.1 Overview ...................................................................................................... 22 3.2 Design and VerificationP ro c e s s ................................................................. 24 3.3 Static O n to lo g y ............................................................................................ 27 3.4 Epistemic O ntology...................................................................................... 29 vi Reproduced with permission of the copyright owner. Further reproduction prohibited without permission. 3.5 Heterogeneous V erification......................................................................... 31 3.6 S u m m a r y ...................................................................................................... 32 C hapter 4 E p istem ic O ntology L anguage w ith C onstraints: E O L C 35 4.1 S y n ta x ............................................................................................................ 36 4.2 Semantics of E O L C .................................................................................. 42 4.3 Four Logic Values in E O L C ........................................ 45 4.3.1 Behavior of -> ......................................... 46 4.3.2 Behavior of AND (A ) ..................................................................... 47 4.3.3 Behavior D (implication) ............................................................. 47 4.3.4 Behavior of n o t ..................................................................................... 49 4.4 E O L C as a Knowledge Representation L an g u ag e............................... 49 4.5 S u m m a r y ...................................................................................................... 52 C hapter 5 Inferencing in E O L C 53 5.1 Model co m p u tatio n...................................................................................... 53 5.2 Algorithm to Compute a Maximal M o d e l ............................................ 56 5.3 Improvements to Algorithm 1 .................................................................. 63 5.3.1 Definitions ................................................................................... 64 5.3.2 Restricting the Instantiated P ro g ram .......................................... 65 5.4 Complexity a n a l y s i s ........................................................ 67 5.4.1 Base A n aly sis................................................................................... 68 5.4.2 Complexity Analysis of Improved A lgorithm ............................. 69 5.5 S u m m a r y ...................................................................................................... 71 C hapter 6 A b d u ction w ith R u le Priorities: T argeted K now ledge A cq u isition 72 6.1 Courteous Logic P ro g ra m s......................................................................... 73 6.2 Abduction in Courteous Logic P ro g ra m s ............................................... 75 vii Reproduced with permission of the copyright owner. Further reproduction prohibited without permission. 6.3 Abduction with Priorities for Diagnosis ............................................... 80 6.4 Explanation C o m p u ta tio n ......................................................................... 81 6.5 Complexity A n a ly s is ................................................................................... 88 6.6 S u m m a r y ...................................................................................................... 88 C hapter 7 Im p lem en tation 90 7.1 P r o t e g e ......................................................................................................... 90 7.2 HV tool A rch itectu re................................................................................... 92 7.3 Tool D e s c r ip tio n ......................................................................................... 93 7.3.1 Static O n tology................................................................................. 95 7.3.2 Epistemic Ontology ....................................................................... 96 7.4 S u m m a r y ...................................................................................................... 98 C hapter 8 A p p lication s to H eterogen eou s V erification 100 8.1 Case 1: A Flight Guidance System A p p lic a tio n ........................................ 101 8.1.1 O v e rv ie w ...............................................................................................102 8.1.2 Heterogeneous Verification..................................................................106 8.1.3 S u m m a r y .............................................................................................. 108 8.2 Case 2: A Wheel Braking System A p p licatio n .......................................... 109 8.2.1 O v e rv ie w ............................................................. 110 8.2.2 Heterogeneous Verification..................................................................112 8.2.3 S u m m a r y ...............................................................................................113 8.3 Targeted Knowledge A c q u is itio n .................................................................114 8.4 Empirical Performance E v a lu a tio n ..............................................................116 8.4.1 Experimental S e t u p ........................................................................... 117 8 .4 .2 R e s u lts ......................................................................................................................... 1 1 7 8.5 S u m m a r y .......................................................................................................... 122 viii Reproduced with permission of the copyright owner. Further reproduction prohibited without permission. C hapter 9 C onclusion 124 9.1 Summary of C ontributions......................................... 124 9.2 Future Research D ir e c tio n s ..........................................................................126 9.2.1 Expressiveness of E O L C .................................................................126 9.2.2 Manageability of Ontology ..............................................................127 9.2.3 Targeted Knowledge A c q u is itio n ....................................................128 B ibliography 129 A p p en d ix A Pow er W in d ow C ase S tu d y 142 A p p en d ix B A b d u ctio n 154 A p p en d ix C O ntology for th e dual FG S and W B S case stu d ies 160 C .l Static O n to lo g y .................................................................................................160 C.2 Epistemic O ntology.......................................................................................... 163 A p p en d ix D Specifications 167 D .l Dual FGS S pecifications.................................................................................167 D.2 Wheel Braking System Specifications.......................................................... 169 A p p en d ix E P erform ance E valuation 172 ix Reproduced with permission of the copyright owner. Further reproduction prohibited without permission. List of Figures 1.1 Elements of the ontology-based framework for heterogeneous verifi­ cation................................................................................................................ 5 2.1 Example ontology from a biological application [110]............................ 11 3.1 The power window system........................ ................................................... 22 3.2 The power window controller....................................................................... 23 3.3 Statechart model of the power window controller................................... 25 3.4 State transition diagram of the power window controller...................... 25 3.5 Low order window model.............................................................................. 26 3.6 High order window model............................................................................ 26 3.7 The representation of requirement 3(f) in Protege................................. 28 4.1 Example: E \ .................................................................................................... 37 4.2 Sample E O L C program to illustrate why well-grounded rule instances are needed........................................................................................................ 44 4.3 Belnap’s tru th space [13].............................................................................. 46 4.4 Truth table for -i............................................................................................ 46 4.5 Truth table for A if comma (V) is taken as the representation of conjunction (A)............................................................................................... 47 4.6 Truth table for the operational behavior of ‘ ’ interpreted as implication. 4 8 x Reproduced with permission of the copyright owner. Further reproduction prohibited without permission. 4.7 Truth table for D if colon is taken as the representation of im­ plication ( d ) .......................... 48 4.8 Truth table for n o t....................................................................................... 49 4.9 Access control................................................................................................ 50 4.10 Verification management............................................................................. 51 4.11 Multiple levels of selection.......................................................................... 51 5.1 A part of the atom dependency graph forthe E O L C program E \. Note the cliques involving the recursive predicates ‘satisfies’ and ‘sub­ model’............................................................................................................... 55 5.2 Sample E O L C program: E 2 ..................................................................... 63 5.3 E ? std............................................................................................................... 63 5-4 E C f dMd.................................... 63 6.1 Example courteous logic program .............................................................. 78 6.2 Labelled atom-dependency graph for example in Figure 6.1................. 78 6.3 Dental diagnostic knowledge....................................................................... 80 7.1 The representation of ontology in Protege. The selected class Model has one subclass - D iscreteM odel. The right side shows the slots for the Model class. The restrictions for the template slots are specified using facets...................................................................................................... 91 7.2 Mapping of KB to ground predicates........................................................ 92 7.3 Implementation architecture of HV framework....................................... 93 7.4 HV tool: Rules ta b ........................................................................................ 94 7.5 HV tool: Queries ta b ................................................................................. . 95 8.1 Elements of a flight control system from [79].............................................. 102 8.2 Wheel Braking System from [61]................................................................... I l l xi Reproduced with permission of the copyright owner. Further reproduction prohibited without permission. 8.3 TKA illustration: dual FGS system wrt Property 2(d)..............................115 8.4 TKA illustration: dual FGS system wrt Property 2(e).............................. 115 8.5 TKA illustration: WBS wrt property 1 (b) (ii)........................................... 116 8.6 A generated program: num_head_pred = 3 and num_assert = 2. . . . 118 8.7 Execution times as the number of rules increases for num _assert = 2. Query complexities shown in the legend vary from 2 to 6................... 119 8.8 Execution times as the number of rules increases for num _assert = 10. Query complexities shown in the legend vary from 2 to 6..................121 8.9 Execution times as the num _assert increases for num_head_pred = 50. Query complexities shown in the legend vary from 2 to 6..................122 A .l Relational database schema representation of the constraint part of the base ontology. .......................................................................................... 146 A, 2 Relational database schema representation of the system part of base ontology (see Fig. A .l for legend).................................................................. 147 A.3 Relational database schema representation of the constraint part of the base onto
Recommended
View more...
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks
SAVE OUR EARTH

We need your sign to support Project to invent "SMART AND CONTROLLABLE REFLECTIVE BALLOONS" to cover the Sun and Save Our Earth.

More details...

Sign Now!

We are very appreciated for your Prompt Action!

x