h1

000464374 001__ 464374
000464374 005__ 20250613102210.0
000464374 0247_ $$2URN$$aurn:nbn:de:hbz:82-opus-52966
000464374 0247_ $$2OPUS$$a5296
000464374 0247_ $$2Laufende Nummer$$a34312
000464374 0247_ $$2HBZ$$aHT018578647
000464374 037__ $$aRWTH-CONV-207070
000464374 041__ $$aEnglish
000464374 082__ $$a004
000464374 1001_ $$0P:(DE-82)012894$$aGückel, Dominique$$b0
000464374 245__ $$aSynthesis of state space generators for model checking microcontroller code$$cvorgelegt von Dominique Marcel Gückel$$honline, print
000464374 246_3 $$aSynthese von Zustandsraum-Generatoren für das Model-Checking von Mikrocontroller-Code$$yGerman
000464374 260__ $$aAachen$$bFachgruppe Informatik, RWTH Aachen University$$c2014
000464374 260__ $$c2015
000464374 300__ $$aXI, 181 S. : Ill., graph. Darst.
000464374 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
000464374 3367_ $$02$$2EndNote$$aThesis
000464374 3367_ $$2DRIVER$$adoctoralThesis
000464374 3367_ $$2BibTeX$$aPHDTHESIS
000464374 3367_ $$2DataCite$$aOutput Types/Dissertation
000464374 3367_ $$2ORCID$$aDISSERTATION
000464374 3367_ $$0PUB:(DE-HGF)3$$2PUB:(DE-HGF)$$aBook$$mbook
000464374 4900_ $$aAachener Informatik-Berichte Technical report / Department of Computer Science, RWTH Aachen$$v2014,15
000464374 500__ $$aDruckausgabe: 2014. - Onlineausgabe: 2015. Auch veröffentlicht auf dem Publikationsserver der RWTH Aachen University.
000464374 502__ $$aAachen, Techn. Hochsch., Diss., 2014$$bDiss.$$cAachen, Techn. Hochsch.$$d2014$$gFak01$$o2014-10-15
000464374 5203_ $$aDie Implementierung von Software für eingebettete Systeme erfordert strenge Maßnahmen zur Qualitätssicherung. Der Grund hierfür ist, daß Fehler in dieser Art von Software sehr teuer werden oder gar katastrophale Auswirkungen haben können. Hieraus motiviert sich der Einsatz formaler Methoden zur Verifikation von Software, wie etwa Model-Checking, Theorem Proving, oder statischer Analysen. Viele eingebettete Systeme basieren entweder auf applikationsspezifischen Schaltungen, rekonfigurierbarer Logik, oder Mikrocontrollern. Typischerweise bieten die Hersteller von Mikrocontrollern eine Vielzahl verschiedener Geräte mit der gleichen Kernarchitektur an, die sich im Hinblick auf die verfügbare Ausstattung unterscheiden. Darüber hinaus gibt es Software-Werkzeuge, mit denen Entwickler bestehende Mikrocontroller an ihre eigenen Anforderungen anpassen oder sogar bei Bedarf neue Architekturen entwickeln können. Aus der Vielfalt an verfügbaren Geräten ergeben sich allerdings auch Nachteile. Die Möglichkeit zur automatisierten formalen Verifikation wird eingeschränkt, weil die dafür benötigten Werkzeuge zunächst einmal an jede neue Plattform angepaßt werden müssen. Je nach Werkzeug kann dies auch bedeuten, daß eine komplette Neuimplementierung nötig wird. Das Thema dieser Dissertation ist die Reduktion des Aufwandes, der nötig ist, um ein Verifikationswerkzeug an neue Mikrocontroller anzupassen. Zu diesem Zweck haben wir eine Sprache zur Beschreibung von Mikrocontrollern entworfen, SGDL, und einen Compiler implementiert, der Beschreibungen in dieser Sprache übersetzen kann in funktionsfähige Simulatoren und statische Analyse-Werkzeuge. Unsere Arbeit basiert auf [mc]square, einer Plattform für das Model-Checking und die statische Analyse von Assembler-Code. Um das Problem der Zustandsexplosion zu begrenzen, ist es erforderlich, daß die generierten Simulatoren auch Abstraktionstechniken unterstützen. Anhand einer Reihe von Abstraktionstechniken zeigen wir, wie diese in den vorgestellten Ansatz integriert werden können, und inwieweit es möglich ist, sie ganz oder teilweise automatisch zu erzeugen. In unseren Fallstudien demonstrieren wir die Implementierung von Simulatoren mit unserer neuen Sprache. Darüber hinaus untersuchen wir die Wirksamkeit der bereits genannten Abstraktionstechniken in den generierten Simulatoren, und vergleichen die Ergebnisse mit denen von handgeschriebenen Simulatoren.$$lger
000464374 520__ $$aCreating software for embedded systems requires rigid quality measures. The reason for this is that errors in the software may have very expensive or even disastrous consequences. This gives rise to the use of formal methods for software verification, such as model checking, theorem proving, and static analysis. Many embedded systems rely on either application-specific circuits, reconfigurable logics, or microcontrollers. Manufacturers of microcontrollers typically offer a wide variety of devices based on the same core architecture, which are equipped differently and thus offer different functionality. Furthermore, some tool chains exist that allow developers not only to choose from such off-the-shelf devices, but to customize them for specific kinds of tasks. In some cases, this may go to the extent of actually designing new architectures. It is precisely this wide variety of available devices that complicates the use of automated verification. Tools need to be adapted to a new platform, or even recreated in case they should be implemented in a too hardware-dependent way. The topic this thesis deals with is the reduction of the necessary effort for adapting a verification tool to new microcontrollers. To this end, we designed a language for describing microcontrollers, SGDL, and a compiler for translating such descriptions into operative simulators and static analyzers. We based our work on [mc]square, which is a platform for model checking and static analysis of assembly code software. In order to counter the state explosion problem, it is also necessary to include abstractions in generated simulators. We illustrate, on a number of abstraction techniques, how they can be integrated into the approach and whether they can be generated either partly or entirely. A number of case studies concerning the implementation of simulators with our new language is presented. Additionally, we examine the effectiveness of the aforementioned abstractions that are integrated into the generated simulators, and compare the results to those obtained when using manually implemented simulators.$$leng
000464374 591__ $$aGermany
000464374 650_7 $$2SWD$$aMikrocontroller
000464374 650_7 $$2SWD$$aEingebettetes System
000464374 650_7 $$2SWD$$aInformatik
000464374 653_7 $$aInformatik
000464374 653_7 $$aFormale Verifikation
000464374 653_7 $$aModel-Checking
000464374 653_7 $$aRetargeting
000464374 653_7 $$aHardware-Beschreibung
000464374 653_7 $$aEingebettete Software
000464374 653_7 $$aformal verification
000464374 653_7 $$ahardware description
000464374 653_7 $$aembedded software
000464374 7001_ $$0P:(DE-82)IDM06137$$aKowalewski, Stefan$$b1$$eThesis advisor
000464374 7001_ $$0P:(DE-82)IDM00503$$aLeupers, Rainer$$b2$$eThesis advisor
000464374 8564_ $$uhttps://publications.rwth-aachen.de/record/464374/files/5296.pdf
000464374 8564_ $$uhttps://publications.rwth-aachen.de/record/464374/files/5296_Gueckel.zip
000464374 8564_ $$uhttps://publications.rwth-aachen.de/record/464374/files/5296.gif?subformat=icon$$xicon
000464374 8564_ $$uhttps://publications.rwth-aachen.de/record/464374/files/5296.jpg?subformat=icon-180$$xicon-180
000464374 8564_ $$uhttps://publications.rwth-aachen.de/record/464374/files/5296.jpg?subformat=icon-700$$xicon-700
000464374 8564_ $$uhttps://publications.rwth-aachen.de/record/464374/files/5296.pdf?subformat=pdfa$$xpdfa
000464374 909CO $$ooai:publications.rwth-aachen.de:464374$$popenaire$$popen_access$$purn$$pdriver$$pVDB$$pdnbdelivery
000464374 9141_ $$y2014
000464374 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
000464374 9201_ $$0I:(DE-82)122810_20140620$$k122810$$lLehrstuhl für Informatik 11 (Software für eingebettete Systeme)$$x0
000464374 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x1
000464374 961__ $$z2015-03-10
000464374 970__ $$aHT018578647
000464374 9801_ $$aFullTexts
000464374 980__ $$aphd
000464374 980__ $$aVDB
000464374 980__ $$aUNRESTRICTED
000464374 980__ $$aI:(DE-82)122810_20140620
000464374 980__ $$aI:(DE-82)120000_20140620
000464374 980__ $$abook