Formal Verification of Fault-Tolerant Safra's Algorithm - Artifact

Description

The project files for the MSc Thesis: "Formal Verification of Fault-Tolerant Safra’s Algorithm". For this thesis, we create our formal specifications in the mCRL2 language, and then use the mCRL2 toolset to make models and carry out model checking.  We create models based on the two algorithms set forward in "Fault-Tolerant Termination Detection with Safra’s Algorithm" (hereafter [1], see related works DOI 10.1007/978-3-030-91014-3_5). We provide further details in the actual thesis. (Link may be added here in the future.) The files contain: - The "PropertyFiles" folder, containing the different formulas for each of the properties we model check. (Note that not all properties hold for each model -> Check Table 6.1 in the thesis.) - A series of python scripts (*.py) which we used to generate our different files. - A series of folders, each containing our specification (.mcrl2) as well as the .mcrl2proj file & properties folder to open the files in the mCRL2 UI.  -- Most folders additionally contain a series of .lps files, a series of models (.lts files) and a series of .pbes files which we use to check certain properties. -- The "Tol_Bug_Demonstration" folder demonstrates the bug we detected in the fault-tolerant algorithm in [1]. Specifically, the EVI file can be examined using the mCRL2 toolset to see an example execution that breaks the Safety property. -- For the tolerant models (excluding Tol_Bug_Demonstration), we generally fix the number of crashes at N-1. The files marked Cr_* have varying (lower) number of maximum allowed crashes. -- The files marked HS[N]_* in Tol_Safra_n4_crashes are partial models, obtained with mCRL2's highway search technique. -- The files marked INFI_HS[N]_* are the models with large M & S values, and have similarly been generated with Highway search, with a maximum of 10 million states being generated per model (before reduction with ltsconvert). Using the .py files, you can re-create the "*_bisim.lts" files, the "*.pbes" files and check the .pbes files. (See "Steps to reproduce" below.) Note: While this artifact contains MOST of the files, we have deleted some of the larger files, specifically some of the larger PSafety*.pbes files. These can be reproduced either by hand, or with the .py files, as detailed below (and in the thesis in more detail).

Steps to reproduce

We use the mCRL2 toolset to create these specifications and models, specifically version 202507.0. We created these files on Windows 11, and recommend at least 32 GB for the larger files/instances. To create the .lps files, we adjusted the matching specifications in each folder to adjust S and M, and then used the mcrl2lps tool with lineariser = regular2. To create the .lts files, we used the lps2lts tool, with the cached option enabled, using 8 threads, and with the no-info option enabled. To create the *_bisim.lts files, we used the ltsconvert tool, with the options -no-reach and -no-state, and specifically the -equivalence=bisim option. (See also the ConvertLts.py script.) To create the *.pbes files, we used the lts2pbes tool, with the option –preprocess-modal-operators enabled. (Note that we generally did *not* add the counter-example information!) (See also the CreatePbes.py script.) To check the *.pbes files, we used the pbessolve tool, with (up to) 8 threads. (See CheckPbes.py) Note: to use the python scripts, decompress the zips for the files you wish to use, and lay out the folder as follows: ~ - PropertyFiles - Safra_n*_Sensi(_Reduced) - - *.lts / *_bisim.lts / *.pbes - Tol_Safra_n*_Crashes(_Reduced) - - *.lts / *_bisim.lts / *.pbes - *.py

Institutions

• Vrije Universiteit Amsterdam

  Noord-Holland, Amsterdam
• Universiteit van Amsterdam

  Noord-Holland, Amsterdam

Categories

Related Links

Licence