Konferenzbeitrag
Automata-based refinement checking for real-time systems
Lade...
Volltext URI
Dokumententyp
Text/Conference Paper
Dateien
Zusatzinformation
Datum
2013
Zeitschriftentitel
ISSN der Zeitschrift
Bandtitel
Quelle
Verlag
Gesellschaft für Informatik e.V.
Zusammenfassung
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.