A verification study based on the CTP model

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.