Computer Science – Software Engineering
Scientific paper
2010-10-08
Integrated Formal Methods - IFM 2010, Nancy : France (2010)
Computer Science
Software Engineering
The original publication is available at http://www.springerlink.com
Scientific paper
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.
Faber Johannes
Ihlemann Carsten
Jacobs Swen
Sofronie-Stokkermans Viorica
No associations
LandOfFree
Automatic Verification of Parametric Specifications with Complex Topologies does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Automatic Verification of Parametric Specifications with Complex Topologies, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Automatic Verification of Parametric Specifications with Complex Topologies will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-485858