I proposed a paper to ITST 2010 conference and it has been accepted!

The core proposal of this paper is to link low level B Method model (B0 code) to Model checking techniques. More exactly, I propose to automatically extract a SPIN model in Promela language from a B0 model. I applied this approach on a simple model of a railway level crossing.

For further details, just read "Checking temporal properties on state based formal specification: application to railway level crossing"! ;-)