Name
Abstract | ||
|---|---|---|
This paper demonstrates an embedding of the semantic models of the cCSP process algebra in the general purpose theorem prover PVS. cCSP is a language designed to model long-running business transactions with constructs for orchestration of compensations. The cCSP process algebra terms are defined in PVS by using mutually recursive datatype. The trace and the operational semantics of the algebra are embedded in PVS. We show how these semantic embeddings are used to define and prove a relationship between the semantic models by using the powerful induction mechanism of PVS. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1016/j.entcs.2009.08.020 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
semantic model,embedding,process algebra,operational semantics,theorem prover | Discrete mathematics,Operational semantics,Embedding,General purpose,Computer science,Automated theorem proving,Theoretical computer science,Business transactions,Process calculus,Orchestration (computing),Recursion | Journal |
Volume | Issue | ISSN |
250 | 2 | 1571-0661 |
Citations | PageRank | References |
6 | 0.50 | 12 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Shamim Ripon | 1 | 24 | 5.22 |
| Michael Butler | 2 | 1768 | 104.74 |