Glesner, SabineHerber, Paula2015-11-202010-04-292010-04-292010-04-29urn:nbn:de:kobv:83-opus-26364https://depositonce.tu-berlin.de/handle/11303/2746http://dx.doi.org/10.14279/depositonce-2449Eingebettete Systeme sind in der heutigen Welt allgegenwärtig. Sie werden zunehmend auch in Bereichen eingesetzt, in denen ein Fehler zu hohen finanziellen Verlusten oder sogar zu Verletzungen und Todesfällen führen kann, zum Beispiel im Automobilbereich. Als Folge davon wird es immer wichtiger, die Korrektheit eingebetteter Systeme mit systematischen und umfassenden Verifikationstechniken sicher zu stellen. Eine besondere Herausforderung ist dabei, dass in eingebetteten Systemen Hardware- und Software-Anteile eng miteinander verflochten sind. Um solche heterogenen Systeme zu modellieren und zu simulieren wird häufig die Systembeschreibungssprache SystemC eingea setzt. Die Verifikationstechniken, die für SystemC eingesetzt werden, sind jedoch uberwiegend ad hoc und unsystematisch. Die Verifikation ist daher entweder sehr teuer oder die Ergebnisse sind nicht zuverlässig. In dieser Arbeit stellen wir einen Ansatz zur Lösung dieses Problems vor. Wir präsentieren einen systematischen, umfassenden und formal fundierten Qualitätssicherungsprozess, der die HW/SW Co-Verifikation durchgängig über den gesamten Entwurfsprozess ermöglicht. Die ubergeordnete Idee ist, eine Kombination von Model Checking und Konformitätstesten anzuwenden. Model Checking verwenden wir um zu zeigen, dass ein abstrakter Entwurf eine gegebene Anforderungsspezifikation erfüllt. Anschließend erzeugen wir Konformitätstests um zu prüfen, ob ein verfeinerter Entwurf konform zu diesem abstrakten Entwurf ist. Mit diesem Ansatz erhalten wir Garantien über bestimmte Eigenschaften des abstrakten Entwurfs und stellen gleichzeitig die Konsistenz verfeinerter Entwürfe über den Entwurfsablauf hinweg sicher. Das Ergebnis ist ein Qualitätssicherungsprozess, der den Entwicklungsprozess von der abstrakten Spezifikation bis zur finalen Implementierung unterstützt. Um eine formale Basis für unseren Ansatz zu etablieren, definieren wir eine formale Semantik für SystemC. Zu diesem Zweck bilden wir die informell definierte Semantik von SystemC auf die formal wohl-definierte Semantik von Uppaal Timed Automata ab. Basierend auf dieser Abbildung können wir einen gegebenen SystemC Entwurf automatisch in ein semantisch äquivalentes Uppaal Modell transformieren. Dies ermöglicht auch die Anwendung des Uppaal Model Checkers. Damit können wir wichtige Eigenschaften, zum Beispiel Lebendigkeit, Sicherheit oder die Einhaltung von Zeitschranken, vollautomatisch verifizieren. Neben dem Model Checking bildet die von uns definierte formale Semantik für SystemC auch eine Basis für Konformitätstests. Wir stellen einen Algorithmus vor, der aus einem abstrakten Modell alle möglichen (zeitbehafteten) Ausgaben berechnet und aus diesen automatisch SystemC Test Benches erzeugt. Diese können einen beliebigen verfeinerten Entwurf ausführen und automatisch prüfen, ob die Ausgaben dieses Entwurfs in der Spezifikation erlaubt sind oder nicht, also ob der verfeinerte Entwurf konform zum abstrakten Enwturf ist. Mit der Kombination aus Model Checking und Konformitätstesten erhalten wir ein Framework für die automatisierte HW/SW Co-Verifikation von SystemC Entwürfen mit Hilfe von Timed Automata (VeriSTA). Das Framework ist voll-automatisch anwendbar und unterstützt den gesamten HW/SW Co-Design Prozess. Wir haben das VeriSTA Framework vollständig umgesetzt und demonstrieren seine Leistungsfähigkeit mit experimentellen Ergebnissen.Embedded systems are usually composed of deeply integrated hardware and software components. They are often used in domains where a failure results in high financial losses or even in serious injury or death. As a consequence, it is indispensable to ensure the correctness of the digital components that control these systems with systematic and comprehensive verification techniques. To model and simulate complex HW/SW systems, the system level design language SystemC is widely used. However, the co-verification techniques used for SystemC are mostly ad-hoc and non-systematic. With that, it is either very expensive to verify a given design, or the results are not reliable. In this thesis, we present an approach to overcome this problem by a systematic, comprehensive, and formally founded quality assurance process, which allows automated co-verification of digital HW/SW systems that are modeled in SystemC. The main idea is to apply model checking to verify that an abstract design meets a requirements specification and to generate conformance tests to check whether refined designs conform to this abstract design. With that, we obtain guarantees about the abstract design, which serves as a specification, and we can ensure the consistency of each refined design to that. The result is a HW/SW co-verification flow that supports the HW/SW co-development process continuously from abstract design down to the final implementation. To establish a formal basis for our HW/SW co-verification approach, we define a formal semantics for SystemC. To this end, we present a mapping from SystemC to Uppaal timed automata, which have a formally well-defined semantics. Using this mapping, we can automatically transform a given SystemC design into a semantically equivalent Uppaal model. Furthermore, the resulting Uppaal model allows the application of the Uppaal model checker. With that, we can verify important properties of a SystemC design fully automatically, for example, liveness, safety, or the compliance with timing constraints. These properties are guaranteed for all possible input scenarios. In addition to the formal semantics that allows model checking, we present a novel test algorithm for SystemC. The algorithm uses the Uppaal model of a given high-level SystemC design to generate conformance tests for lower abstraction levels. Existing algorithms for the generation of conformance tests from timed automata models either support only deterministic subclasses of timed automata or compute expected results online during the test execution. The first is inacceptable because SystemC designs are inherently nondeterministic. The latter makes it impossible to reuse the conformance tests in multiple refinement steps. The algorithm presented in this thesis generates conformance tests offline and it can cope with non-deterministic systems. The result is a set of SystemC test benches that can be used to check automatically whether a refined design conforms to a given abstract design. Together with our model checking approach for abstract SystemC designs, we obtain a framework for the automated HW/SW co-Verification of SystemC designs using Timed Automata (VeriSTA). The framework is fully automatically applicable and continuously supports the whole HW/SW co-design process. We implemented the complete VeriSTA framework and demonstrate its performance and its error detecting capability with experimental results.en004 Datenverarbeitung; InformatikEingebettete SystemeHW/SW Co-VerifikationQualitätssicherungSystemCTimed AutomataEmbedded SystemsHW/SW Co-VerificationQuality AssuranceSystemCTimed AutomataDoctoral Thesis