| dc.description.abstract | Telecommunication systems are structured to enable incremental growth, so that new telecommunication features can be added to the set of existing features. With the addition of more features, certain existing features may exhibit unpredictable behaviour. This is known as the feature interaction problem, and it is very old problem in telecommunication systems. Jackson and Zave have proposed a technology, Distributed Feature Composition (DFC) to manage the feature interaction problem. DFC is a pipe-and-filter-like architecture where features are "filters" and communication channels connecting features are "pipes".
DFC does not prescribe how features are specified or programmed. Instead, Zave and Jackson have developed BoxTalk, a call-abstraction, domain-specific, high-level programming language for programming features. BoxTalk is based on the DFC protocol and it uses macros to combine common sequences of read and write actions, thus simplifying the details of the DFC protocol in feature models. BoxTalk features must adhere to the DFC protocol in order to be plugged into a DFC architecture (i.e., features must be "DFC compliant"). We want to use model checking to check whether a feature is DFC compliant. We express DFC compliance using a set of properties expressed as linear temporal logic formulas.
To use the model checker SPIN, BoxTalk features must be translated into Promela. Our automatic verification process comprises three steps:
1. Explicate BoxTalk features by expanding macros and introducing implicit details.
2. Mechanically translate explicated BoxTalk features into Promela models.
3. Verify the Promela models of features using the SPIN model checker.
We present a case study of BoxTalk features, describing the original features and how they are explicated and translated into Promela by our software, and how they are proven to be DFC compliant. | en |
