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:








Author, Editor

Author(s):

Meyer, Roland
Faber, Johannes
Rybalchenko, Andrey

dblp
dblp
dblp

Not MPG Author(s):

Meyer, Roland
Faber, Johannes

Editor(s):

Barkaoui, Kamel
Cavalcanti, Ana
Cerone, Antonio

dblp
dblp
dblp

Not MPII Editor(s):

Barkaoui, Kamel
Cavalcanti, Ana
Cerone, Antonio

BibTeX cite key*:

Rybalchenko2006ICTAC-DC

Title, Booktitle

Title*:

Model checking Duration Calculus: a practical approach

Booktitle*:

Theoretical Aspects of Computing - ICTAC 2006 : Third International Colloquium

Event, URLs

URL of the conference:

http://www.iist.unu.edu/ICTAC2006/

URL for downloading the paper:

http://www.springerlink.com/content/v462n245450349w0/fulltext.pdf

Event Address*:

Tunis, Tunisia

Language:

English

Event Date*
(no longer used):


Organization:

ICTAC

Event Start Date:

18 March 2007

Event End Date:

18 March 2007

Publisher

Name*:

Springer

URL:

http://www.springer.com/

Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Computer Science

Volume:

4281

Number:


Month:


Pages:

332-346

Year*:

2006

VG Wort Pages:

15

ISBN/ISSN:

3-540-48815-4

Sequence Number:


DOI:

10.1007/11921240_23



Note, Abstract, ©


(LaTeX) Abstract:

Model checking of real-time systems with respect to Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. This task is difficult to automate. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to real world applications. Our algorithm significantly extends the subset of DC that can be handled. It decomposes DC specifications into sub-properties that can be verified independently. The decomposition bases on a novel distributive law for DC. We implemented the algorithm as part of our tool chain for the automated verification of systems comprising data, communication, and real-time aspects. Our translation facilitated a successful application of the tool chain on an industrial case study from the European Train Control System (ETCS).

URL for the Abstract:

http://www.springerlink.com/content/v462n245450349w0/?p=43a2aa89b214458b8dab461fbce09615&pi=10



Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Audience:

Expert

Appearance:

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



BibTeX Entry:

@INPROCEEDINGS{Rybalchenko2006ICTAC-DC,
AUTHOR = {Meyer, Roland and Faber, Johannes and Rybalchenko, Andrey},
EDITOR = {Barkaoui, Kamel and Cavalcanti, Ana and Cerone, Antonio},
TITLE = {Model checking Duration Calculus: a practical approach},
BOOKTITLE = {Theoretical Aspects of Computing - ICTAC 2006 : Third International Colloquium},
PUBLISHER = {Springer},
YEAR = {2006},
ORGANIZATION = {ICTAC},
VOLUME = {4281},
PAGES = {332--346},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Tunis, Tunisia},
ISBN = {3-540-48815-4},
DOI = {10.1007/11921240_23},
}


Entry last modified by Uwe Brahm, 01/28/2008
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)
Andrey Rybalchenko
Created
03/18/2007 11:36:38 PM
Revisions
7.
6.
5.
4.
3.
Editor(s)
Uwe Brahm
Uwe Brahm
Uwe Brahm
Christine Kiesel
Christine Kiesel
Edit Dates
2007-07-09 09:46:09
2007-07-09 09:45:45
2007-07-09 09:45:24
28.06.2007 16:11:43
2007-04-26 11:27:47
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section