Some Projects Examples

Formal modeling of moving block signaling system
We provide a formal model of a part of ERTMS/ETCS moving block level 3 for safety analysis in the presence of cyber attacks.
PDF Code
Formal modeling of moving block signaling system
EBSysMLSec
Translation of SysML models to Event-B specification for formal analysis.
Code
EBSysMLSec
RBC ID block assignment
An optimization tool developed for Trafikverket to configure RBCs.
RBC ID block assignment
Deductive verification of an ABS controller
We annotate and verify a C implementation of an ABS controller using Frama-C.
Deductive verification of an ABS controller
Model checking of a device driver of a transmitter
We model a device driver of a transmitter in NuSMV and verify the system properties.
Model checking of a device driver of a transmitter