Libdmc - Libdmc

libdmc
Geliştirici (ler)Alexandre Hamez
İşletim sistemiPosix Sistemler
TürModel kontrolü

Libdmc [1][2] bir kütüphane LIP6'da tasarlandı [3] laboratuar. Amacı var olanların dağıtımını kolaylaştırmaktır. model dama. Ayrıca, performanstan ödün vermeden en genel arayüzleri sağlamak için tasarlanmıştır. C ++ dil.

Model kontrolü özellikleri doğrulayarak modellenmiş bir sistem davranışının doğru olduğunu otomatik olarak kanıtlamanın bir yolunu sunar. Ancak, sözde acı çekiyor durum alanı yoğun bellek kullanımından kaynaklanan patlama sorunu. Bu sorunun üstesinden gelmek için birçok çözüm önerilmiştir (örneğin, karar diyagramları ile sembolik temsiller - BDD ) ancak bu yöntemler hızla kabul edilemez bir zaman tüketimine yol açabilir.

Dağıtılmış model denetimi, ayrılmış bir kümenin toplu kaynaklarını kullanarak hem bellek hem de zaman tüketiminin üstesinden gelmenin bir yoludur. Bununla birlikte, bir model denetleyicisinin tamamını yeniden yazmak zor bir iştir, bu nedenle libdmc'nin yaklaşımı, bir model denetleyicisi oluşturmak için bir çerçeve vermektir.

Referanslar

  1. ^ Hamez, Alexandre; Kordon, Fabrice; Thierry-Mieg, Yann (2007). "IibDMC: Verimli Dağıtılmış Model Denetimi Çalıştırmak İçin Bir Kitaplık". 2007 IEEE Uluslararası Paralel ve Dağıtık İşleme Sempozyumu: 1–8. doi:10.1109 / IPDPS.2007.370647. ISBN  978-1-4244-0909-9.
  2. ^ Hamez, Alexandre; Kordon, Fabrice; Thierry-Mieg, Yann; Legond-Aubry, Fabrice (2007). "dmcG: GreatSPN'ye Dayalı Dağıtılmış Sembolik Model Denetleyicisi". Bilgisayar Bilimlerinde Ders Notları. 4546: 495–504. doi:10.1007/978-3-540-73094-1_29. ISBN  978-3-540-73093-4.
  3. ^ Accueil LIP6