Proof search algorithms for detecting interactions in telecommunication features

Abstract

This thesis presents a theorem proving approach to automatically detecting feature interactions in telecommunications systems. Feature requirements are formalized as specifications using Linear Temporal Logic (LTL) formulas and feature conflicts are specified by LTL formulas expressing logical inconsistency of specifications of two requirements of two different features. These LTL formulas are translated into First-Order Logic (FOL) formulas. We begin with an existing FOL theorem prover and optimize and enrich this prover for our application. In particular, we develop algorithms for integers and relational expressions which appear in translated FOL formulas and integrate these algorithms into the existing proof search procedure. Implementation and experiments in lambdaProlog demonstrate that our theorem prover is efficient and powerful when applied to the task of feature interaction detection. We also develop a proof checker to verify proofs obtained from our prover.