Technical, Research Report
@TechReport
Technischer-, Forschungsbericht


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):

Bernd, Becker
Damm, Werner
Fränzle, Martin
Olderog, Ernst-Rüdiger
Podelski, Andreas
Wilhelm, Reinhard

dblp
dblp
dblp
dblp
dblp
dblp

Not MPII Editor(s):

Bernd, Becker
Damm, Werner
Fränzle, Martin
Olderog, Ernst-Rüdiger
Podelski, Andreas
Wilhelm, Reinhard

BibTeX Citekey*:

faber-ihlemann-jacobs-sofronie-2010-report

Language:

English

Title, Institution

Title*:

Automatic Verification of Parametric Specifications with Complex Topologies

Institution*:

Sonderforschungsbereich/Transregio 14 AVACS (Automatic Verification and Analysis of Complex Systems)

Publishers or Institutions Address*:

Saarbrücken

Type:

Technical Report

No, Year, pp.,

Number*:

ATR 66

Pages*:

40

Month:

October

VG Wort
Pages*:


Year*:

2010

ISBN/ISSN:

1860-9821





DOI:




Note, Abstract, ©

Note:


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

Categories / Keywords:


Copyright Message:


HyperLinks / References / URLs:


Personal Comments:


File Upload:


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:
@TECHREPORT{faber-ihlemann-jacobs-sofronie-2010-report,
AUTHOR = {Faber, Johannes and Ihlemann, Carsten and Jacobs, Swen and Sofronie-Stokkermans, Viorica},
EDITOR = {Bernd, Becker and Damm, Werner and Fr{\"a}nzle, Martin and Olderog, Ernst-R{\"u}diger and Podelski, Andreas and Wilhelm, Reinhard},
TITLE = {Automatic Verification of Parametric Specifications with Complex Topologies},
YEAR = {2010},
TYPE = {Technical Report},
INSTITUTION = {Sonderforschungsbereich/Transregio 14 AVACS (Automatic Verification and Analysis of Complex Systems)},
NUMBER = {ATR 66},
PAGES = {40},
ADDRESS = {Saarbr{\"u}cken},
MONTH = {October},
ISBN = {1860-9821},
}


Entry last modified by Anja Becker, 03/15/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
10/06/2010 04:07:08 PM
Revisions
5.
4.
3.
2.
1.
Editor(s)
Anja Becker
Anja Becker
Anja Becker
Anja Becker
Anja Becker
Edit Dates
15.03.2011 09:51:12
15.03.2011 09:50:57
09.03.2011 16:32:38
07.02.2011 10:44:46
10/06/2010 04:09:19 PM
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section