inria-00492694, version 1

A Synchronous Approach to Threaded Program Verification

Kenneth Johnson () ^a, 1, Loïc Besnard () ^b, 1, Thierry Gautier () ^a, 1, Jean-Pierre Talpin () ^a, 1

N° RR-7320 (2010)

• a –  INRIA
• b –  CNRS
• 1:  ESPRESSO (INRIA - IRISA)
• http://www.inria.fr/equipes/espresso
  CNRS : UMR6074 – INRIA – Institut National des Sciences Appliquées (INSA) - Rennes – Université de Rennes 1 Campus de Beaulieu 35042 Rennes cedex France

Available versions :  v1 (2010-06-16) v2 (2010-06-28)

Bibliographic reference

• Type of document: Research reports
• Domain: Computer Science/Embedded Systems
• Title: A Synchronous Approach to Threaded Program Verification
• 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.
• Abstract in french: Les systèmes actuels s'appuient sur une organisation complexe de processus de calcul partageant l'accès aux processeurs et aux ressources. La programmation au moyen de "threads" fournit une méthode dans laquelle des processus légers se voient attribuer des tâches spécifiques qui peuvent être menées soit indépendamment, soit en coopération avec d'autres threads. L'utilisation correcte et efficace de ressources partagées entre les threads repose sur des mécanismes de synchronisation tels que les sémaphores, les sections critiques ou les événements. Notre travail décrit une méthode semi-automatique de traduction de logiciels organisés en threads vers le langage synchrone Signal dans le but de vérifier la correction des synchronisations des programmes sources.
• Full text language: English
• Report type: Research Report
• Publication date: 2010-06-16
• Keywords: Signal – polychrony – threads – model generation – model checking
• Internal note: RR-7320
• ANR Project:

  Project Id	ANR-06-SETI-007
  Year	2006
  Project acronyme	FoToVP
  Project title	Formal Tools for Virtual Prototyping of embedded systems
  Intitule	Programme "Sécurité et Informatique
  Acronyme	SETI

Attached file list to this document: 

• inria-00492694, version 1
• http://hal.inria.fr/inria-00492694
• oai:hal.inria.fr:inria-00492694
• From: Kenneth Johnson <>
• Submitted on: Wednesday, 16 June 2010 16:35:40
• Updated on: Thursday, 17 June 2010 16:03:10