Libdmc

From Wikipedia, the free encyclopedia

Page Module:Infobox/styles.css has no content.

libdmc
[[Programmer|DeveloperTemplate:Pluralize from text]]Alexandre Hamez
Template:Infobox software/simple
EnginePage Template:Plainlist/styles.css has no content.Template:EditAtWikidata
Operating systemPosix Systems
TypeModel checking
WebsiteScript error: No such module "WikidataIB".
RepositoryPage Template:Plainlist/styles.css has no content.

Script error: No such module "Check for conflicting parameters".

Libdmc [1][2] is a library designed at the LIP6 [3] laboratory. Its goal is to ease the distribution of existing model checkers. It has also been designed to provide the most generic interfaces, without sacrificing performance, thanks to the C++ language.

Model checking offers a way to automatically prove that a modeled system behavior is correct by verifying properties. However, it suffers from the so-called state space explosion problem, caused by an intensive use of memory. Many solutions have been proposed to overcome this problem (e.g. symbolic representations with decisions diagrams - like BDD) but these methods can rapidly lead to an unacceptable time consumption.

Distributed model checking is a way to overcome both memory and time consumptions by using aggregated resources of a dedicated cluster. However, re-writing an entire model checker is a difficult task, so the approach of libdmc is to give a framework in order to construct a model checker.

References

Page Template:Reflist/styles.css has no content.

  1. ^ Page Module:Citation/CS1/styles.css has no content.Hamez, Alexandre; Kordon, Fabrice; Thierry-Mieg, Yann (2007). "IibDMC: A Library to Operate Efficient Distributed Model Checking". 2007 IEEE International Parallel and Distributed Processing Symposium. pp. 1–8. doi:10.1109/IPDPS.2007.370647. ISBN 978-1-4244-0909-9. S2CID 12586847.
  2. ^ Page Module:Citation/CS1/styles.css has no content.Hamez, Alexandre; Kordon, Fabrice; Thierry-Mieg, Yann; Legond-Aubry, Fabrice (2007). "DMCG: A Distributed Symbolic Model Checker Based on GreatSPN". Petri Nets and Other Models of Concurrency – ICATPN 2007. Lecture Notes in Computer Science. Vol. 4546. pp. 495–504. doi:10.1007/978-3-540-73094-1_29. ISBN 978-3-540-73093-4.
  3. ^ Accueil LIP6


Template:Asbox

Template:Asbox