Libdmc: Difference between revisions
KolbertBot (talk | contribs) m Bot: HTTP→HTTPS |
|||
| Line 9: | Line 9: | ||
}} |
}} |
||
'''Libdmc''' <ref> |
'''Libdmc''' <ref>{{cite journal|doi=10.1109/IPDPS.2007.370647 | title=IibDMC: a Library to Operate Efficient Distributed Model Checking | year=2007 | journal=2007 IEEE International Parallel and Distributed Processing Symposium | last1 = Hamez | first1 = Alexandre | last2 = Kordon | first2 = Fabrice | last3 = Thierry-Mieg | first3 = Yann}}</ref><ref>{{cite journal|doi=10.1007/978-3-540-73094-1_29 | title=dmcG: A Distributed Symbolic Model Checker Based on GreatSPN | journal=Lecture Notes in Computer Science | pages=495–504 | last1 = Hamez | first1 = Alexandre | last2 = Kordon | first2 = Fabrice | last3 = Thierry-Mieg | first3 = Yann | last4 = Legond-Aubry | first4 = Fabrice}}</ref> is a [[Library (computing)|library]] designed at the LIP6 <ref>[http://www.lip6.fr Accueil LIP6<!-- Bot generated title -->]</ref> laboratory. Its goal is to ease the distribution of existing [[Model checking|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 [[Binary decision diagram|BDD]]) but these methods can rapidly lead to an unacceptable time consumption. |
[[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 [[Binary decision diagram|BDD]]) but these methods can rapidly lead to an unacceptable time consumption. |
||
Revision as of 13:26, 3 September 2017
| Developer(s) | Alexandre Hamez |
|---|---|
| Operating system | Posix Systems |
| Type | Model checking |
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
- ^ 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. doi:10.1109/IPDPS.2007.370647.
- ^ Hamez, Alexandre; Kordon, Fabrice; Thierry-Mieg, Yann; Legond-Aubry, Fabrice. "dmcG: A Distributed Symbolic Model Checker Based on GreatSPN". Lecture Notes in Computer Science: 495–504. doi:10.1007/978-3-540-73094-1_29.
- ^ Accueil LIP6
  | This bioinformatics-related article is a stub. You can help Wikipedia by expanding it. |
 | This Unix-related article is a stub. You can help Wikipedia by expanding it. |