POOSL – Computational Modeling

POOSL, the Parallel Object-Oriented Specification Language [1, 2], is an expressive formal modelling language for system specification. POOSL specifications are executable and can be used for validation, verification and performance analysis. In POOSL a system is captured as a set of parallel communicating processes. Processes encapsulate their state and data and interact only through synchronous message passing. POOSL has a mathematically defined semantics [3], which builds on operational semantics of common process calculi, such as CCS [4].

A particular strength of POOSL is its support for performance modeling and statistical analysis techniques [5]. There is an extensive library of stochastic modelling and statistical analysis techniques.

Tools

The POOSL language is only useful, because of the modelling and efficient simulation tools that have been developed, initially by TU/e. Later TNO-ESI has taken over the development of the Integrated Development Environment (IDE), while TU/e continued work on the simulator or execution engine. Currently, the POOSL IDE is an Eclipse project, supported by Obeo, specialist in visual development tools.

The execution engine for POOSL is called Rotalumis. It is a C++ based simulator that efficiently executes POOSL models. It supports co-simulation with external tools and interactive debugging within the POOSL IDE.

Selected Related Publications

B. D. Theelen, O. Florescu, M. C. W. Geilen, J. Huang, P. H. A. van der Putten, and J. P. M. Voeten, “Software/hardware engineering with the parallel object-oriented specification language,” in 2007 5th ieee/acm international conference on formal methods and models for codesign (memocode 2007), 2007, pp. 139-148.
[Bibtex]

@INPROCEEDINGS{TFGea07,
author={Theelen, B.D. and Florescu, O. and Geilen, M.C.W. and Huang, J. and van der Putten, P.H.A. and Voeten, J.P.M.},
booktitle={2007 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE 2007)},
title={Software/Hardware Engineering with the Parallel Object-Oriented Specification Language},
year={2007},
volume={},
number={},
pages={139-148},
doi={10.1109/MEMCOD.2007.371231}
}

M. C. W. Geilen, “Formal techniques for verification of complex real-time systems,” PhD Thesis, 2002.
[Bibtex]

@phdthesis{Gei02,
title = "Formal techniques for verification of complex real-time systems",
author = "M.C.W. Geilen",
year = "2002",
doi = "10.6100/IR557598",
language = "English",
isbn = "90-386-1930-8",
publisher = "Technische Universiteit Eindhoven",
school = "Electrical Engineering",
}

L. J. Bokhoven van, “Constructive tool design for formal languages : from semantics to executing models,” PhD Thesis, 2002.
[Bibtex]

@phdthesis{Bok02,
title = "Constructive tool design for formal languages : from semantics to executing models",
author = "Bokhoven, van, L.J.",
year = "2002",
doi = "10.6100/IR559665",
language = "English",
isbn = "90-386-1960-X",
publisher = "Technische Universiteit Eindhoven",
school = "Electrical Engineering",
}

B. D. Theelen, “Performance modelling for system-level design,” PhD Thesis, 2004.
[Bibtex]

@phdthesis{The04,
title = "Performance modelling for system-level design",
author = "B.D. Theelen",
note = "Proefschrift.",
year = "2004",
doi = "10.6100/IR581220",
language = "English",
isbn = "90-386-1633-3",
publisher = "Technische Universiteit Eindhoven",
school = "Electrical Engineering",
}

P. H. A. Putten van der and J. P. M. Voeten, “Specification of reactive hardware/software systems : the method software/hardware engineering (she),” PhD Thesis, 1997.
[Bibtex]

@phdthesis{PV97,
title = "Specification of reactive hardware/software systems : the method software/hardware engineering (SHE)",
author = "Putten, van der, P.H.A. and J.P.M. Voeten",
year = "1997",
doi = "10.6100/IR491299",
language = "English",
isbn = "90-386-0280-4",
publisher = "Technische Universiteit Eindhoven",
school = "Electrical Engineering",
}

J. Huang, J. Voeten, and H. Corporaal, “Correctness-preserving synthesis for real-time control software,” in 2006 sixth international conference on quality software (qsic’06), 2006, pp. 65-73.
[Bibtex]

@INPROCEEDINGS{HVC06,
author={Huang, Jinfeng and Voeten, Jeroen and Corporaal, Henk},
booktitle={2006 Sixth International Conference on Quality Software (QSIC'06)},
title={Correctness-preserving synthesis for real-time control software},
year={2006},
volume={},
number={},
pages={65-73},
doi={10.1109/QSIC.2006.21}
}

References

[1]

@INPROCEEDINGS{TFGea07,
author={Theelen, B.D. and Florescu, O. and Geilen, M.C.W. and Huang, J. and van der Putten, P.H.A. and Voeten, J.P.M.},
booktitle={2007 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE 2007)},
title={Software/Hardware Engineering with the Parallel Object-Oriented Specification Language},
year={2007},
volume={},
number={},
pages={139-148},
doi={10.1109/MEMCOD.2007.371231}
}

[2]