PEA-Toolkit

 

1 Einleitung

Das PEA-Toolkit ist ein GPL-lizensiertes Werkzeugpaket für Phasen-EventAutomatan (PEA).
Es beinhaltet ein Kommandozeilenprogramm, das Testautomaten zu Duration Calculus Testformeln erzeugen kann. Außerdem berechnet es auf Wunsch die Parallelkomposition dieser Testautomaten mit gegebenen PEA-Netzwerken. Die Testformeln und die PEA liegen dabei in einer XML-Repräsentation vor, die durch die XML-Schemata gegeben ist, die unten heruntergeladen werden können.
Das PEA-Toolkit unterstützt verschiedene Ausgaben, unter anderem ein Format, das von dem Model-Checker ARMC gelesen werden kann.

Ein weiteres, graphisches Entwicklungswerzeug, mit dem PEA (in dem vom PEA-Toolkit lesbaren Format) erstellt werden können, gibt es hier.

Die theoretischen Grundlagen zu PEA sind in [Hoe06] zu finden.

 

2 Downloads

Tool	Version	Beschreibung
peatoolkit	0.80b	Das PEA-Toolkit als binäre Version ohne Quellcode.	[.tgz]
peatoolkit	0.80b	Das PEA-Toolkit als binäre Version mit Quellcode.	[.tgz]
peatoolkit	0.79b	Das PEA-Toolkit als binäre Version ohne Quellcode.	[.tgz]
peatoolkit	0.79b	Das PEA-Toolkit als binäre Version mit Quellcode.	[.tgz]
peatoolkit	0.78b	Das PEA-Toolkit als binäre Version ohne Quellcode. Version mit verbesserter Unterstützung von Testautomaten und Bug-Fixes.	[.tgz]
peatoolkit	0.78b	Das PEA-Toolkit als binäre Version mit Quellcode. Version mit verbesserter Unterstützung von Testautomaten und Bug-Fixes.	[.tgz]
peatoolkit	0.76b	Das PEA-Toolkit als binäre Version ohne Quellcode.	[.tgz]
peatoolkit	0.76b	Das PEA-Toolkit als binäre Version mit Quellcode.	[.tgz]
tf2Latex	08/01	Ein einfaches Skript zum Übersetzen von XML-Testformeln nach LaTeX.	[.tgz]
peaschemas	r189	Die XML-Schemata für das PEA-Toolkit.	[.tgz]
results/examples	0.2	Eine aktualisierte Variante des ersten Beispielpakets (0.1)	[.tgz]
results/examples	0.1	Dieses Paket beinhaltet experimentelle Daten in Bezug auf die Fallstudie Emergency Treatment in the ETCS. Außerdem sind XML-Dateien mit Testformeln und Automatenmodellen enthalten, sodass unsere Ergebnisse unabhängig überprüft werden können.	[.tgz]

Das graphische Entwicklungswerkzeug Moby/PEA ist nicht Teil des PEA-Toolkits, sondern der Moby-Produktreihe.

 

3 Weitere Informationen

Für technische Fragen zu dem Toolkit kontaktieren Sie bitte J. Faber, R. Meyer
oder J. Hoenicke.

 

4 Veröffentlichung (über PEA)

[MFHR08]

R. Meyer, J. Faber, J. Hoenicke, and A. Rybalchenko. Model checking duration calculus: A practical approach. Formal Aspects of Computing, 20(4-5):481-505, July 2008. ISSN 0934-5043 (Print) 1433-299X (Online).
[ bib | .pdf | Abstract ]

[FJSS07]

Johannes Faber, Swen Jacobs, and Viorica Sofronie-Stokkermans. Verifying CSP-OZ-DC specifications with complex data types and timing parameters. In J. Davies and J. Gibbons, editors, Integrated Formal Methods, volume 4591 of Lecture Notes in Computer Science, pages 233-252. Springer-Verlag, July 2007.
[ bib | .pdf | Abstract ]

[MFR06]

Roland Meyer, Johannes Faber, and Andrey Rybalchenko. Model checking duration calculus: A practical approach. In K. Barkaoui, A. Cavalcanti, and A. Cerone, editors, Theoretical Aspects of Computing - ICTAC 2006, volume 4281 of LNCS, pages 332-346, 2006. This publication is available at SpringerLink.
[ bib | http | Abstract ]

[HM05]

Jochen Hoenicke and Patrick Maier. Model-checking of specifications integrating processes, data and time. In J.S. Fitzgerald, I.J. Hayes, and A. Tarlecki, editors, FM 2005, volume 3582 of LNCS, pages 465-480. Springer, 2005.
[ bib | .pdf | Abstract ]

[Hoe06]

J. Hoenicke. Combination of Processes, Data, and Time. PhD thesis, University of Oldenburg, Germany, 2006.
[ bib | .pdf ]