Model Checking of Concurrent Algorithms: From Java to C

Abstract : 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.
Type de document :
Communication dans un congrès
Mike Hinchey; Bernd Kleinjohann; Lisa Kleinjohann; Peter A. Lindsay; Franz J. Rammig; Jon Timmis; Marilyn Wolf. 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. Springer, IFIP Advances in Information and Communication Technology, AICT-329, pp.90-101, 2010, Distributed, Parallel and Biologically Inspired Systems. 〈10.1007/978-3-642-15234-4_10〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01054483
Contributeur : Hal Ifip <>
Soumis le : jeudi 7 août 2014 - 11:15:08
Dernière modification le : samedi 16 décembre 2017 - 06:54:03
Document(s) archivé(s) le : mercredi 26 novembre 2014 - 01:06:44

Fichier

final_008.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Yoshinori Tanabe, Mitsuharu Yamamoto. Model Checking of Concurrent Algorithms: From Java to C. Mike Hinchey; Bernd Kleinjohann; Lisa Kleinjohann; Peter A. Lindsay; Franz J. Rammig; Jon Timmis; Marilyn Wolf. 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. Springer, IFIP Advances in Information and Communication Technology, AICT-329, pp.90-101, 2010, Distributed, Parallel and Biologically Inspired Systems. 〈10.1007/978-3-642-15234-4_10〉. 〈hal-01054483〉

Partager

Métriques

Consultations de la notice

191

Téléchargements de fichiers

97