A Synchronous Approach to Threaded Program Verification

Kenneth Johnson 1 Loïc Besnard 1 Thierry Gautier 1 Jean-Pierre Talpin 1
1 ESPRESSO - Synchronous programming for the trusted component-based engineering of embedded systems and mission-critical systems
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : 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.
Type de document :
Rapport
[Research Report] RR-7320, INRIA. 2010
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00492694
Contributeur : Kenneth Johnson <>
Soumis le : lundi 28 juin 2010 - 10:00:26
Dernière modification le : vendredi 16 novembre 2018 - 01:22:54
Document(s) archivé(s) le : jeudi 30 septembre 2010 - 17:41:11

Fichier

RR-7320.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00492694, version 2

Citation

Kenneth Johnson, Loïc Besnard, Thierry Gautier, Jean-Pierre Talpin. A Synchronous Approach to Threaded Program Verification. [Research Report] RR-7320, INRIA. 2010. 〈inria-00492694v2〉

Partager

Métriques

Consultations de la notice

477

Téléchargements de fichiers

237