POOSL

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.

Links

• https://projects.eclipse.org/projects/modeling.poosl
• https://www.poosl.org/
• documentation: https://eclipse.github.io/poosl/nightly/help/index.html

References

1. B. D. Theelen and O. Florescu and M. C. W. Geilen and J. Huang and P. H. A. Putten and J. P. M. Voeten (2007): 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), pp. 139-148, 2007.
2. P. H. A. van der Putten and J. P. M. Voeten (1997): Specification of reactive hardware/software systems : the method software/hardware engineering (SHE). Electrical Engineering, 1997, ISBN: 90-386-0280-4.
3. L. J. van Bokhoven (2002): Constructive tool design for formal languages : from semantics to executing models. Electrical Engineering, 2002, ISBN: 90-386-1960-X.
4. Robin Milner (1980): A calculus of communicating systems. Springer, 1980.
5. B. D. Theelen (2004): Performance modelling for system-level design. Electrical Engineering, 2004, ISBN: 90-386-1633-3, (Proefschrift.).

Selected Related Publications

@inproceedings{TFGea07,

title = {Software/Hardware Engineering with the Parallel Object-Oriented Specification Language},

author = {B. D. Theelen and O. Florescu and M. C. W. Geilen and J. Huang and P. H. A. Putten and J. P. M. Voeten},

doi = {10.1109/MEMCOD.2007.371231},

year  = {2007},

date = {2007-01-01},

urldate = {2007-01-01},

booktitle = {2007 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE 2007)},

pages = {139-148},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{The07,

title = {A Performance Analysis Tool for Scenario-Aware Streaming Applications},

author = {B. D. Theelen},

doi = {10.1109/QEST.2007.7},

year  = {2007},

date = {2007-01-01},

urldate = {2007-01-01},

booktitle = {Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007)},

pages = {269-270},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@inproceedings{HVC06,

title = {Correctness-preserving synthesis for real-time control software},

author = {Jinfeng Huang and Jeroen Voeten and Henk Corporaal},

doi = {10.1109/QSIC.2006.21},

year  = {2006},

date = {2006-01-01},

urldate = {2006-01-01},

booktitle = {2006 Sixth International Conference on Quality Software (QSIC'06)},

pages = {65-73},

keywords = {},

pubstate = {published},

tppubtype = {inproceedings}

}

@phdthesis{The04,

title = {Performance modelling for system-level design},

author = {B. D. Theelen},

doi = {10.6100/IR581220},

isbn = {90-386-1633-3},

year  = {2004},

date = {2004-01-01},

urldate = {2004-01-01},

publisher = {Technische Universiteit Eindhoven},

school = {Electrical Engineering},

note = {Proefschrift.},

keywords = {},

pubstate = {published},

tppubtype = {phdthesis}

}

@phdthesis{Bok02,

title = {Constructive tool design for formal languages : from semantics to executing models},

author = {L. J. van Bokhoven},

doi = {10.6100/IR559665},

isbn = {90-386-1960-X},

year  = {2002},

date = {2002-01-01},

urldate = {2002-01-01},

publisher = {Technische Universiteit Eindhoven},

school = {Electrical Engineering},

keywords = {},

pubstate = {published},

tppubtype = {phdthesis}

}

@phdthesis{Gei02,

title = {Formal techniques for verification of complex real-time systems},

author = {M. C. W. Geilen},

doi = {10.6100/IR557598},

isbn = {90-386-1930-8},

year  = {2002},

date = {2002-01-01},

urldate = {2002-01-01},

publisher = {Technische Universiteit Eindhoven},

school = {Electrical Engineering},

keywords = {},

pubstate = {published},

tppubtype = {phdthesis}

}

@phdthesis{PV97,

title = {Specification of reactive hardware/software systems : the method software/hardware engineering (SHE)},

author = {P. H. A. van der Putten and J. P. M. Voeten},

doi = {10.6100/IR491299},

isbn = {90-386-0280-4},

year  = {1997},

date = {1997-01-01},

urldate = {1997-01-01},

publisher = {Technische Universiteit Eindhoven},

school = {Electrical Engineering},

keywords = {},

pubstate = {published},

tppubtype = {phdthesis}

}

@book{Mil80,

title = {A calculus of communicating systems},

author = {Robin Milner},

year  = {1980},

date = {1980-01-01},

urldate = {1980-01-01},

publisher = {Springer},

keywords = {},

pubstate = {published},

tppubtype = {book}

}