Systematické testování kritických aplikací reálného času v Javě

Abstrakt

Při tradičním testování softwarových aplikací není možné ovlivnit nedeterministická rozhodnutí různých částí systému, zejména plánování vláken. Test tak může ověřit jen jedno možné proložení vláken.

Java Path Finder (JPF) umožňuje systematicky procházet různá možná proložení, ale nedokáže testovat aplikace reálného času. V této práci navrhujeme a implementujeme algorithmus rozšíření JPF, které kritické aplikace reálného času v Javě testovat umí.

Naši implementaci testujeme na modelových aplikacích, včetně otevřeného autopilota PapaBench, který jsme pro tyto účely přepsali do jazyka Java s rozšířením SCJ a RTSJ.

Klíčová slova

• systematické testování
• model checking
• systémy reálného času
• kritické aplikace