Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/53647
Title: Transformations between CSP# and C#
Authors: ZHU HUIQUAN
Keywords: Formal Verification, Model Checking, Concurrent Systems, CSP#, C#
Issue Date: 11-Jul-2013
Source: ZHU HUIQUAN (2013-07-11). Transformations between CSP# and C#. ScholarBank@NUS Repository.
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.
URI: http://scholarbank.nus.edu.sg/handle/10635/53647
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
ZhuHQ.pdf1.03 MBAdobe PDF

OPEN

NoneView/Download

Page view(s)

66
checked on Dec 11, 2017

Download(s)

138
checked on Dec 11, 2017

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.