Sciweavers

Share
B
2007
Springer

Automatic Translation from Combined B and CSP Specification to Java Programs

9 years 6 days ago
Automatic Translation from Combined B and CSP Specification to Java Programs
Abstract. A recent contribution to the formal specification and verification of concurrent systems is the integration of the state- and event-based approaches B and CSP, specifically in the ProB model checking tool. At the implementation end of the development, concurrent programming in Java remains a demanding and error-prone activity, because of the need to verify critical properties of safety and liveness as well as functional correctness. This work contributes to the automated development of concurrent Java programs from such integrated specifications. The JCSP package was originally designed as a proven clean Java concurrency vehicle for the implementation of certain CSP specifications. In the context of best current Java concurrent programming practice, we extend the original JCSP package to support the integrated B and CSP specification by implementing new channel classes. We propose rules for the automated translation of the integrated specification to multi-threaded Java using...
Letu Yang, Michael Poppleton
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2007
Where B
Authors Letu Yang, Michael Poppleton
Comments (0)
books