Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:




Library Locked Library locked




Author, Editor

Author(s):

Faber, Johannes
Ihlemann, Carsten
Jacobs, Swen
Sofronie-Stokkermans, Viorica

dblp
dblp
dblp
dblp

Not MPG Author(s):

Faber, Johannes
Jacobs, Swen

Editor(s):

Mery, Dominique
Merz, Stephan

dblp
dblp

Not MPII Editor(s):

Mery, Dominique
Merz, Stephan

BibTeX cite key*:

faber-ihlemann-jacobs-sofronieStokkermans-ifm-2010

Title, Booktitle

Title*:

Automatic Verification of Parametric Specifications with Complex Topologies

Booktitle*:

Integrated Formal Methods : 8th International Conference, IFM 2010

Event, URLs

URL of the conference:

http://ifm2010.loria.fr/

URL for downloading the paper:

http://dx.doi.org/10.1007/978-3-642-16265-7_12

Event Address*:

Nancy, France

Language:

English

Event Date*
(no longer used):


Organization:


Event Start Date:

11 October 2010

Event End Date:

14 October 2010

Publisher

Name*:

Springer

URL:

http://www.springer-ny.com/

Address*:

Berlin

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Computer Science

Volume:

6396

Number:

-

Month:


Pages:

152-167

Year*:

2010

VG Wort Pages:


ISBN/ISSN:

978-3-642-16264-0

Sequence Number:


DOI:

10.1007/978-3-642-16265-7_12



Note, Abstract, ©


(LaTeX) 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.



Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Automation of Logic

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{faber-ihlemann-jacobs-sofronieStokkermans-ifm-2010,
AUTHOR = {Faber, Johannes and Ihlemann, Carsten and Jacobs, Swen and Sofronie-Stokkermans, Viorica},
EDITOR = {Mery, Dominique and Merz, Stephan},
TITLE = {Automatic Verification of Parametric Specifications with Complex Topologies},
BOOKTITLE = {Integrated Formal Methods : 8th International Conference, IFM 2010},
PUBLISHER = {Springer},
YEAR = {2010},
NUMBER = {-},
VOLUME = {6396},
PAGES = {152--167},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Nancy, France},
ISBN = {978-3-642-16264-0},
DOI = {10.1007/978-3-642-16265-7_12},
}


Entry last modified by Anja Becker, 01/19/2011
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]
Created
08/17/2010 01:32:40 PM
Revisions
2.
1.
0.

Editor(s)
Anja Becker
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans

Edit Dates
19.01.2011 14:32:19
09/02/2010 10:06:19 AM
08/17/2010 01:32:40 PM

Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section