Skip to Main content Skip to Navigation
Conference papers

Automatic Verification of Parametric Specifications with Complex Topologies

Abstract : The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact.We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download
Contributor : Ist Inria Nancy Grand Est Connect in order to contact the contributor
Submitted on : Thursday, October 7, 2010 - 5:32:07 PM
Last modification on : Friday, September 21, 2018 - 8:02:04 PM
Long-term archiving on: : Monday, January 10, 2011 - 11:09:05 AM


Files produced by the author(s)


  • HAL Id : inria-00523033, version 1
  • ARXIV : 1010.1602



Johannes Faber, Carsten Ihlemann, Swen Jacobs, Viorica Sofronie-Stokkermans. Automatic Verification of Parametric Specifications with Complex Topologies. Integrated Formal Methods - IFM 2010, INRIA Nancy Grand Est, Oct 2010, Nancy, France. ⟨inria-00523033⟩



Record views


Files downloads