Gesellschaft für Informatik e.V.

Lecture Notes in Informatics

Software Engineering 2013 P-213, 99-112 (2013).

Gesellschaft für Informatik, Bonn

Copyright © Gesellschaft für Informatik, Bonn


Automata-based refinement checking for real-time systems

Christian Brenner , Christian Heinzemann , Wilhelm Schäfer and Stefan Henkler


Model-driven development of real-time safety-critical systems requires to support refinement of behavioral model specifications using, for example, timed simulation or timed bisimulation. Such refinements, if defined properly, guarantee that (safety and liveness) properties, which have been verified for an abstract model, still hold for the refined model. In this paper, we propose an automatic selection algorithm selecting the most suitable refinement definition concerning the type of model specification applied and the properties to be verified. By extending the idea of test automata construction for refinement checking, our approach also guarantees that a refined model is constructed correctly concerning the selected and applied refinement definition. We illustrate the application of our approach by an example of an advanced railway transportation system.

Full Text: PDF

Gesellschaft für Informatik, Bonn
ISBN 978-3-88579-607-7

Last changed 20.02.2014 13:02:19