Publication

Deadlock detection for synchronous Java

Duy Vo Duc
2007
Thèse EPFL
Résumé

The aim of this thesis is to construct toolsets that support the Synchronous Java programming language, an extension to the Java language that introduces a new method of synchronization between threads. The contributions of this thesis include a State Space Analyzer (SSAS) and a Deadlock Detector for Synchronous Java (DDSJ). As the first tool I developed an analyzer, the SSAS, that explores all the reachable states and all the possible execution paths of an sJava model. This exploration aims at the analysis of the communication between active threads and the detection of deadlocks in a given sJava model. When a deadlock is encountered, the toolset generates the error traces that help the developers to examine how the deadlocks were produced in the input model. The analyzer also generates the state space of the system model and a graphical representation of this state space. In the second toolset, the DDSJ, I developed an approach that reduces the number of states when verifying an sJava program in Bandera and Bogor, which are the toolsets that support the verification of Java models. If errors are detected when verifying an sJava model, DDSJ generates a counter-example that allows developers to simulate the execution of the given model to study how errors were produced. The outcomes of this thesis give the Synchronous Java developers more confidence in using this programming language. These toolsets provide a possibility to examine sJava programs and to refine them before they can be delivered as product.

À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.