Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/13642
Title: A verification study based on the CTP model
Authors: KAMRUL HASAN TALUKDER
Keywords: Message Sequence Charts, Verification,CTP model, SMV, CTL,Event Structures
Issue Date: 13-Feb-2004
Source: KAMRUL HASAN TALUKDER (2004-02-13). A verification study based on the CTP model. ScholarBank@NUS Repository.
Abstract: Message Sequence Charts (MSCs) are an appealing visual formalism mainly used inthe early stages of system design to capture the system requirements. However, if wemove towards an implementation, an executable specifications related in some fashionto the MSC-based requirements must be obtained. The main difficulty here is that theinter-object interactions described in forms of MSCs must be synthesized asexecutable specifications given in terms of intra-object behaviors. A. Roychoudhuryand P. S. Thiagarajan proposed an executable formalism called CommunicatingTransaction Processes (CTP) that uses MSCs to construct executable specifications ina more direct way. The proposed CTP model uses high-level transition systems tocapture the control flow of the system components (agents) and MSCs to describe thenon-atomic component interactions. This model is amenable to formal verification. Inthis thesis, we present a verification study based on the proposed CTP model. We havecontributed significantly to the following tasks in this respect. Firstly, the syntax tospecify the CTP model has been formulated. The CTP model is described in a textualinput file using that syntax. Secondly, a translator that translates the CTP specificationsinto Symbolic Model Verifier (SMV) programs has been constructed. Thirdly, we havemodeled the major features of the AMBA bus protocol though CTP model. This modelhas been translated into SMV program using CTP-SMV translator. Finally, automaticverification of the protocol is done using the SMV program.
URI: http://scholarbank.nus.edu.sg/handle/10635/13642
Appears in Collections:Master's Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
Verification_CTP.pdf341.87 kBAdobe PDF

OPEN

NoneView/Download

Page view(s)

206
checked on Dec 11, 2017

Download(s)

146
checked on Dec 11, 2017

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.