Transformations between CSP# and C#

Abstract

Concurrent software system contains multiple processes running in parallel and they synchronize with each other. Due to the complexity of concurrency, it is difficult to ensure the implemented system satisfying the desired concurrent properties. CSP# is a formal language that models concurrent systems on event and channel communications. After a CSP# model has been verified on the desired properties, it is usually implemented in the programming language, such as C#, used in target platform. This thesis discusses automatic techniques on transformation and verification between concurrent models in CSP# and their implementations in C#. A translation-based approach and a VM-based approach are proposed to verify properties on implemented C# programs. We also proposed an automatic code generation technique to transform CSP# models to C# programs. The generated C# programs preserve the verified properties on the original CSP# models.