libdmc
Libdmc| 개발자 | 알렉산드르 하메즈 |
|---|---|
| 운영 체제 | Posix 시스템 |
| 유형 | 모델 체크 |
Libdmc는 LIP6 연구소에서 설계된 라이브러리입니다.기존 모델 체커의 유통을 완화하는 것이 목표다.또한 C++ 언어 덕분에 퍼포먼스를 희생하지 않고 가장 일반적인 인터페이스를 제공하도록 설계되어 있습니다.
모델 확인을 통해 속성을 검증하여 모델링된 시스템 동작이 올바른지 자동으로 증명할 수 있습니다.그러나 메모리의 대량 사용으로 인해 발생하는 이른바 상태 공간 폭발 문제를 겪고 있습니다.이 문제를 극복하기 위해 많은 해결책이 제안되었지만(예: 의사결정 다이어그램이 있는 상징적 표현(BDD)), 이러한 방법은 빠르게 허용할 수 없는 시간 소비로 이어질 수 있다.
분산 모델 체크는 전용 클러스터의 집계된 리소스를 사용하여 메모리와 시간 소비를 모두 해결하는 방법입니다.그러나 전체 모델 체커를 다시 쓰는 것은 어려운 작업이기 때문에 libdmc의 접근법은 모델 체커를 구성하기 위한 프레임워크를 제공하는 것입니다.
레퍼런스
- ^ 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: 1–8. doi:10.1109/IPDPS.2007.370647. ISBN 978-1-4244-0909-9. S2CID 12586847.
- ^ Hamez, Alexandre; Kordon, Fabrice; Thierry-Mieg, Yann; Legond-Aubry, Fabrice (2007). "dmcG: A Distributed Symbolic Model Checker Based on GreatSPN". Lecture Notes in Computer Science. 4546: 495–504. doi:10.1007/978-3-540-73094-1_29. ISBN 978-3-540-73093-4.
- ^ 액큐일 LIP6
