de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Automatic Verification of Parametric Specifications with Complex Topologies

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44396

Faber,  Johannes
Automation of Logic, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons44669

Ihlemann,  Carsten
Automation of Logic, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons44687

Jacobs,  Swen
Automation of Logic, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45516

Sofronie-Stokkermans,  Viorica
Automation of Logic, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

Faber, J., Ihlemann, C., Jacobs, S., & Sofronie-Stokkermans, V. (2010). Automatic Verification of Parametric Specifications with Complex Topologies. In D. Mery, & S. Merz (Eds.), Integrated Formal Methods (pp. 152-167). Berlin: Springer. doi:10.1007/978-3-642-16265-7_12.


Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-14A8-4
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. \begin{itemize} \item For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. \item At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. \item At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. \end{itemize} 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.