Location
Toggle navigation
HOME
INSTITUTE
Mission
Address
Executive Board
Scientific Members of MPG
Scientific Advisory Board
Board of Trustees
NEWS
Overview
Press Releases
Awards
Spotlights
Campus Event Calendar
25th Anniversary
Employment
DEPARTMENTS
Algorithms & Complexity
Computer Vision and Machine Learning
Internet Architecture
Computer Grapics
Databases and Information Systems
Visual Computing and Artificial Intelligence
Research Group Computational Biology
Automation of Logic
Network and Cloud Systems
PUBLICATIONS
Algorithms & Complexity
Computer Vision and Machine Learning
Internet Architecture
Computer Graphics
Databases and Information Systems
Visual Computing and Artificial Intelligence
Research Group Computational Biology
Automation of Logic
Network and Cloud Systems
Research Reports
Scientific Advisory Board
Curatorship Board
25th anniversary
IMPRS-CS
PEOPLE
SOFTWARE
SERVICES
Joint Central Services
Joint Administration
- Library
- International Office
Joint Scientific IT and Technical Services
- Building and Technical Support
Research Coordination
Representative for Equal Opportunities
- Equal Opportunities
Representative for Severely Disabled Persons
Representative for Safety
Ombudsperson for
Good Scientific Practice
and Doctoral Research
Company Physician
CS@MPG
CS@SAAR
Saarland Informatics Campus
Computer Science Department,
Saarland University
Max Planck Institute for
Software Systems (MPI-SWS)
German Center for
Artificial Intelligence (DFKI)
Center for Security, Privacy
and Accountability (CISPA)
VIA - Saarbrücken Center for
Visual Computing, Interaction
and Artificial Intelligence
Graduate School for
Computer Science
Cluster of Excellence (MMCI)
Max Planck Center for Visual
Computing and Communication
Kaiserslautern-Saarbrücken
Computer Science Cluster
IT Incubator
Publications
Home
Intranet
Server
halma.mpi-inf.mpg.de
Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop
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
Conference URL::
http://www.iist.unu.edu/ICTAC2006/
Downloading URL:
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
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
Attachment Section
Attachment Section