|
|
Uni
 Fk. II
Informatik
theoretica
CSD
~jfaber
AVACS
Informationen zum AVACS-Projekt
Da ich momentan beim SFB/TR 14 AVACS
(Automatic Verification and Analysis of Complex Systems) beschäftigt bin,
stelle ich hier aktuelles Material zu meiner Arbeit zur
Verfügung.
Konferenz-Vorträge:
| Dokumente |
Stand |
Hinweis |
|
| Verifying CSP-OZ-DC Specifications with Complex Data Types
and Timing Parameters |
07/07/12 |
Vortrag von der IFM 2007 in Oxford |
[.pdf]
|
| Model Checking Data-Dependent Real-Time Properties of the
European Train Control System |
06/11/13 |
Vortrag von der FMCAD 2006 in San Jose (CA) |
[.pdf]
|
| Verifying Real-Time Aspects of the European Train Control
System |
06/08/30 |
Vortrag vom German Verification Day 2006 in Bonn |
[.pdf]
|
Prototypen verschiedener Werkzeuge, die im Rahmen von AVACS entstanden sind:
| Werkzeug |
Stand |
Beschreibung |
|
| tf2Latex |
08/01/18 |
Ein einfaches Skript zum Übersetzen von XML-Testformeln nach
LaTeX. |
[.tgz]
|
| PEA-Toolkit |
06/08/29 |
Das PEA-Toolkit hat mittlerweile eine eigene Webseite. |
[link]
|
| Moby/PEA |
06/07/31 |
Moby/PEA ist ein graphischer Editor für Phasen-Event-Automaten (PEA). Es ist auf der Moby-Homepage verfügbar. |
[link]
|
| pea2tcs |
05/08/19 |
Transformiert Phasen-Event-Automaten in Transition-Constraint-Systems. |
[.tgz]
|
| tcs2armc |
05/08/19 |
Transformiert Transition-Constraint-Systems in XML-Syntax in
ARMC2-Eingabesyntax. |
[.tgz]
|
| simplifypeas |
05/08/19 |
Führt einige für's Model-Checking hilfreiche Operationen auf PEAs
durch, wie zum Beispiel das Hinzufügen von Testautomaten sowie das
Berechnen des Parallelprodukts. |
[.tgz]
|
| peatoolbox |
05/08/19 |
Umfasst die hier aufgeführten Tools zur Bearbeitung von PEAs
sowie zusätzlich einen graphischen Editor für PEAs (Moby/PEA). |
[.tgz]
|
Vorträge, Poster und Dokumente zu AVACS-Fallstudien (Zugriff auf auf AVACS-Mitglieder beschränkt; Zugangsdaten wie für AVACS-Webseite):
| Dokumente |
Stand |
Hinweis |
|
| From CSP-OZ-DC to Task Networks |
06/09/28 |
Vortrag vom AVACS-Meeting in Oldenburg. |
[.pdf]
|
| Poster, das den Kontext der Fallstudie in AVACS-R1 skizziert. |
06/03/30 |
Während des AVACS-Meetings im März '06 präsentiert. |
[.pdf]
|
| Case Study: Treatment of Emergency Messages - Informal Description |
04/10/27 |
|
[.pdf]
|
| Case Study: Treatment of Emergency Messages |
05/04/01 |
Überarbeitete Fassung |
[.pdf]
|
| Case Study: Placement of Movement Authorities - Informal Description |
04/10/27 |
|
[.pdf]
|
| Case Study: Placement of Movement Authorities |
05/03/29 |
RC1 |
[.pdf]
|
|
|
Seite empfehlen![[Logo]](http://theoretica.informatik.uni-oldenburg.de/pics/logos/logo-csd.gif){kind=logo}