Beitrags-Archiv für die Kategory 'Modellierung'

ASSIST – Architecture Synthesis for Safety-Critical Systems

Dienstag, 29. Juli 2014 22:17

Die Forschungsergebnisse meiner Dissertation im Bereich “Entwicklung von sicherheitskritischen eingebetteten Systemen mit harten Echtzeitanforderungen” werden in der neuen Toolsuite ASSIST umgesetzt. Sie ermöglicht die zielgerichtete Konstruktion von Mappings und Schedules von Softwarekomponenten auf komplexen Hardware-Architekturen mit Multicore-Prozessoren. Der Funktionsumfang dieser Toolsuite wird schrittweise erweitert. Der aktuelle Stand kann unter assist.hilbri.ch heruntergeladen werden.

assist-540px

 

Die ASSIST Toolsuite ist unter Windows (32/64bit), Linux (GTK 32/64bit) und OSX (64bit) lauffähig. Sie steht unter der GPLv2 Lizenz. Andere Lizenzen sind auf Anfrage möglich. Der Quellcode wird auf GitHub gehostet. Zur Synthese von Systemarchitekturen wird der JaCoP 4.1 Constraint Solver verwendet.

Thema: Forschung & Promotion, Modellierung, Multicore | Kommentare (0) | Autor:

Nutzung von Mehrkernprozessoren in sicherheitskritischen Cyber-Physical Systems

Donnerstag, 14. Juni 2012 9:58

An der BTU Cottbus hielt ich am 01.06.2012 einen Vortrag zu meinem Promotionsthema. Der lange Vortragstitel lautet: “Nutzung von Mehrkernprozessoren in sicherheitskritischen Cyber-Physical Systems – Eine Entwicklungsmethodik zur Multifunktionsintegration auf der Basis von Correctness-by-Construction”. Hier eine kurze Zusammenfassung aus der Ankündigung:

Eingebettete Systeme übernehmen immer mehr Funktionen in unserem Alltag. Dazu werden sie stärker vernetzt und enger an physikalische Prozesse in der Umgebung gekoppelt. Sie
werden zu Cyber-Physical Systems. Mehrkernprozessoren bieten eine vielversprechende Plattform zur Realisierung dieser Systeme. Allerdings ist ihr Einsatz mit verschiedenen Herausforderungen verbunden. Diese liegen insbesondere bei der sicheren Integration von verschiedenen Anwendungen mit unterschiedlichen Kritikalitätsstufen.

Die Entwicklung derartiger Systeme muss die Umsetzung von sowohl funktionalen Anforderungen als auch Qualitätsanforderungen, wie Echtzeitfähigkeit und Zuverlässigkeit,
miteinander verbinden. Dies stellt eine signifikante Herausforderung für etablierte Entwicklungsprozesse dar.

“Correctness-by-Construction (CbyC)” ist ein etablierter Ansatz zur Entwicklung von High-Integrity Software, zum Beispiel für die Steuerung von Kernkraftwerken. Dieser Ansatz ist die Folge der
Erkenntnis, dass klassische Entwicklungsverfahren für sicherheitskritische Systeme nicht ausreichend sind. Im Rahmen von CbyC wird deshalb ein starker Fokus auf ein formalisiertes und
automatisierbares Vorgehen gelegt.

In diesem Vortrag wird gezeigt, wie die Grundsätze von CbyC auch im Rahmen des Systems Engineering bei der Integration von Anwendungen auf Mehrkernprozessoren angewendet werden
können. Der Schwerpunkt wird dabei auf die Aspekte: Konstruktion von Deployments und Schedules, sowie eine automatisierte Validierung gelegt.

Hier gibt es die Folien zum Download.

Thema: Forschung & Promotion, Modellierung, Multicore, Vorträge | Kommentare (0) | Autor:

“Correctness by Construction” für die Konsolidierung auf Multicore Prozessoren

Mittwoch, 5. Oktober 2011 14:28

In meiner Promotion entwickele ich einen methodischen Ansatz weiter, der sich bereits mehrfach in der Entwicklung sicherheitskritischer Systeme bewährt hat. Er verbirgt sich hinter dem Motto “Correctness by Construction” und versucht eine schrittweise Formalisierung des Entwicklungsprozesse zu erreichen, um damit automatisierte Verifikationen zu ermöglichen, so dass die Fehlerraten um Größenordnungen gesenkt werden.

Währten dieser Ansatz bisher im Bereich der Software-Entwicklung eingesetzt wurde, arbeite ich an einer Erweiterung auf die Integration von sicherheitskritischen Anwendungen auf einem Multicore oder Manycore Prozessor. Die Grundidee bleibt dabei natürlich erhalten: das korrekte Verhalten kann anhand der Entwicklungsschritte nachgewiesen werden und muss nicht umständlich die Analysen des Verhalten gezeigt werden.

Ich glaube nicht, dass man mit vollständiger Formalisierung des Entwicklungsprozesses die Anforderungen heutiger Systeme bändigen kann. Dafür sind die Entwicklungszyklen zu kurz und die Anforderungskataloge zu kurz. Dennoch bin ich davon überzeugt, dass gerade die Komplexität von Mehrkernprozessoren zu einer verstärkten Akzeptanz von punktuell eingesetzten, formalen Methoden führen wird. Diese müssen dann natürlich auch durch den Fachexperten nutzbar gestaltet sein. Kann man denn eine formale Spezifikation in Z für eine kritische ECU von einem Automotive-Entwickler erwarten? Ich denke nicht.

Thema: Forschung & Promotion, Modellierung, Multicore | Kommentare (0) | Autor:

Scala Actors Library

Freitag, 27. November 2009 11:21

Im Rahmen meiner Promotion beschäftige ich mich mit dem Thema Multi-/Many-core Prozessoren, insbesondere im Umfeld sicherheitskritischer, verteilter, eingebetteter Systeme mit harten Echtzeitanforderungen.

In diesem Zusammenhang habe ich mir detailliert die Programmiersprache Scala und die dazugehörige Bibliothek “Actors” angeschaut. Dabei entstand der folgende Überblicksvortrag, der auf den am Ende genannten Referenzen aufbaut.

Natürlich erschlägt man mit diesem zugrunde liegenden Prozessmodell nicht alle Problemklassen der parallelen Programmierung. Dennoch bin ich der Überzeugung, dass es eine hinreichend große Menge an Anwendungsbereichen gibt, in denen diese Art der Modellierung sinnvoll ist.

[Scala-Actors.pdf]

Thema: Modellierung, Multicore, Vorträge | Kommentare (0) | Autor:

Petri Netze mit Zeitangaben

Mittwoch, 12. August 2009 10:58

In einem Doktoranden-Seminar wurde ein Buch zur Spezifikation Echtzeitanforderungen in Form verschiedener Vorträge bearbeitet. Ich hatte eines der einführenden Kapitel und habe die “Zeit-Peti-Netze” vorgestellt.

Das zugrunde liegende Buch trägt den etwas sperrigen Titel “Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach” und läßt hier von Amazon beziehen.

Diesen Vortrag als PDF will ich natürlich auch der Allgemeinheit zur Verfügung stellen.

Download

Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach (Studies in Computational Intelligence)

Thema: Forschung & Promotion, Modellierung, Vorträge | Kommentare (0) | Autor: