TAPAAL Model Denetleyicisi - TAPAAL Model Checker

TAPAAL
Geliştirici (ler)Aalborg Üniversitesi
İlk sürüm2008 (2008)
Kararlı sürüm
3.6.1 / 18 Mart 2020; 8 ay önce (2020-03-18)
YazılmışC ++ ve GUI içinde Java
İşletim sistemiLinux
Mac OS X
Microsoft Windows
Uyguningilizce
TürModel kontrolü
LisansAçık kaynak
İnternet sitesihttp://www.tapaal.net

TAPAAL modelleme için bir araçtır, simülasyon ve doğrulama nın-nin Zamanlı-Arc Petri ağları Bilgisayar Bilimleri Bölümü'nde geliştirildi Aalborg Üniversitesi Danimarka'da ve Linux, Windows ve Mac OS X platformları için mevcuttur.[1]

Timed-Arc Petri Net (TAPN), klasik Petri ağı model (yaygın olarak kullanılan dağıtılmış hesaplamaların grafik modeli Carl Adam Petri 1962'deki tezinde). TAPN'de dikkate alınan zaman uzantısı, ağdaki belirteçlerle ilişkilendirilen (her simgenin kendi yaşı vardır) gerçek zamanın açık bir şekilde işlenmesine izin verir ve yerlerden geçişlere yaylar, belirteçlerin yaşını kısıtlayan zaman aralıklarıyla etiketlenir ilgili geçişi ateşlemek için kullanılabilir. TAPAAL aracında, bu modelin, taşıma yaylarına sahip yaş değişmezleri (örneğin daha önce kabul edilen okuma yaylarından daha anlamlı olan) ve inhibitör yayları ile bir başka uzantısı uygulanmaktadır.

TAPAAL aracı, TAPN modellerini çizmek için bir grafik düzenleyici, tasarlanmış ağlarla deney yapmak için bir simülatör ve bir alt kümede formüle edilen mantıksal sorguları otomatik olarak yanıtlayan bir doğrulama ortamı sunar. CTL mantık (esasen EF, EG, AF, AG formülleri iç içe geçmeden). Ayrıca, kullanıcının belirli bir ağın belirli bir k sayısı için k-sınırlı olup olmadığını kontrol etmesine izin verir. TAPAAL, TAPAAL ile birlikte dağıtılan kendi doğrulama motorlarıyla donatılmıştır (biri sürekli[2] ve biri ayrık zaman için[3] ). Kullanıcı isteğe bağlı olarak TAPAAL modellerini otomatik olarak UPPAAL ve güvenmek UPPAAL doğrulama motoru.

TAPAAL 2.2.1 ekran görüntüsü

Dış bağlantılar

Referanslar

  1. ^ Alexandre David; Lasse Jacobsen; Morten Jacobsen; Kenneth Yrke Jørgensen; Mikael H. Møller; Jiří Srba (2012). "TAPAAL 2.0: Zamanlanmış Ark Petri Ağları için Entegre Geliştirme Ortamı". TACAS. LNCS. 7214: 492–497. doi:10.1007/978-3-642-28756-5_36. ISBN  978-3-642-28755-8.
  2. ^ Alexandre David; Lasse Jacobsen; Morten Jacobsen; Jiří Srba (2012). "Sınırlı Zamanlı Yaylı Petri Ağları için İleri Erişilebilirlik Algoritması". SSV. EPTCS. 102: 141–155. arXiv:1211.6194. doi:10.4204 / EPTCS.102.12.
  3. ^ M. AndersenH.G. LarsenJ. SrbaM.G. SørensenJ.H. Taankvist (2012). "Kapalı Zamanlı Ark Petri Ağlarında Canlılık Özelliklerinin Doğrulanması". MEMİKLER. LNCS: 69–81.