University thesis:
Dissertation, Carl von Ossietzky Universität Oldenburg, 2017
Footnote:
Description:
Funktionalitäten von sicherheitskritischen Systemen müssen exakt nach deren Spezifikation arbeiten. Ein wichtiger Aspekt solcher Systeme ist, dass die Berechnungen rechtzeitig erfolgen müssen. In dieser Dissertation wird eine zustandsbasierte Timing-Analyse vorgestellt. Um das Problem der Skalierbarkeit zu adressieren, wird der Zustandsraum iterativ berechnet und an den Schnittstellen abhängiger Ressourcen spezielle Abstraktionsmethoden eingesetzt. Die Timing Analyse wird mit einer Impact Analyse erweitert, mit der Re-Verifikationen von zeitlichen Eigenschaften verringert werden. Da Verifikationsaufgaben zeitaufwendig sind, ist das Wiederverwenden von vorherigen Analyseergebnissen erstrebenswert. Eine Methodik wird ausgearbeitet, die die vorgestellten Techniken integriert. Das Ändern eines Teilsystems während der Entwicklungsphase führt zu einer Integrationsprüfung und der Re-Verifikation der internen Struktur. <dt.>
Functionalities of safety-critical systems have to work exactly as specified. A major aspect of such systems is the timeliness of computations. In this thesis a state-based approach for the analysis of timing constraints is introduced. To alleviate the problem of state space explosion, the state space is constructed iteratively, and abstraction operations are applied on the interfaces of dependent resources. On top of this timing analysis an impact analysis approach is introduced to minimize re-verification efforts of timing properties. As verification tasks are typically time consuming it is desirable to reuse previous results of analyses. An overall methodology is presented which integrates all introduced techniques. Changing a part of a system during the design stage implicates the integration check of this part into its context, and the re-verification of its internal structure. <engl.>