[Javapathfinder-user] RTEmbed extension

[Pavel P. <pa...@ds...>]

Hello,

my name is Pavel Parizek. I am the main developer of the newly added
extension "RTEmbed".

The extension is aimed at verification of Java programs for real-time
and embedded platforms, in particular (but not exclusively) of Java
programs compliant with RTSJ.
Currently, it includes a checker of RTSJ memory access rules and an
optimization of state space traversal that is based on platform-specific
restrictions of concurrency. The restrictions are described in

P.Parizek and Tomas Kalibera. Platform-Specific Restrictions on
Concurrency in Model Checking of Java Programs, In FMICS 2009, LNCS, to
appear.

PDF of the paper is available at
http://dsrg.mff.cuni.cz/publications/ParizekKalibera-RestrictConcurrency.pdf.

In future, we plan to add support for other kinds of runtime errors
introduced by RTSJ and to develop additional domain-specific
optimizations of state space traversal.

The extension is in the "rtembed" directory. Additional information on
configuration and running are in the Readme file.
With questions or bug reports, please contact me at
pa...@ds....

Regards,

Pavel


-- 

Pavel Parizek, Ph.D.

Researcher
Distributed Systems Research Group
http://dsrg.mff.cuni.cz/~parizek
Phone:  (+420) 2 2191 4235
Fax:    (+420) 2 2191 4323
__________________________________
Department of Software Engineering
Faculty of Mathematics and Physics
Charles University in Prague
Malostranske namesti 25
11800 Prague 1, Czech Republic