English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 Local TagsRelease HistoryDetailsSummary
  Model checking Duration Calculus: a practical approach

Meyer, R., Faber, J., & Rybalchenko, A. (2006). Model checking Duration Calculus: a practical approach. In Theoretical Aspects of Computing - ICTAC 2006, Third International Colloquium (pp. 332-346). Berlin, Germany: Springer.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-236E-F Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-2370-7
Genre: Conference Paper

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Meyer, Roland, Author
Faber, Johannes1, Author           
Rybalchenko, Andrey1, Author           
Barkaoui, Kamel, Editor
Cavalcanti, Ana, Editor
Cerone, Antonio, Editor
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 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).

Details

show
hide
Language(s): eng - English
 Dates: 2007-04-262006
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 314630
Other: Local-ID: C1256104005ECAFC-EEC1D2A3E8A4DEA9C12572A2007C343E-Rybalchenko2006ICTAC-DC
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: Tunis, Tunisia
Start-/End Date: 2006-11-20

Legal Case

show

Project information

show

Source 1

show
hide
Title: Theoretical Aspects of Computing - ICTAC 2006, Third International Colloquium
Source Genre: Proceedings
 Creator(s):
Affiliations:
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 332 - 346 Identifier: ISBN: 3-540-48815-4

Source 2

show
hide
Title: Lecture Notes in Computer Science
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 4281 Sequence Number: - Start / End Page: - Identifier: -