Master Thesis Online
N/A
Leruth, Guillaume 
Promotor(s) :
Fontaine, Pascal
Date of defense : 5-Sep-2024/6-Sep-2024 • Permalink : http://hdl.handle.net/2268.2/20979
All files (archive ZIP)
main.pdfDetails
| Title : | N/A |
| Translated title : | [fr] Spécification et vérification de popriétés de sûreté d'algorithmes parallèles à l'aide de la Toolbox TLA+ |
| Author : | Leruth, Guillaume
|
| Date of defense : | 5-Sep-2024/6-Sep-2024 |
| Advisor(s) : | Fontaine, Pascal
|
| Committee's member(s) : | Boigelot, Bernard
Debruyne, Christophe
|
| Language : | English |
| Number of pages : | 65 |
| Keywords : | [en] TLA+ [en] Parallel Programming [en] Formal Methods [en] Concurrent Programming [en] Software Verification [en] Parallel Algorithms [en] TLAPS [en] Computer-Assisted Proof |
| Discipline(s) : | Engineering, computing & technology > Computer science |
| Institution(s) : | Université de Liège, Liège, Belgique |
| Degree: | Master : ingénieur civil en informatique, à finalité spécialisée en "computer systems security" |
| Faculty: | Master thesis of the Faculté des Sciences appliquées |
Abstract
[en] The goal of this Master’s thesis is to specify and verify safety properties of a few classical algorithms taken from the Parallel Programming lectures taught by Prof. Pascal Fontaine by using the TLA+ tool suite. The first chapter of this work lays out the minimal concepts of concurrent programming required to motivate the distinctive significance of software verification in the world of parallel and distributed algorithms. The second one presents all the tools of the TLA+ environment used in the following chapters. A rough methodology is established to turn pseudo-code descriptions of algorithms into unambiguous TLA+ specifications and to consequently identify and express safety properties of interest before checking and proving them.
The next chapters consist in applying the previously described tools and methods to Barz’s algorithm and the Readers-writers. The resulting TLA+ specifications, adjoining definitions and properties as well as TLAPS proofs constitute the original contribution of this Master’s thesis..
File(s)
Document(s)
Cite this master thesis
The University of Liège does not guarantee the scientific quality of these students' works or the accuracy of all the information they contain.