{"id":2832,"date":"2012-11-16T12:06:54","date_gmt":"2012-11-16T10:06:54","guid":{"rendered":"http:\/\/www.foerderverein-technische-fakultaet.at\/?p=2832"},"modified":"2013-05-09T19:53:51","modified_gmt":"2013-05-09T17:53:51","slug":"theorie-praxis-und-perspektiven-der-operationsbasierten-formalen-schaltungsverifikation","status":"publish","type":"post","link":"https:\/\/www.ftf.or.at\/?p=2832","title":{"rendered":"Theorie, Praxis und Perspektiven der operationsbasierten formalen Schaltungsverifikation"},"content":{"rendered":"

Formale Methoden wenden mathematische Arbeitsweisen \u2013 wie Modellbildung oder das Beweisen wesent-licher Eigenschaften solcher Modelle \u2013 auf den Entwurf technischer Systeme an. Das Teilgebiet der formalen Verifikation besch\u00e4ftigt sich mit dem Beweisen von Eigenschaften wichtiger Modelle. Als besonders wichtig gelten Endliche Automaten, denn diese beschreiben das Verhalten von Software- oder Hardwareimplemen-tierungen diskreter Steuerungen und damit von Schl\u00fcsselfunktionalit\u00e4t fast aller technischen Systeme.<\/span><\/p>\n

Einf\u00fchrend wird der Stand der Kunst des Model Checking erl\u00e4utert. Technischer Kern des Vortrags ist ein wesentlich anwendungsspezifischeres Verfahren, das durch ein VHDL-Programm beschriebenes Verhalten einer digitalen Schaltung l\u00fcckenlos und automatisch mit einem abstrakten Automaten, einem abstrakten VHDL, vergleicht. Abstraktes VHDL ist eine Feinspezifikation der Schaltung durch ihre Operationen. Operationen formalisieren i.A. kurze Schaltungsaktivit\u00e4ten wie Lese- oder Schreibzugriffe, Instruktionen oder Arbitrierungs-zyklen. Es wird erl\u00e4utert, wie abstraktes VHDL erstellt, bez\u00fcglich der Grobspezifikation verifiziert, und dann mit dem VHDL automatisch verglichen wird. Dieser Vergleich zeigt Fehler in der Implementierung der Operationen an sowie Diagnosen zu ihrer Behebung. Automatische \u00dcberpr\u00fcfung eines Kriteriums zur vollst\u00e4ndigen Erfassung der Schaltungsfunktionalit\u00e4t durch Operationen garantiert Korrektheit des Codes. \u00a0<\/span><\/p>\n

Es folgt eine kurze Darstellung der Anwendungs- und Prozessseite des Themas: Die operationsbasierte formale Schaltungsverifikation wurde in der zentralen Siemensforschung vor fast 20 Jahren konzipiert, bei Siemens, Infineon und weiteren Chipherstellern erprobt und schlie\u00dflich in dem Spin-Off OneSpin Solutions zur Produkt-reife gef\u00fchrt. Der Ansatz garantierte Korrektheit zahlreicher VHDL-Programme einer Gr\u00f6\u00dfenordnung von 100000 LoC \u2013 ein prominentes Beispiel ist der in der Automobilelektronik weit verbreitete TriCore-Prozessor von Infineon. Obwohl die Verifikationsproduktivit\u00e4t des Ansatzes mit der der simulationsbasierten Verifikation vergleichbar ist und auch \u201eNichtformalisten\u201c die Technik erfolgreich erlernen k\u00f6nnen, hat sich der Ansatz noch nicht in der Breite durchgesetzt. Auch die \u00dcbertragbarkeit des Erfolgsrezepts der operationsbasierten Modellierung auf andere Anwendungsbereiche wie die Fertigungstechnik wurde bisher kaum untersucht.<\/span><\/p>\n

Der Vortrag schlie\u00dft mit der Analyse der Erfolgsfaktoren f\u00fcr den Breiteneinsatz der operationsbasierten Schal-tungsverifikation und schildert m\u00f6gliche n\u00e4chste Schritte. Vielversprechend erscheint eine weitere Nutzung von abstraktem VHDL f\u00fcr die funktionale Sicherheitsanalyse einer Schaltung. W\u00e4hrend Verifikation Entwurfs-fehler aufsp\u00fcrt, besch\u00e4ftigt sich die Sicherheitsanalyse mit zuf\u00e4lligen Fehlern, verursacht etwa durch Alterungs-prozesse oder durch Strahlungseinfl\u00fcsse, und so m\u00f6glichen schwerwiegenden Systemausf\u00e4llen. Es wird skizziert, wie mithilfe des abstrakten VHDL eine Sicherheitsanalyse f\u00fcr Schaltungen konzipiert und so eine Br\u00fccke zwischen formaler Verifikation und funktionaler Sicherheitsanalyse geschlagen wurde. <\/span><\/p>\n

Kurz-Bio: Wolfram B\u00fcttner promovierte 1978 in Mathematik an der Tulane University in New Orleans, habilitierte in diesem Fach an der TU Darmstadt und wechselte dann in die Informatik. Seit 1989 ist er Au\u00dferplanm\u00e4\u00dfiger Professor an der TU Kaiserslautern. Von 1984 bis 2002 arbeitete Dr. B\u00fcttner in den Corporate Technology Labs (CT) von Siemens in M\u00fcnchen – zuletzt als Abteilungsdirektor mit Verantwortung f\u00fcr die Themengebiete formale Methoden, diskrete und stochastische Optimierung sowie Lernende Systeme. Seit 2000 fokussierte Dr. B\u00fcttner seine T\u00e4tigkeit auf die formale Schaltungsverifikation und f\u00fchrte die Verifikationstechnologie von CT zur Produktreife und auf den canadian pharmacy no prescription<\/a> Markt \u2013 erst bei Infineon und ab 2005 in zwei Start-Up\u2019s.<\/p>\n

 <\/p>\n","protected":false},"excerpt":{"rendered":"

Formale Methoden wenden mathematische Arbeitsweisen \u2013 wie Modellbildung oder das Beweisen wesent-licher Eigenschaften solcher Modelle \u2013 auf den Entwurf technischer Systeme an. Das Teilgebiet der formalen Verifikation besch\u00e4ftigt sich mit dem Beweisen von Eigenschaften wichtiger Modelle. Als besonders wichtig gelten … Continue reading →<\/span><\/a><\/p>\n","protected":false},"author":7,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"sfsi_plus_gutenberg_text_before_share":"","sfsi_plus_gutenberg_show_text_before_share":"","sfsi_plus_gutenberg_icon_type":"","sfsi_plus_gutenberg_icon_alignemt":"","sfsi_plus_gutenburg_max_per_row":"","footnotes":""},"categories":[1],"tags":[],"class_list":["post-2832","post","type-post","status-publish","format-standard","hentry","category-tewi-kolloquium"],"_links":{"self":[{"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/posts\/2832","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/users\/7"}],"replies":[{"embeddable":true,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=2832"}],"version-history":[{"count":3,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/posts\/2832\/revisions"}],"predecessor-version":[{"id":4265,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=\/wp\/v2\/posts\/2832\/revisions\/4265"}],"wp:attachment":[{"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=2832"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=2832"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.ftf.or.at\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=2832"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}