Publikace na Matematicko-fyzikální fakulta |
2010
Abstrakt
Poruchy systémů reálného času mohou mít katastrofální následky, v krajním případě i ztrátu lidských životů. Verifikace software pro tyto systémy tak představuje důležitý úkol pro verifikační komunitu.
Bohužel, software pro tyto systémy typicky není veřejně dostupný, což prakticky znemožňuje vývoj a porovnávání verifikačních nástrojů. V této práci představujeme klíčové problémy pro verifikaci systémů reálného času v Javě a zejména volně dostupné modelové úlohy pro Javu i C, které umožní testování verifikačních nástrojů.