@INPROCEEDINGS{Faber2009,
   AUTHOR = {J. Faber},
   TITLE = {Verification Architectures for Real-time Systems},
   BOOKTITLE = {Proceedings of Formal Methods 2009 Doctoral Symposium},
   YEAR = {2009},
   EDITOR = {M. Mousavi and E. Sekerinski},
   NUMBER = {09-15},
   SERIES = {CS-Report, Eindhoven University of Technology},
   PAGES = {14--19},
   URL = {http://alexandria.tue.nl/repository/books/654108.pdf },
   INSTITUTION = {Eindhoven University of Technology},
   TYPE = {CS-Report},
   subproject={R1},
   access={open},
   bibtex={faber.fmds09.bib},
   pdf={faber.fmds09.pdf},
   abstract={We introduce a new conceptual approach of Verification Architectures that uses 
             formally defined design patterns for complex real-time systems to facilitate 
             decomposional verification of large systems. To this end, we provide an extension 
             of CSP by data and undefined processes that allow us to specify Verification 
             Architectures, i.e., abstract protocols with additional local assumptions in a 
             real-time logic. We embedded our CSP extension into dynamic logic and define a 
             sequent calculus to prove desired properties of those protocols. With a case study 
             from the railway domain, we show that a Verification Architecture proven correct 
             with our calculus helps us verify large systems decompositionally that are too 
             complex for direct verification.},
}