{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T02:30:26Z","timestamp":1747881026992},"reference-count":41,"publisher":"Oxford University Press (OUP)","issue":"4","license":[{"start":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T00:00:00Z","timestamp":1641513600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,4,15]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we present sasa, an open-source SimulAtor of Self-stabilizing Algorithms. Self-stabilization defines the ability of a distributed algorithm to recover after transient failures. sasa is implemented as a faithful representation of the atomic-state model (also called the locally shared memory model with composite atomicity). This model is the most commonly used one in the self-stabilizing area to prove both the correct operation of self-stabilizing algorithms and complexity bounds on them. sasa encompasses all features necessary to debug, test and analyze self-stabilizing algorithms. All these facilities are programmable to enable users to accommodate to their particular needs. For example, asynchrony is modeled by programmable stochastic daemons playing the role of input sequence generators. Properties of algorithms can be checked using formal test oracles. The sasa distribution also provides several facilities to easily achieve (batch-mode) simulation campaigns. We show that the lightweight design of sasa allows to efficiently perform huge such campaigns. Following a modular approach, we have aimed at relying as much as possible the design of sasa on existing tools, including ocaml, dot and several tools developed in the Synchrone Group of the VERIMAG laboratory.<\/jats:p>","DOI":"10.1093\/comjnl\/bxab196","type":"journal-article","created":{"date-parts":[[2021,11,16]],"date-time":"2021-11-16T20:11:25Z","timestamp":1637093485000},"page":"796-814","source":"Crossref","is-referenced-by-count":3,"title":["<scp>sasa<\/scp>: a SimulAtor of Self-stabilizing Algorithms"],"prefix":"10.1093","volume":"66","author":[{"given":"Karine","family":"Altisen","sequence":"first","affiliation":[{"name":"Univ. Grenoble Alpes , CNRS, Grenoble INP, VERIMAG, 38000 Grenoble, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Devismes","sequence":"additional","affiliation":[{"name":"Univ. Picardie Jules Verne , MIS, 80039 Amiens Cedex 1, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erwan","family":"Jahier","sequence":"additional","affiliation":[{"name":"Univ. Grenoble Alpes , CNRS, Grenoble INP, VERIMAG, 38000 Grenoble, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2022,1,7]]},"reference":[{"key":"2023041809382592500_","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1145\/361179.361202","article-title":"Self-stabilizing systems in spite of distributed control","volume":"17","author":"Dijkstra","year":"1974","journal-title":"Commun. ACM"},{"key":"2023041809382592500_","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/6156.001.0001","volume-title":"Self-Stabilization","author":"Dolev","year":"2000"},{"key":"2023041809382592500_","article-title":"Introduction to Distributed Self-Stabilizing Algorithms","volume-title":"Synthesis Lectures on Distributed Computing Theory","author":"Altisen","year":"2019"},{"key":"2023041809382592500_","doi-asserted-by":"crossref","first-page":"1203","DOI":"10.1002\/1097-024X(200009)30:11<1203::AID-SPE338>3.0.CO;2-N","article-title":"An open graph visualization system and its applications to software engineering","volume":"30","author":"Gansner","year":"2000","journal-title":"Softw. Pract. Exper."},{"key":"2023041809382592500_","volume-title":"The synchrone reactive toolbox","author":"Jahier"},{"key":"2023041809382592500_","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/0020-0190(94)90103-1","article-title":"Self-stabilizing depth-first search","volume":"49","author":"Collin","year":"1994","journal-title":"Inf. Process. Lett."},{"key":"2023041809382592500_","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-642-11322-2_19","article-title":"Probabilistic Self-Stabilizing Vertex Coloring in Unidirectional Anonymous Networks","volume-title":"Distributed Computing and Networking","author":"Bernard","year":"2010"},{"key":"2023041809382592500_","first-page":"55","article-title":"Self-stabilizing vertex coloration and arbitrary graphs","volume-title":"Proceedings of the 4th International Conference on Principles of Distributed Systems (OPODIS)","author":"Gradinariu","year":"2000"},{"key":"2023041809382592500_","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1142\/S0129626491000161","article-title":"Maintaining digital clocks in step","volume":"1","author":"Arora","year":"1991","journal-title":"Parallel Process. Lett."},{"key":"2023041809382592500_","first-page":"486","article-title":"Asynchronous Unison (Extended Abstract)","volume-title":"Proceedings of the 12th International Conference on Distributed Computing Systems","author":"Couvreur","year":"1992"},{"key":"2023041809382592500_","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/j.jpdc.2017.05.003","article-title":"Evaluating and optimizing stabilizing dining philosophers","volume":"109","author":"Adamek","year":"2017","journal-title":"J. Parallel Distrib. Comput."},{"key":"2023041809382592500_","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-642-33536-5_13","article-title":"Evaluating Practical Tolerance Properties of Stabilizing Programs Through Simulation: The Case of Propagation of Information with Feedback","volume-title":"Stabilization, Safety, and Security of Distributed Systems: 14th International Symposium, SSS 2012, Toronto, Canada, October 1-4, 2012","author":"Adamek","year":"2012"},{"key":"2023041809382592500_","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1109\/IPSN.2007.4379677","article-title":"Worldsens: Development and Prototyping Tools for Application Specific Wireless Sensors Networks","volume-title":"Proceedings of the 6th International Conference on Information Processing in Sensor Networks","author":"Fraboulet","year":"2007"},{"key":"2023041809382592500_","doi-asserted-by":"crossref","DOI":"10.4108\/ICST.SIMUTOOLS2008.3027","article-title":"An Overview of the omnet++ Simulation Environment","volume-title":"Proceedings of the 1st International Conference on Simulation Tools and Techniques for Communications, Networks and Systems & Workshops, Marseille, France, March Simutools \u201808, pp. 60:1\u201360:10. ICST","author":"Varga","year":"2008"},{"key":"2023041809382592500_","volume-title":"Introduction to Network Simulator NS2","author":"Issariyakul","year":"2010"},{"key":"2023041809382592500_","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1016\/j.tcs.2016.02.010","article-title":"Competitive self-stabilizing k-clustering","volume":"626","author":"Datta","year":"2016","journal-title":"Theor. Comput. Sci."},{"key":"2023041809382592500_","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1109\/SIMSYM.1992.227579","article-title":"Simulation of Self-Stabilizing Algorithms in Distributed Systems","volume-title":"Proceedings 25th Annual Simulation Symposium, Orlando, Florida, USA, April 6-9","author":"Flatebo","year":"1992"},{"key":"2023041809382592500_","volume-title":"A simulator for self-stabilizing distributed algorithms","author":"Har-Tal","year":"2000"},{"key":"2023041809382592500_","first-page":"183","article-title":"Derivation of Fault Tolerance Measures of Self-Stabilizing Algorithms by Simulation","volume-title":"Proceedings of the 41st Annual Simulation Symposium, Ottawa, Canada, April 14\u201316","author":"M\u00fcllner","year":"2008"},{"key":"2023041809382592500_","first-page":"1","article-title":"Selfsim: A Discrete-Event Simulator for Distributed Self-Stabilizing Algorithms","author":"Evcimen","year":"2018"},{"key":"2023041809382592500_","volume-title":"Probability and Statistics with Reliability, Queuing and Computer Science Applications","author":"Trivedi","year":"2002"},{"key":"2023041809382592500_","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/978-3-030-50995-8_8","article-title":"sasa: A Simulator of Self-Stabilizing Algorithms","volume-title":"Tests and Proofs: 14th International Conference, TAP 2020, Held as Part of STAF 2020, Bergen, Norway, June 22\u201323, 2020","author":"Altisen","year":"2020"},{"key":"2023041809382592500_","article-title":"SASA: a SimulAtor of Self-stabilizing Algorithms","author":"Jahier"},{"key":"2023041809382592500_","article-title":"SASA artifact: how to reproduce the results","author":"Jahier"},{"key":"2023041809382592500_","article-title":"L\u2019unisson","author":"Boulinier","year":"2007"},{"key":"2023041809382592500_","volume-title":"Verimag tools tutorials: tutorials related to sasa","author":"Jahier"},{"key":"2023041809382592500_","article-title":"The objective caml system, documentation and user\u2019s manual","author":"Leroy"},{"key":"2023041809382592500_","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1145\/1631687.1596591","article-title":"Experience report","volume":"44","author":"Cuoq","year":"2009","journal-title":"SIGPLAN Not."},{"key":"2023041809382592500_","first-page":"1","article-title":"Une biblioth\u00e8que de typage dynamique en OCaml","volume-title":"22e Journ\u00e9es Francophones des Langages Applicatifs (JFLA\u201911)","author":"Signoles","year":"2011"},{"key":"2023041809382592500_","volume-title":"The Lustre V6 Reference Manual","author":"Jahier","year":"2018"},{"key":"2023041809382592500_","article-title":"Programming and verifying critical systems by means of the synchronous data-flow programming language Lustre","volume-title":"ACM-SIGSOFT\u201991 Conference on Software for Critical Systems","author":"Nicolas","year":"1991"},{"key":"2023041809382592500_","first-page":"510","article-title":"The kind 2 model checker","volume-title":"Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17\u201323, 2016, Part II","author":"Champion","year":"2016"},{"key":"2023041809382592500_","first-page":"140","article-title":"Engineering Functional Requirements of Reactive Systems Using Synchronous Languages","volume-title":"International Symposium on Industrial Embedded Systems","author":"Jahier","year":"2013"},{"key":"2023041809382592500_","first-page":"116","article-title":"RDBG: a reactive programs extensible debugger","volume-title":"Proceedings of the 19th International Workshop on Software and Compilers for Embedded Systems, SCOPES 2016, Sankt Goar, Germany, May","author":"Jahier","year":"2016"},{"key":"2023041809382592500_","doi-asserted-by":"crossref","first-page":"290","DOI":"10.5486\/PMD.1959.6.3-4.12","article-title":"On random graphs","volume":"6","author":"Erd\u00f6s","year":"1959","journal-title":"Publ. Math. Debr."},{"key":"2023041809382592500_","volume-title":"Comparing randomized coloring algorithms","author":"Jahier"},{"key":"2023041809382592500_","volume-title":"Statistical analysis of data obtained by simulation campaigns","author":"Jahier"},{"key":"2023041809382592500_","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/S0020-0190(99)00164-7","article-title":"Error-detecting codes and fault-containing self-stabilization","volume":"73","author":"Herman","year":"2000","journal-title":"Inf. Process. Lett."},{"key":"2023041809382592500_","volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","author":"Lamport","year":"2002"},{"key":"2023041809382592500_","article-title":"A framework for certified self-stabilization. Log. Methods Comput. Sci.","volume":"13","author":"Altisen","year":"2017"},{"key":"2023041809382592500_","article-title":"Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions Texts in Theoretical Computer Science","volume-title":"Interactive Theorem Proving and Program Development","author":"Bertot","year":"2004"}],"container-title":["The Computer Journal"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/comjnl\/article-pdf\/66\/4\/796\/49932031\/bxab196.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/comjnl\/article-pdf\/66\/4\/796\/49932031\/bxab196.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,12]],"date-time":"2023-11-12T18:52:46Z","timestamp":1699815166000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/comjnl\/article\/66\/4\/796\/6499477"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,7]]},"references-count":41,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2022,1,7]]},"published-print":{"date-parts":[[2023,4,15]]}},"URL":"https:\/\/doi.org\/10.1093\/comjnl\/bxab196","relation":{},"ISSN":["0010-4620","1460-2067"],"issn-type":[{"value":"0010-4620","type":"print"},{"value":"1460-2067","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2023,4]]},"published":{"date-parts":[[2022,1,7]]}}}