Model Checking of Concurrent Algorithms: From Java to C - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

Model Checking of Concurrent Algorithms: From Java to C

Résumé

Concurrent software is difficult to verify. Because the thread schedule is not controlled by the application, testing may miss defects that occur under specific thread schedules. This problem gave rise to software model checking, where the outcome of all possible thread schedules is analyzed. Among existing software model checkers for multi-threaded programs, Java PathFinder for Java bytecode is probably the most flexible one. We argue that compared to C programs, the virtual machine architecture of Java, combined with the absence of direct low-level memory access, lends itself to software model checking using a virtual machine approach. C model checkers, on the other hand, often use a stateless approach, where it is harder to avoid redundancy in the analysis. Because of this, we found it beneficial to prototype a concurrent algorithm in Java, and use the richer feature set of a Java model checker, before moving our implementation to C. As the thread models are nearly identical, such a transition does not incur high development cost. Our case studies confirm the potential of our approach.
Fichier principal
Vignette du fichier
final_008.pdf (236.93 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01054483 , version 1 (07-08-2014)

Licence

Paternité

Identifiants

Citer

Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Yoshinori Tanabe, Mitsuharu Yamamoto. Model Checking of Concurrent Algorithms: From Java to C. 7th IFIP TC 10 Working Conference on Distributed, Parallel and Biologically Inspired Systems (DIPES) / 3rd IFIP TC 10 International Conference on Biologically-Inspired Collaborative Computing (BICC) / Held as Part of World Computer Congress (WCC) , Sep 2010, Brisbane, Australia. pp.90-101, ⟨10.1007/978-3-642-15234-4_10⟩. ⟨hal-01054483⟩
135 Consultations
203 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More