FDR (yazılım) - FDR (software)

FDR FDR2 FDR3 FDR4
FDR4 CSP iyileştirme kontrol yazılımı logo.png
Geliştirici (ler)Oxford Üniversitesi, Cocotec
Kararlı sürüm
4.2.4 / 19 Şubat 2019; 21 ay önce (2019-02-19)
İşletim sistemi
  • GNU / Linux
  • Mac os işletim sistemi
  • pencereler
TürCSP ayrıntılandırma denetleyicisi
Lisanstescilli yazılım
İnternet sitesihttps://cocotec.io/fdr/

FDR (Hatalar-Sapmalar Ayrıntılandırma) ve ardından FDR2, FDR3 ve FDR4 vardır inceltme kontrol etme yazılım araçları, kontrol etmek için tasarlandı resmi modeller olarak ifade edildi Sıralı süreçleri iletmek (CSP). Araçlar orijinal olarak Formal Systems (Europe) Ltd. tarafından geliştirilmiştir.[1] Bill Roscoe of Bilgisayar Bilimleri Bölümü, Oxford Üniversitesi araç tarafından kullanılan algoritmaların çoğunu tasarladı ve Michael Goldsmith[2] uygulamada etkili oldu.[3] FDR2, Bilgisayar Bilimleri Bölümü, Oxford Üniversitesi akademik ve diğer ticari olmayan kullanım için ücretsiz olarak[4]

FDR genellikle bir model denetleyicisi, ancak teknik olarak bir inceltme checker, iki CSP işlem ifadesini Etiketli Geçiş Sistemleri (LTS'ler) ve ardından süreçlerden birinin belirli bir süre içinde diğerinin iyileştirilmesi olup olmadığını belirler. anlamsal model (izler, başarısızlıklar, başarısızlıklar / sapma ve diğer bazı alternatifler).[5] FDR2, çeşitli durum uzayı bir iyileştirme denetimi sırasında araştırılması gereken durum uzayının boyutunu azaltmak için işlem LTS'lerine sıkıştırma algoritmaları.

FDR2, 1995 yılında FDR1 olarak anılan önceki aracın yerini alarak birçok sürümden geçti. Bunun yerine, paralel yürütme ve entegre bir tür denetleyici dahil, tamamen yeniden yazılmış bir sürüm olan FDR3 geldi. FDR3, Oxford Üniversitesi 2008-12 döneminde de FDR2'yi piyasaya sürdü.[6] ProBE CSP Animator, FDR3'e entegre edilmiştir. Şimdi FDR4 tarafından başarıldı. FDR4, Cocotec'ten temin edilebilir.[7]

Referanslar

  1. ^ Biçimsel Sistemler (Avrupa) Ltd.
  2. ^ Profesör Michael Goldsmith (ayrıca şimdi Oxford Üniversitesi'nde).
  3. ^ Philippa Broadfoot ve Bill Roscoe. FDR ve Uygulamaları Üzerine Eğitim. Klaus Havelund'da, John Penix, Willem Visser (editörler), SPIN model kontrolü ve yazılım doğrulama, Springer-Verlag, Bilgisayar Bilimlerinde Ders Notları, Cilt 1885, sayfa 322, 2000.
  4. ^ Yazılım: FDR2 ticari lisanslar ile Biçimsel Sistemler (Avrupa) Ltd.
  5. ^ A.W. Roscoe (1994). "Model denetimi CSP". İçinde A Classical Mind: onuruna makaleler C.A.R. Hoare. Prentice Hall. Alıntı dergisi gerektirir | günlük = (Yardım)
  6. ^ FDR3'e Giriş
  7. ^ Yazılım: FDR4, indirdikten ve ilk başlatmadan sonra alınabilen ticari lisanslarla