Mapping BoxTalk to Promela Model

dc.contributor.authorPeng, Yuan
dc.date.accessioned2007-06-13T13:28:16Z
dc.date.available2007-06-13T13:28:16Z
dc.date.issued2007-06-13T13:28:16Z
dc.date.submitted2007
dc.description.abstractA 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.en
dc.format.extent848502 bytes
dc.format.mimetypeapplication/pdf
dc.identifier.urihttp://hdl.handle.net/10012/3094
dc.language.isoenen
dc.pendingfalseen
dc.publisherUniversity of Waterlooen
dc.subjectBoxTalken
dc.subject.programComputer Science (Software Engineering)en
dc.titleMapping BoxTalk to Promela Modelen
dc.typeMaster Thesisen
uws-etd.degreeMaster of Mathematicsen
uws-etd.degree.departmentSchool of Computer Scienceen
uws.peerReviewStatusUnrevieweden
uws.scholarLevelGraduateen
uws.typeOfResourceTexten

Files

Original bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
yuan_thesis.pdf
Size:
828.62 KB
Format:
Adobe Portable Document Format

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
245 B
Format:
Item-specific license agreed upon to submission
Description: