Uppaal Model Checker - Uppaal Model Checker

UPPAAL
ӘзірлеушілерУпсала университеті
Ольборг университеті
Бастапқы шығарылым1995 (1995)
Тұрақты шығарылым
4.0.14 / 20 мамыр 2014 ж; 6 жыл бұрын (2014-05-20)
Алдын ала қарау
4.1.22 / 28 наурыз, 2019; 19 ай бұрын (2019-03-28)
ЖазылғанC ++ және GUI жылы Java
Операциялық жүйеLinux
Mac OS X
Microsoft Windows
Қол жетімдіАғылшын Дат жапон Қытай Литва
ТүріМодельді тексеру
ЛицензияКоммерциялық лицензиялар
Академиялық лицензиялар
Веб-сайтhttp://www.uppaal.org/ http://www.uppaal.com/

UPPAAL интегралды болып табылады құрал қоршаған орта үшін модельдеу, тексеру және тексеру шынайы уақыт желілері ретінде модельделген жүйелер уақытты автоматтар, кеңейтілген деректер түрлері (шектелген бүтін сандар, массивтер және т.б.).

Ол 1995 жылы шыққаннан бері кем дегенде 17 жағдайлық зерттеулерде қолданылды, оның ішінде Lego Mindstorms, үшін Philips аудио протокол және беріліс қорабының контроллерлерінде Mecel.[1]

Құрал нақты уақыт жүйелерін жобалау және талдау тобы арасында бірлесіп жасалған Упсала университеті, Швеция және информатика саласындағы негізгі зерттеулер Ольборг университеті, Дания.

Келесі кеңейтімдер бар:

  • Кора Қол жетімділікті оңтайлы талдау үшін.
  • Трон ON-line режиміндегі нақты уақыт жүйелерін тексеруге арналған (қара жәшіктің сәйкестігін сынау).
  • Мұқабасы COVERerage-оңтайлы желіден тыс тест құру үшін.
  • Тига TImed GAmes негізіндегі контроллер синтезі үшін.
  • Порт ішінара тапсырыс азайту әдістерін қолдана отырып, компоненттерге негізделген уақытша жүйелер үшін.
  • Pro қол жетімділікті PRObabilistic талдау үшін. (Тоқтатылды)
  • SMC Статистикалық модельді тексеруге арналған.

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

  1. ^ «Тақырыптық зерттеулер».

Сыртқы сілтемелер