The VESG tool (Vital Embedded Settings Generator) was developed in B within the scope of the Urbalis Evolution project.
- CLIENT : Alstom
- DATE : May 2009/September 2010
In order to function correctly the onboard Urbalis Evolution software requires the presence of information about the tracks used by the rolling stock. The role of the VESG is to produce the file which will be embarked and which contains this data. The tooling can function on work stations equipped with Windows or Linux.
It processes the input XML files containing track descriptions. These files are generated by the Alstom teams from other dedicated tooling. They contain information on different noteworthy elements present on the tracks: points, signals, slopes, speed limits… The VESG reads these files, then performs a set number of pre-calculations on the information they contain. Ultimately it generates a binary file containing the results of this processing, in a format able to be understood by the onboard software.
This data file will then be loaded onto the trains running along the relevant tracks. The energy control software uses it to find out about the environment around the train in relation to its current position, and thus decides on the procedure to adopt according to this information, especially in view of the possible need to activate an emergency brake.
CLEARSY was fully responsible for the development of the VESG, when applying the B method. The first stage was the tooling specification in the form of B models, in collaboration with the Alstom teams.
The code corresponding with these specifications was then developed and proven thanks to Atelier B. It was decided to develop this new version in B so as to avoid the burden of maintaining the two pieces of redundant software, as was the case beforehand. The proof of the models also enables a reduction in the number of tests to be performed on the VESG B.
- The VESG is a sizeable B software. The B model leads to around 30,000 proof obligations, which are notably processed with the help of numerous proof rules, which have been integrated into the proof tooling.
- The VESG regularly undergoes slight modifications, linked to the new types of elements to be taken into account on the tracks. However, in 2010, it underwent a more sizeable evolution. Before that time, Alstom used a specific tool to deal with the slopes on the tracks. The information generated by this tooling was then integrated into the XML files for the VESG. As such it was decided in 2010 to merge this tooling into the VESG. The latter now makes the more complicated calculations about the slope information itself.