Computer Science – Software Engineering
Scientific paper
2010-09-26
International Journal of the Computer, the Internet and Management, Vol 15, Number 3, 2007
Computer Science
Software Engineering
13 pages, International Journal of the Computer, the Internet and Management
Scientific paper
Message Sequence Charts (MSCs) are an appealing visual formalism mainly used in the early stages of system design to capture the system requirements. However, if we move towards an implementation, an executable specifications related in some fashion to the MSC-based requirements must be obtained. The MSCs can be used effectively to specify the bus protocol in the way where high-level transition systems is used to capture the control flow of the system components of the protocol and MSCs to describe the non-atomic component interactions. This system of specification is amenable to formal verification. In this paper, we present the way how we can specify the bus protocols using MSCs and how these specifications can be translated into program of verification tool (we have used Symbolic Model Verifier (SMV)) for the use of formal verification. We have contributed to the following tasks in this respect. Firstly, the way to specify the protocol using MSC has been presented. Secondly, a translator that translates the specifications (described in a textual input file) into SMV programs has been constructed. Finally, we have presented the verification result of the AMBA bus protocol using the SMV program found through the translation process. The SMV program found through the translation process can be used in order to automatically verify various properties of any bus protocol specified.
No associations
LandOfFree
Bus Protocols: MSC-Based Specifications and Translation into Program of Verification Tool for Formal Verification does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Bus Protocols: MSC-Based Specifications and Translation into Program of Verification Tool for Formal Verification, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Bus Protocols: MSC-Based Specifications and Translation into Program of Verification Tool for Formal Verification will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-561774