Computer Science – Logic in Computer Science
Scientific paper
2010-01-20
Computer Science
Logic in Computer Science
9 pages
Scientific paper
Compensating CSP (cCSP) is a language defined to model long running business transactions within the framework of standard CSP process algebra. In earlier work, we have defined both traces and operational semantics of the language. We have shown the consistency between the two semantic models by defining a relationship between them. Synchronization was missing from the earlier semantic definitions which is an important feature for any process algebra. In this paper, we address this issue by extending the syntax and semantics to support synchronization and define a relationship between the semantic models. Moreover, we improve the scalability of our proof technique by mechanically verifying the semantic relationship using theorem prover PVS. We show how to embed process algebra terms and semantics into PVS and to use these embeddings to prove the semantic relationship.
Butler Michael
Ripon Shamim H.
No associations
LandOfFree
Formalizing cCSP Synchronous Semantics in PVS 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 Formalizing cCSP Synchronous Semantics in PVS, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Formalizing cCSP Synchronous Semantics in PVS will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-128208