Formal Data Validation with Event-B
Software Engineering
2012-10-29 v1
Abstract
This article presents a verification and validation activity performed in an industrial context, to validate configuration data of a metro CBTC system by creating a formal B model of these configuration data and of their properties. A double tool chain is used to safely check whether a certain given input of configuration data fulfill its properties. One tool is based on some Rodin and open source plug-ins and the other tool is based on ProB.
Keywords
Cite
@article{arxiv.1210.7039,
title = {Formal Data Validation with Event-B},
author = {Frédéric Badeau and Marielle Doche-Petit},
journal= {arXiv preprint arXiv:1210.7039},
year = {2012}
}
Comments
In Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in developing dependable systems in Event-B, in conjunction with ICFEM 2012 - Kyoto, Japan, November 13, 2012