KIT | KIT-Bibliothek | Impressum

NORA/HAMMR: Making Deduction-Based Software Component Retrieval Practical

Fischer, Bernd; Schumann, Johann

Abstract: Deduction-based software component retrieval uses pre- and postconditions as indexes and search keys and an automated theorem prover (ATP) to check whether a component matches. This idea is very simple but the vast number of arising proof tasks makes a practical implementation very hard. We thus pass the components through a chain of filters of increasing deductive power. In this chain, rejection filters based on signature matching and model checking techniques are used to rule out non-matches as early as possible and to prevent the subsequent ATP from "drowning". Hence, intermediate results of reasonable precision are available at (almost) any time of the retrieval process. The final ATP step then works as a confirmation filter to lift the precision of the answer set. We implemented a chain which runs fully automatically and uses MACE for model checking and SETHEO as ATP and evaluated it over a medium-sized collection of components. The results confirm the practicality of our approach.

Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Proceedingsbeitrag
Jahr 1997
Sprache Englisch
Identifikator ISBN: 0-8186-7961-1
KITopen ID: 1000017603
Erschienen in Proceedings / 12th IEEE International Conference Automated Software Engineering, November 1-5, 1997, Incline Village, Nevada, USA. Ed.: Bob Werner
Verlag IEEE Computer Society, Los Alamitos (Calif.)
Seiten 246 - 254
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page