Search
 
loader loading subjects...
cover
Verification of JCSP Programs
Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt
203 - 218
Concurrent Systems Engineering Series
Volume 63: Communicating Process Architectures 2005
Abstract

We describe the first proof system for concurrent programs based on Communicating Sequential Processes for Java (JCSP). The system extends a complete calculus for the JavaCard Dynamic Logic with support for JCSP, which is modeled in terms of the CSP process algebra. Together with a novel efficient calculus for CSP, a rule system is obtained that enables JCSP programs to be executed symbolically and to be checked against temporal properties. The proof system has been implemented within the KeY tool and is publicly available.

$35.00 / €27.50 / £22.00
Add PDF to cart