Velos (Verifica Logica di Sicurezza) is a project aimed to apply formal methods to verification and validation of Logica di Sicurezza (LdS), software designed to monitor and control railway systems.
VELOS is able to convert LdS specifications from a C++ like format to C and SMV. After this step several different tools can be used to validate the code. Depending on the user intention some of the generated SMV files can be merged into one and provided to NUSMV model checker which can verify the properties.
General Info:
Start Date: 9 Aug 2009
