36
2 Spezifikation und Modellierung
• Terminierung: Es sollte möglich sein, anhand der Spezifikation Prozesse zu identifizieren, die terminieren. Daher möchten wir Spezifikationen verwenden, für die
das Halteproblem (das Problem, herauszufinden, ob ein gegebener Algorithmus
terminieren wird oder nicht, siehe z.B. [494]) entscheidbar ist.
• Unterstützung für Nicht-Standard-Ein/Ausgabegeräte: Viele eingebettete
Systeme verwenden andere Ein- und Ausgabegeräte als die vom PC her bekannten Tastaturen und Mäuse. Es sollte möglich sein, die Eigenschaften solcher
Geräte in bequemer Weise zu spezifizieren.
• Nicht-funktionale Eigenschaften: Reale Systeme besitzen eine Reihe nichtfunktionaler Eigenschaften, wie etwa Fehlertoleranz, Größe, Erweiterbarkeit,
Lebenserwartung, Energieverbrauch, Gewicht, Recycling-Fähigkeit, Benutzerfreundlichkeit, elektromagnetische Verträglichkeit (EMC) und so weiter. Es ist
nicht zu erwarten, dass sich all diese Eigenschaften auf eine formale Weise definieren lassen.
• Unterstützung für den Entwurf verlässlicher Systeme: Spezifikationstechniken sollten den Entwurf von verlässlichen Systemen unterstützen. Beispielsweise
sollte die Spezifikationssprache eine eindeutige Semantik haben und den Einsatz formaler Verifikationstechniken erlauben. Außerdem sollte es möglich sein,
Anforderungen an Betriebs- und Informationssicherheit zu beschreiben.
• Keine Hürden für die Erzeugung von effizienten Implementierungen: Da
eingebettete Systeme effizient sein müssen, sollte die Spezifikationssprache eine
effiziente Realisierung des Systems nicht behindern oder unmöglich machen.
• Geeignetes Berechnungsmodell (engl. Model of Computation (MoC)): Ein häufig verwendetes Berechnungsmodell ist das sequenzielle Ausführungsmodell nach
von Neumann in Kombination mit einem Kommunikationsverfahren. Im MoC
nach von Neumann sind Spezifikationen üblicherweise in Tasks, Prozesse oder
Threads gegliedert, die wie folgt definiert werden können:
Definition 2.2 ([394]): Eine Task kann allgemein definiert werden als „eine
zugewiesene Menge an Arbeit, die häufig in einer bestimmten Zeit zu erledigen
ist”.
Im Kontext von eingebetteten Systemen verstehen wir unter einer Task i.d.R.
bestimmte Berechnungen, die auszuführen sind.
Definition 2.3 ([525]): Ein Prozess ist ein in Ausführung befindliches Programm.
Eine Präzisierung dieses Begriffs wird in der Definition 4.1 gegeben werden.
Tasks sind teilweise abstrakter beschrieben als die Prozesse, sie sind dann auf
konkrete Prozesse innerhalb eines Betriebssystems abzubilden. Allerdings werden die Begriffe Task und Prozess auch teilweise austauschbar benutzt. Eng
verwandt mit dem Begriff „Prozess” ist der Begriff des Threads.
Definition 2.4: Ein Thread ist ein „leichtgewichtiger” Prozess. Das bedeutet,
dass die Umschaltung zwischen der Ausführung von Threads mit weniger Aufwand verbunden ist als bei der Umschaltung zwischen allgemeinen Prozessen.
2 Spezifikation und Modellierung
• Terminierung: Es sollte möglich sein, anhand der Spezifikation Prozesse zu identifizieren, die terminieren. Daher möchten wir Spezifikationen verwenden, für die
das Halteproblem (das Problem, herauszufinden, ob ein gegebener Algorithmus
terminieren wird oder nicht, siehe z.B. [494]) entscheidbar ist.
• Unterstützung für Nicht-Standard-Ein/Ausgabegeräte: Viele eingebettete
Systeme verwenden andere Ein- und Ausgabegeräte als die vom PC her bekannten Tastaturen und Mäuse. Es sollte möglich sein, die Eigenschaften solcher
Geräte in bequemer Weise zu spezifizieren.
• Nicht-funktionale Eigenschaften: Reale Systeme besitzen eine Reihe nichtfunktionaler Eigenschaften, wie etwa Fehlertoleranz, Größe, Erweiterbarkeit,
Lebenserwartung, Energieverbrauch, Gewicht, Recycling-Fähigkeit, Benutzerfreundlichkeit, elektromagnetische Verträglichkeit (EMC) und so weiter. Es ist
nicht zu erwarten, dass sich all diese Eigenschaften auf eine formale Weise definieren lassen.
• Unterstützung für den Entwurf verlässlicher Systeme: Spezifikationstechniken sollten den Entwurf von verlässlichen Systemen unterstützen. Beispielsweise
sollte die Spezifikationssprache eine eindeutige Semantik haben und den Einsatz formaler Verifikationstechniken erlauben. Außerdem sollte es möglich sein,
Anforderungen an Betriebs- und Informationssicherheit zu beschreiben.
• Keine Hürden für die Erzeugung von effizienten Implementierungen: Da
eingebettete Systeme effizient sein müssen, sollte die Spezifikationssprache eine
effiziente Realisierung des Systems nicht behindern oder unmöglich machen.
• Geeignetes Berechnungsmodell (engl. Model of Computation (MoC)): Ein häufig verwendetes Berechnungsmodell ist das sequenzielle Ausführungsmodell nach
von Neumann in Kombination mit einem Kommunikationsverfahren. Im MoC
nach von Neumann sind Spezifikationen üblicherweise in Tasks, Prozesse oder
Threads gegliedert, die wie folgt definiert werden können:
Definition 2.2 ([394]): Eine Task kann allgemein definiert werden als „eine
zugewiesene Menge an Arbeit, die häufig in einer bestimmten Zeit zu erledigen
ist”.
Im Kontext von eingebetteten Systemen verstehen wir unter einer Task i.d.R.
bestimmte Berechnungen, die auszuführen sind.
Definition 2.3 ([525]): Ein Prozess ist ein in Ausführung befindliches Programm.
Eine Präzisierung dieses Begriffs wird in der Definition 4.1 gegeben werden.
Tasks sind teilweise abstrakter beschrieben als die Prozesse, sie sind dann auf
konkrete Prozesse innerhalb eines Betriebssystems abzubilden. Allerdings werden die Begriffe Task und Prozess auch teilweise austauschbar benutzt. Eng
verwandt mit dem Begriff „Prozess” ist der Begriff des Threads.
Definition 2.4: Ein Thread ist ein „leichtgewichtiger” Prozess. Das bedeutet,
dass die Umschaltung zwischen der Ausführung von Threads mit weniger Aufwand verbunden ist als bei der Umschaltung zwischen allgemeinen Prozessen.