Abstract
In this paper we apply the contract theory to the analysis of the door control functionality in a metro train. The system under development is specified and modeled by rail domain experts. Contract theory is used to formalize some safety requirements that can be then automatically analyzed by our developed tool suite, Formal Specs Verifier (FSV). The produced work that derives by working with and on FSV represents a good starting point for matching the industrial needs in the field of system analysis and testing and for the definition of new analysis methods that provides indications on how to efficiently reduce the effort of making an exhaustive testing. © 2014 Springer International Publishing.
Author supplied keywords
Cite
CITATION STYLE
Carloni, M., Ferrante, O., Ferrari, A., Massaroli, G., Orazzo, A., Petrone, I., & Velardi, L. (2014). Contract-based analysis for verification of Communication-Based Train Control (CBTC) system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8696 LNCS, pp. 137–146). Springer Verlag. https://doi.org/10.1007/978-3-319-10557-4_17
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
