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 the extended JCSP channel classes. We briefly present a prototype translation tool which extends ProB, with a worked example, and conclude with a strategy for formally verifying the translation.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bert, D., Boulmé, S., Potet, M.-L., Requet, A., Voisin, L.: Adaptable Translator of B Specifications to Embedded C Programs. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 94–113. Springer, Heidelberg (2003)
Butler, M.J., Leuschel, M.: Combining CSP and B for Specification and Property Verification. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 221–236. Springer, Heidelberg (2005)
Brörken, M., Möller, M.: Jassda Trance Assertions: Runtime Checking the Dynamic of Java Programs. In: International Conference on Testing of Communicating Systems (2002)
Butler, M.J.: csp2B: A Practical Approach to Combining CSP and B. In: World Congress on Formal Methods, pp. 490–508 (1999)
Formal Systems (Europoe) Ltd.: Failures-Divergence Refinement: FDR2 User Manual (2003)
Goetz, B.: Concurrency in JDK 5.0. Technical report, IBM (2004)
Lawrence, J.: Practical Application of CSP and FDR to Software Design. In: 25 Years Communicating Sequential Processes, pp. 151–174 (2004)
Peleska, J.: Applied Formal Methods - From CSP to Executable Hybrid Specifications. In: 25 Years Communicating Sequential Processes, pp. 293–320 (2004)
Abrial, J.-R.: The B-Book: Assigning Programs toMeanings. Cambridge University Press, Cambridge (1996)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Muller, P., Kiniry, J.: JML Reference Manual (2005)
Magee, J., Kramer, J.: Concurrency: State Models & Java Programs. John Wiley and Sons, Chichester (1999)
Manson, J., Pugh, W., Adve, S.V.: The Java Memory Model. In: POPL 2005: Proceedings of the 32nd ACM SIGPLAN-SIGACT, pp. 378–391. ACM Press, New York (2005)
Muller, H., Walrath, K.: Threads and Swing, http://java.sun.com/products/jfc/tsc/articles/threads/threads1.html
Oliveira, M., Cavalcanti, A.: From Circus to JCSP. In: Sixth International Conference on Formal Engineering Methods (November 2004)
Pugh, W.: The Java Memory Model is Fatally Flawed. Concurrency: Practice and Experience 12(6), 445–455 (2000)
Welch, P.H., Martin, J.M.: A CSP Model for Java Multithreading. In: ICSE 2000, pp. 114–122 (2000)
Welch, P.H., Martin, J.M.: Formal Analysis of Concurrent Java System. In: Communicating Process Architectures (2000)
Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Englewood Cliffs (1989)
Raju, V., Rong, L., Stiles, G.S.: Automatic Conversion of CSP to CTJ, JCSP, and CCSP. In: Communicating Process Architectures 2003, pp. 63–81 (2003)
Schneider, S., Delicata, R.: Verifying Security Protocols: An Application of CSP. In: 25 Years Communicating Sequential Processes, pp. 243–263 (2004)
Schneider, S.: Concurrent and Real-Time System: The CSP Approach. John Wiley and Sons LTD, Chichester (2000)
S.-T. M. Limited.: Occam 2.1 Reference Manual (1995)
Treharne, H., Schneider, S.: Using a Process Algebra to Control B Operations. In: IFM, pp. 437–456 (1999)
Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: Int. Conf. on Automated Software Engineering (2000)
Voisinet, J.C., Tatibouet, B., Hammand, A.: JBTools: An experimental platform for the formal B method. In: PPPJ 2002, pp. 137–140 (2002)
Welch, P.: Wow, no chicken?, http://wotug.ukc.ac.uk/parallel/groups/wotug/java/discussion/3.html
Welch, P.H., Martin, J.M.: Formal Analysis of Concurrent Java System. In: Communicating Process Architectures (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yang, L., Poppleton, M.R. (2006). Automatic Translation from Combined B and CSP Specification to Java Programs. In: Julliand, J., Kouchnarenko, O. (eds) B 2007: Formal Specification and Development in B. B 2007. Lecture Notes in Computer Science, vol 4355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11955757_8
Download citation
DOI: https://doi.org/10.1007/11955757_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68760-3
Online ISBN: 978-3-540-68761-0
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.