Scalable compatibility for embedded real-time components via language progressive timed automata

Mehr zum Buch

Die korrekte Komposition individuell entwickelter Komponenten von eingebetteten Realzeitsystemen stellt eine Herausforderung dar, da neben funktionalen auch nicht funktionale Eigenschaften berücksichtigt werden müssen. Ein Beispiel ist die Kompatibilität von Realzeiteigenschaften, die entscheidend für eingebettete Systeme ist. Aktuell erfolgt die Prüfung dieser Kompatibilität durch aufwändige Integrations- und Konfigurationstests am Ende des Entwicklungsprozesses, was im schlimmsten Fall zu Fehlschlägen führt. Um dem entgegenzuwirken, wurden formale Verfahren entwickelt, die eine frühzeitige Analyse von Realzeiteigenschaften ermöglichen, um Inkompatibilitäten in späteren Phasen zu vermeiden. Bestehende Verfahren erfordern jedoch oft Bedingungen, die von realen Systemen schwer zu erfüllen sind, oder sie skalieren nicht für größere Systeme. Der in dieser Arbeit vorgestellte Ansatz basiert auf dem formalen Modell des Timed Automaton und benötigt keine schwer erfüllbaren Bedingungen. Er beinhaltet ein Framework, das eine modulare Analyse ermöglicht, bei der nur kommunizierende Komponenten paarweise überprüft werden müssen. Dadurch wird eine skalierbare Analyse von Realzeiteigenschaften erreicht, die keine Bedingungen erfordert, die nur bedingt von realen Systemen erfüllt werden können.