PEA Toolkit

 

1 Introduction

The PEA tool set is a GPL licensed collection of tools for Phase Event Automata (PEA).
It comprises a command line java program that generates test automata of a duration calculus test formula and that computes the parallel product of those test automata and an input PEA network. The test formulae and the PEA have to be in the XML format defined by the XML schemas given below.
It supports output in several formats, in particular the input format for the model checker ARMC.

Additionally, there is a tool Moby/PEA for designing PEA, which also supports an XML import/export into the format readable by the PEA toolkit. It can be found here and it is part of the Moby product line.

The theoretical foundation of PEA can be found in [Hoe06].

 

2 Downloads

Tool	Version	Description
peatoolkit	0.90b	The PEA toolkit as binary version without sources.	[.tgz]
peatoolkit	0.90b	The PEA toolkit as binary version with sources.	[.tgz]
peatoolkit	0.80b	The PEA toolkit as binary version without sources.	[.tgz]
peatoolkit	0.80b	The PEA toolkit as binary version with sources.	[.tgz]
peatoolkit	0.79b	The PEA toolkit as binary version without sources.	[.tgz]
peatoolkit	0.79b	The PEA toolkit as binary version with sources.	[.tgz]
peatoolkit	0.78b	The PEA toolkit as binary version without sources. Improved test automata support and some bug fixes.	[.tgz]
peatoolkit	0.78b	The PEA toolkit as binary version with sources. Improved test automata support and some bug fixes.	[.tgz]
peatoolkit	0.76b	The PEA toolkit as binary version without sources.	[.tgz]
peatoolkit	0.76b	The PEA toolkit as binary version with sources.	[.tgz]
tf2Latex	08/01	A simple script to translate XML test formulae to LaTeX.	[.tgz]
peaschemas	r189	The XML schemas for the PEA toolkit.	[.tgz]
results/examples	0.2	Updated version of the first example packages (0.1).	[.tgz]
results/examples	0.1	Contains example files comprising PEA models and test formulae used for verifying our case study Emergency Treatment in the ETCS. Thus, our results can be reproduced independently.	[.tgz]

The graphical editor Moby/PEA is not part of the PEA toolkit but of the Moby product line.

 

3 Further Information

For technical questions please contact J. Faber, R. Meyer, or J. Hoenicke.

 

4 Publications (related to 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 | DOI | .pdf | Abstract ]

[FJSS07]

J. Faber, S. Jacobs, and V. 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]

R. Meyer, J. Faber, and A. 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 | .pdf | 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 ]