- Abstract:
-
We report on an initial success obtained in investigating the Feature Interaction problem (FI) via proof planning. FIs arise as an unwanted/unexpected behaviour in large telephone networks and have recently attracted interest not only from the Computer Science community but also from the industrial world. So far, FIs have been solved mainly via approximation plus finite-state methods (model checking being the most popular); in our work we attack the problem via proof planning in First-Order Linear Temporal Logic (FOLTL), therefore making use of no finite-state approximation or restricting assumption about quantification. We have integrated the proof planner lambda-CLAM with an object-level FOLTL theorem prover called FTL, and have so far re-discovered a feature interaction in a basic (but far from trivial) example.
- Copyright:
- 2002 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @InProceedings{EDI-INF-RR-0153,
- author = {
Claudio Castellini
and Alan Smaill
},
- title = {Proof Planning for Feature Interactions: a preliminary report},
- book title = {Proceedings of LPAR 2002},
- year = 2002,
- month = {Oct},
- }
|
