Please use this identifier to cite or link to this item: https://hdl.handle.net/10356/83777
Title: From verified model to executable program: the PAT approach
Authors: Zhu, Huiquan
Sun, Jing
Dong, Jin Song
Lin, Shang-Wei
Keywords: Modeling Checking
CSP#
Issue Date: 2015
Source: Zhu, H., Sun, J., Dong, J. S., & Lin, S.-W. (2016). From verified model to executable program: the PAT approach. Innovations in Systems and Software Engineering, 12(1), 1-26.
Series/Report no.: Innovations in Systems and Software Engineering
Abstract: CSP# is a formal modeling language that emphasizes the design of communication in concurrent systems. PAT framework provides a model checking environment for the simulation and verification of CSP# models. Although the desired properties can be formally verified at the design level, it is not always straightforward to ensure the correctness of the system’s implementation conforms to the behaviors of the formal design model. To avoid human error and enhance productivity, it would be beneficial to have a tool support to automatically generate the executable programs from their corresponding formal models. In this paper, we propose such a solution for translating verified CSP# models into C# programs in the PAT framework. We encoded the CSP# operators in a C# library-“PAT.Runtime”, where the event synchronization is based on the “Monitor” class in C#. The precondition and choice layers are built on top of the CSP event synchronization to support language-specific features. We further developed a code generation tool to automatically transform CSP# models into multi-threaded C# programs. We proved that the generated C# program and original CSP# model are equivalent on the trace semantics. This equivalence guarantees that the verified properties of the CSP# models are preserved in the generated C# programs. Furthermore, based on the existing implementation of choice operator, we improved the synchronization mechanism by pruning the unnecessary communications among the choice operators. The experiment results showed that the improved mechanism notably outperforms the standard JCSP library.
URI: https://hdl.handle.net/10356/83777
http://hdl.handle.net/10220/42797
ISSN: 1614-5046
DOI: 10.1007/s11334-015-0269-z
Rights: © 2015 Springer-Verlag London Limited. This is the author created version of a work that has been peer reviewed and accepted for publication by Innovations in Systems and Software Engineering, Springer-Verlag London Limited. It incorporates referee’s comments but changes resulting from the publishing process, such as copyediting, structural formatting, may not be reflected in this document. The published version is available at: [http://dx.doi.org/10.1007/s11334-015-0269-z].
Fulltext Permission: open
Fulltext Availability: With Fulltext
Appears in Collections:SCSE Journal Articles

Files in This Item:
File Description SizeFormat 
From verified model to executable program _ the PAT approach.pdf731.05 kBAdobe PDFThumbnail
View/Open

SCOPUSTM   
Citations 20

8
checked on Sep 5, 2020

WEB OF SCIENCETM
Citations 50

4
checked on Oct 19, 2020

Page view(s) 50

218
checked on Oct 25, 2020

Download(s) 50

64
checked on Oct 25, 2020

Google ScholarTM

Check

Altmetric


Plumx

Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.