Blogs (1) >>
ICSE 2019
Sat 25 - Fri 31 May 2019 Montreal, QC, Canada
Mon 27 May 2019 14:40 - 15:05 at Foyer - Session 3 Chair(s): Eunsuk Kang

In this paper, we use the process algebra CSP and the formal model-checker FDR to show that the implementation of one-to-one channel communication in the process-oriented language ProcessJ is correct. ProcessJ is a new process-oriented language with Java-like syntax and CSP-based communication using synchronous channels. ProcessJ allows for hundreds of millions of processes to be executed on a single processor core. ProcessJ generates Java code which eventually runs concurrently on the JVM using a cooperative scheduler. We use the translation from the ProcessJ code generator to translate ProcessJ to Java and further into CSP. We then utilize the FDR model-checker to show that the generated Java code behaves like a generic synchronous, blocking, non-buffered one-to-one channel used previously to show the correctness of channel communication in JCSP – a Java library that supports JVM thread-based concurrency. Finally, we highlight a lesson from verifying our behaviour using FDR – the ability to simplify our approach and show the implementation still meets our specification.

Mon 27 May

Formalise-2019-papers
14:00 - 15:30: FormaliSE 2019 - Session 3 at Foyer
Chair(s): Eunsuk KangCarnegie Mellon University
Formalise-2019-papers14:00 - 14:25
Full-paper
Hoang-Dung TranVanderbilt University, Patrick MusauVanderbilt University, Diego Manzanas LopezVanderbilt University, Xiao Dong YangVanderbilt University, Luan NguyenUniversity of Pennsylvania, Weiming XiangVanderbilt University, Taylor T JohnsonVanderbilt University
Formalise-2019-papers14:25 - 14:40
Short-paper
Maxime CordySnT, University of Luxembourg, Axel Legay, Sami LazregVisteon Electronics and Universite Cote d Azur, Philippe ColletUniversity of Nice
Formalise-2019-papers14:40 - 15:05
Full-paper
Jan PedersenUniversity of Nevada Las Vegas, Kevin ChalmersEdinburgh Napier University
Formalise-2019-papers15:05 - 15:30
Full-paper
Cláudio Belo LourençoLRI, Université Paris-Sud & INRIA Saclay, Maria João FradeHASLab/INESC TEC & Universidade do Minho, Portugal, Jorge Sousa PintoHASLab/INESC TEC & Universidade do Minho, Portugal