Mapping BoxTalk to Promela Model
Loading...
Date
2007-06-13T13:28:16Z
Authors
Peng, Yuan
Journal Title
Journal ISSN
Volume Title
Publisher
University of Waterloo
Abstract
A telecommunication feature is an optional or incremental unit of functionality, such as call display (CD) and call forwarding (CF). A feature interaction occurs when, in the presence of other features, the actual behavior of a feature becomes inconsistent with its specified behavior. This feature interaction problem is a long-existing problem in telephony, and it becomes an increasingly pressing problem as more and more sophisticated features are developed and put into use. It takes a lot of effort to test that the addition of a new feature to a system doesn’t affect any existing features in an undesired way.
Distributed Feature Composition (DFC) proposed by Michael Jackson and Pamela Zave, is an architectural approach to the feature interaction problem. Telecommunication features are modeled as independent components, which we call boxes. Boxes are composed in a pipe-and-filter-like sequence to form an end-to-end call. Our work studies the behaviour of single feature boxes. We translate BoxTalk specifications into another format, that is more conducive to automated reasoning. We build formal models on the translated format, then the formal models are checked by a model checker, SPIN, against DFC compliance properties written in Linear Temporal Logic (LTL). From BoxTalk specifications to Promela models, the translation takes steps: 1) Explicating BoxTalk, which expands BoxTalk macros and presents its implicit behaviours as explicit transitions. 2) Define BoxTalk semantics in terms of Template Semantics. 3) Construct Promela model from Template Semantics HTS. Our case studies exercised this translation process, and the resulting models are proven to hold desired properties.
Description
Keywords
BoxTalk