Model checking for Synchronous Java

In this paper, we present a model-checking toolset for a synchronous version of the Java language (Synchronous Java or in short sJava). The toolset includes a set of extensions to the Bandera and Bogor model-checking frameworks. It inherits thus a large number of advantages and features implemented in Bandera and Bogor. It supports the verification of the source models that are directly written in sJava. We developed a new algorithm for optimizing the synchronization tasks between threads. The toolset also generates the outputs that help developers to understand the source of errors and to correct the implementation of the input models in case of failure

Published in:
SEDE-2006, 15th International Conference on Software Engineering and Data Engineering, 7
International Society for Computers and Their Applications

 Record created 2007-01-11, last modified 2018-03-17

Rate this document:

Rate this document:
(Not yet reviewed)