inria-00492694, version 1
A Synchronous Approach to Threaded Program Verification
N° RR-7320 (2010)
Résumé : Modern systems involve a complex organization of computational processes sharing access to both processors and resources. The use of threads in programming provides a method in which lightweight processes may be given specific tasks that can be carried out either independently or in cooperation with other threads. The correct and efficient use of shared resources between threads relies on synchronisation methods, such as semaphores, mutexes, or events. Our work demonstrates a semi-automated method of translating threaded software to the synchronous programming language Signal in order to verify the correctness of thread synchronisations in the source code.
- a – INRIA
- b – CNRS
- 1 :
- CNRS : UMR6074 – INRIA – Institut National des Sciences Appliquées (INSA) - Rennes – Université de Rennes 1
- Domaine : Informatique/Systèmes embarqués
- Mots-clés : Signal – polychrony – threads – model generation – model checking
- Référence interne : RR-7320
- Versions disponibles : v1 (16-06-2010) v2 (28-06-2010)
- inria-00492694, version 1
- http://hal.inria.fr/inria-00492694
- oai:hal.inria.fr:inria-00492694
- Contributeur :
- Soumis le : Mercredi 16 Juin 2010, 16:35:40
- Dernière modification le : Jeudi 17 Juin 2010, 16:03:10
Documents associés
Exporter