Pflichtenheft (5): Snot

Abstract:

Das Dokument beschreibt das Pflichtenheft für das Java-Fortgeschrittenenpraktikum im Sommersemester 2001. Es liegt auch in Postscriptform oder als Pdf vor. Das Pflichtenheft wird während des Semesters dem Projektfortschritt und entsprechend den getroffenen Entscheidungen angepaßt und verfeinert.

1   Einleitung

• die von ihr bereitgestellte Funktionalität, und
• die von den anderen Gruppen erwartete Funktionalität festlegen.

2   Graphische Benutzerschnittstelle (Gui)

• Start: Beim Start einer Snot-Session erscheint ein Fenster, von dem aus es möglich ist, verschiedene Komponenten des Systems aufzurufen.
• Abhängigkeitsverwaltung: Eine Simulation kann erst dann aufgerufen werden, wenn das Programm syntaktisch korrekt ist. Das gleiche gilt für den Modelchecker. Die Aufgabe besteht darin, eine Definition der Abhängigkeiten zwischen den Komponenten festzulegen und sie im Tool zu implementieren.
• Sessionsverwaltung: (2te Priorität) Es soll möglich sein, eine Session (geöffnete Fenster, geladene Dateien, gewählte Optionen) zu speichern. Eine gespeicherte Session sollte wieder hergestellt werden können.

Schnittstellen

Design-Entscheidungen

• Die Oberflache wird mit swing-Komponenten aufgebaut; das gleiche gilt für den Editor.
• Die Oberfläche wird mit dem Werkzeug Forte 2.0 aufgebaut, das gleiche gilt für den Editor.

3   Editor

• Aufbau: Es soll möglich sein, ein SFC aus Schablonen von Schritten (steps), Transitionen und Pfaden zu zeichnen. Ein Vorschlag, wie SFCs aussehen können, ist in Abbildung 1 zu sehen.
• Speichern und Laden: Die Systeme sollen gespeichert und geladen werden können. Die Verwaltung des Speicherns liegt in der Zuständigkeit der Gui
• Selektieren: Einzelne Komponenten sollen selektiert werden können. Das dient zur Vorbereitung weiterer Aktionen.
• Löschen & Kopieren: Es soll möglich sein, selektierte Komponenten zu entfernen und zu kopieren.
• Highlight: der Editor soll eine Highlightfunktion zur Verfügung stellen. Es soll möglich sein, bestimmte Schritte und Transitionen hervorzuheben.

Schnittstelle

• der Bezeichner des Zustandes, oder
• der Zustand als Objekt.

1. das gespeicherte SFC (für den Simulator aus Abschnitt 5) und
2. Zugriff auf den Status (unveräandert, gespeichert ...)

4   Checks

Schnittstelle

• Wohlgeformtheit (was das genau ist, bleibt festzulegen)
• wohltypisiertheit der Aussdrücke. Wir gehen davon aus, das die Sprache stark typisiert ist. Die Typen der Operatoren sind in Tabelle 1 festgehalten.
• Die Verwendung von ausschließlich booleschen Variablen (dies ist für die SMV-Gruppe wichtig.)

---

operator/constant type(s) true,false Bool 0,1,... Int +,*,/ Int × Int ® Int - Int × Int ® Int, Int®Int <,>,£,³ Int ×Int ® Bool =, ¹ Int×Int ® Bool, Bool×Bool®Bool ¬ Bool×Bool

Table 1: Typen

---

5   Simulator

Berechnung des Nachfolgezustandes:

Anzeige eines Schrittes:

• Back-stepping
• Aufzeichnen (und Speichern) der genommenen Schritte.

Schnittstelle

6   Übersetzung nach SMV

MODULE main
VAR
  request : boolean;
  state : {ready,busy};
ASSIGN
  init(state) := ready;
  next(state) := case
                   state = ready & request : busy;
                   1 : {ready,busy};
                 esac;

7   Platzierung

Schnittstelle

Erweiterungsmöglichkeiten:

8   Parser

Schnittstelle

9   Model Checker (optional)

Schnittstelle

10   Codegenerierung (optional)

11   Hilfsprogramme

11.1   Pretty-Printer

Schnittstelle

A   Abstrakte Syntax

                      SFC ::=  istep      : step
                               steps      : step list
                               transs     : transition list
                               actions    : action list
                               declist    : declaration list
                     step ::=  name       : string
                               actions    : stepaction list
               stepaction ::=  qualifier  : action_qualifier
                               a_name     : string
                   action ::=  a_name     : string
                               sap        : stmt list  (* simple assignment program *)
                    stmt  ::=               skip
                           |                assign
                   assign ::=  var        : variable
                               val        : expr
                 variable ::=  name       : string
                               type       : type
         action_qualifier ::=  Nqual                            (* may be extended *)

               transition ::=  source     : step list
                               guard      : expr
                               target     : step list

              declaration ::=  var        : variable
                               type       : type
                               val        : constval

               expr       ::=               b_expr
                           |                u_expr
                           |                constval
                           |                variable
             b_expr       ::=  left_expr  : expr
                               right_expr : expr
                               op         : operand
                               type       : type
             u_expr       ::=  sub_expr   : expr
                               op         : operand             
                               type       : type
               operand    ::=               PLUS | MINUS | TIMES | DIV  (* Operand als *)
                           |                AND | OR | NEG              (* Konstanten in expr *)
                           |                LESS | GREATER | LEQ | GEQ | EQ | NEQ
                constval  ::=               ...| -2 | -1 | 0 | 1 | ... | true | false
                type      ::=               inttype
                           |                booltype

B   Informelle Semantik

B.1   Sequential Function Charts

---

Figure 1: SFC

---

• Inputs lesen von der Umgebung
• Aktionen der aktiven Steps ausführen
• Guards auswerten
• Transitionen nehmen (wenn möglich)
• Outputs schreiben

B.2   Zustände

References

[McM99a]

K. L. McMillan. Getting Started with SMV. Cadence Berkely Labs, 2001 Addison St., Berkely, CA, March 1999.

[McM99b]

K. L. McMillan. The SMV Language. Cadence Berkely Labs, 2001 Addison St., Berkely, CA, March 1999.

1

Es gibt Ausnahmen von der letzten Regel, nämlich für die (Snot-)Typen in den Ausdrücken. Die Typen sind nicht in die Konstruktoren mit aufgenommen. Die entsprechenden Felder werden nachträglich eingetragen.

This document was translated from L^AT_EX by H^EV^EA.