FDR (бағдарламалық жасақтама) - FDR (software)

FDR FDR2 FDR3 FDR4
FDR4 CSP нақтылауын тексеруші бағдарлама logo.png
ӘзірлеушілерОксфорд университеті, Cocotec
Тұрақты шығарылым
4.2.4 / 19 ақпан 2019; 21 ай бұрын (2019-02-19)
Операциялық жүйе
  • GNU / Linux
  • MacOS
  • Windows
ТүріCSP нақтылау тексерушісі
Лицензияменшікті бағдарламалық жасақтама
Веб-сайтhttps://cocotec.io/fdr/

FDR (Сәтсіздіктер-айырмашылықтарды нақтылау) және кейіннен FDR2, FDR3 және FDR4 болып табылады нақтылау тексеру бағдарламалық құралдар, тексеруге арналған ресми модельдер ішінде көрсетілген Бірізді процестерді байланыстыру (CSP). Құралдарды бастапқыда Formal Systems (Europe) Ltd.[1] Билл Розко туралы Оксфорд университетінің компьютерлік ғылымдар бөлімі құралы қолданатын көптеген алгоритмдерді ойлап тапты Майкл Голдсмит[2] жүзеге асыруға ықпал етті.[3] FDR2 әзірлеген Оксфорд университетінің компьютерлік ғылымдар бөлімі академиялық және басқа коммерциялық емес мақсаттар үшін ол еркін қол жетімді болатын жерден.[4]

FDR жиі а ретінде сипатталады модель тексерушісі, бірақ техникалық жағынан а нақтылау CSP процесінің екі өрнегін түрлендіретін тексергіш Белгіленген өтпелі жүйелер (LTS), содан кейін процестердің біреуі екіншісінің нақтыланған белгілі бір шегінде болатындығын анықтайды семантикалық модель (іздер, сәтсіздіктер, сәтсіздіктер / дивергенция және кейбір басқа баламалар).[5] FDR2 әртүрлі қолданылады мемлекет-кеңістік нақтылықты тексеру кезінде зерттелуге тиісті күй-кеңістіктің көлемін азайту мақсатында LTS процестеріне қысу алгоритмдері.

FDR2 1995 жылы FDR1 деп аталатын бұрынғы құралды ауыстыра отырып, көптеген шығарылымдарды бастан өткерді. Оның орнына FDR3, параллель орындалуы мен интегралданған тип тексерушісін қосатын, толығымен қайта жазылған нұсқасы болды. FDR3 ​​шығарады Оксфорд университеті, ол сонымен қатар FDR2 шығарды 2008-12 жж.[6] ProBE CSP аниматоры FDR3-ке біріктірілген. Енді оның орнына FDR4 келді. FDR4 Cocotec-тен қол жетімді.[7]

Әдебиеттер тізімі

  1. ^ Formal Systems (Еуропа) Ltd..
  2. ^ Профессор Майкл Голдсмит (сонымен қатар қазір Оксфорд университетінің).
  3. ^ Филиппа Бродфут пен Билл Розко. FDR және оның қосымшалары туралы оқу құралы. Клаус Гавелундта, Джон Пеникс, Виллем Виссер (редакторлар), SPIN моделін тексеру және бағдарламалық жасақтаманы тексеру, Шпрингер-Верлаг, Информатика пәнінен дәрістер, 1885 том, 322 бет, 2000 ж.
  4. ^ Бағдарламалық жасақтама: FDR2, алуға болатын коммерциялық лицензияларымен Formal Systems (Еуропа) Ltd..
  5. ^ А.В. Розко (1994). «CSP моделін тексеру». Жылы Классикалық ақыл: құрметіне арналған эсселер C.A.R. Хоар. Prentice Hall. Журналға сілтеме жасау қажет | журнал = (Көмектесіңдер)
  6. ^ FDR3-ке кіріспе
  7. ^ Бағдарламалық жасақтама: FDR4, коммерциялық лицензиялар жүктелгеннен кейін және бірінші басталғаннан кейін алуға болады