@misc(absint,
 title        = "{AbsInt Angewandte Informatik. Worst-Case Execution Time Analyzers}",
)
@misc(af3homepage,
 title        = "The \textsc {AutoFocus}\ensuremath {^3} homepage",
 howpublished = "\url {http://af3.fortiss.org}",
)
@article(verisoft_journal,
 author       = "J. Botaschanjan and M. Broy and A. Gruler and A. Harhurin and S. Knapp and L. Kof and W. Paul and M. Spichkova",
 year         = "2008",
 title        = "{On the Correctness of Upper Layers of Automotive Systems}",
 journal      = "Formal Aspects of Computing (FACS)",
 volume       = "20",
 number       = "6",
 pages        = "637--662",
 doi          = "10.1007/s00165-008-0097-0",
)
@inproceedings(VerisoftAutomotive_FM06,
 author       = "J.\ Botaschanjan and A.\ Gruler and A.\ Harhurin and L.\ Kof and M.\ Spichkova and D.\ Trachtenherz",
 year         = "2006",
 title        = "{Towards Modularized Verification of Distributed Time-Triggered Systems}",
 booktitle    = "{FM} 2006: Formal Methods",
 pages        = "163--178",
 doi          = "10.1007/11813040\_12",
)
@inproceedings(BoKoKuSp05,
 author       = "J. Botaschanjan and L. Kof and C. K{\"u}hnel and M. Spichkova",
 year         = "2005",
 title        = "{Towards Verified Automotive Software}",
 booktitle    = "2nd International ICSE workshop on Software",
 publisher    = "ACM",
 doi          = "10.1145/1082983.1083199",
)
@book(focus,
 author       = "M. Broy and K. St{\o }len",
 year         = "2001",
 title        = "Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement",
 publisher    = "Springer",
)
@article(ptolemy:ieee2003,
 author       = "J. Eker and J. W. Janneck and E. A. Lee and J. Liu and X. Liu and J. Ludvig and S. Neuendorffer and S. Sachs and Y. Xiong",
 year         = "2003",
 title        = "{Taming heterogeneity - the Ptolemy approach}",
 journal      = "Proc. of the IEEE",
 volume       = "91",
 number       = "1",
 pages        = "127--144",
 doi          = "10.1109/JPROC.2002.805829",
)
@techreport(dentum_tb,
 author       = "M. Feilkas and F. H\"olzl and C. Pfaller and S. Rittmann and K. Scheidemann and M. Spichkova and D. Trachtenherz",
 year         = "2009",
 title        = "{A Top-Down Methodology for the Development of Automotive Software}",
 type         = "Tech. Rep.",
 number       = "TUM-I0902",
 institution  = "{TU M{\"u}nchen}",
)
@phdthesis(fleischmann08,
 author       = "A. Fleischmann",
 year         = "2008",
 title        = "Model-based formalization of requirements of embedded automotive systens",
 school       = "TU M{\"u}nchen",
)
@incollection(MSC:Kluwer2003,
 author       = "D. Harel and P. S. Thiagarajan",
 year         = "2003",
 title        = "{Message Sequence Charts}",
 editor       = "L. Lavagno and G. Martin and B. Selic",
 booktitle    = "{UML for Real: Design of Embedded Real-Time Systems}",
 publisher    = "{Kluwer Academic Publishers}",
 pages        = "77--105",
)
@misc(Hofmann_approachesto,
 author       = "C. Hofmann and E. Horn and W. Keller and K. Renzel and M. Schmidt and W. Horn and B. Anger",
 title        = "Approaches to Software Architecture",
)
@techreport(c-code-gen,
 author       = "F. H\"olzl",
 year         = "2009",
 title        = "{The AutoFocus 3 C0 Code Generator}",
 type         = "Tech. Rep.",
 number       = "TUM-I0918",
 institution  = "TU M\"unchen",
)
@book(jackson,
 author       = "M. Jackson",
 year         = "2001",
 title        = "Problem Frames: Analysing and Structuring Software Development Problems",
 publisher    = "Addison-Wesley",
)
@inproceedings(efts_book,
 author       = "C. K{\"u}hnel and M. Spichkova",
 year         = "2007",
 title        = "{Fault-Tolerant Communication for Distributed Embedded Systems}",
 booktitle    = "Software Engineering and Fault Tolerance",
 series       = "Series on Software Engineering and Knowledge Engineering",
)
@phdthesis(Leinenbach:PhD,
 author       = "D. Leinenbach",
 year         = "2008",
 title        = "Compiler Verification in the Context of Pervasive System Verification",
 school       = "Saarland University",
)
@inproceedings(MullerNipkow:TACAS1995,
 author       = "O. M{\"u}ller and T. Nipkow",
 year         = "1995",
 title        = "{Combining Model Checking and Deduction for I/O-Automata}",
 editor       = "Ed Brinksma and R. Cleaveland and K. G. Larsen and T. Margaria and B. Steffen",
 booktitle    = "{TACAS}",
 series       = "{LNCS}",
 volume       = "1019",
 publisher    = "Springer",
 pages        = "1--16",
 doi          = "10.1.1.11.1585",
)
@book(npw,
 author       = "T. Nipkow and L. C. Paulson and M. Wenzel",
 year         = "2002",
 title        = "{Isabelle/HOL -- A Proof Assistant for Higher-Order Logic}",
 series       = "LNCS",
 volume       = "2283",
 publisher    = "Springer",
 doi          = "10.1007/3-540-45949-9",
)
@article(parnas_madey,
 author       = "D. L. Parnas and J. Madey",
 year         = "1995",
 title        = "Functional Documents for Computer Systems",
 journal      = "Science of Computer Programming",
 volume       = "25",
 pages        = "41--61",
 doi          = "10.1016/0167-6423(95)96871-J",
)
@phdthesis(Petrova:phD,
 author       = "E. Petrova",
 year         = "2007",
 title        = "Verification of the {C0} Compiler Implementation on the Source Code Level",
)
@inproceedings(PR99,
 author       = "J. Philipps and B. Rumpe",
 year         = "1999",
 title        = "{Refinement of Pipe-and-Filter Architectures}",
 editor       = "J. M. Wing and J. Woodcock and J. Davies",
 booktitle    = "World Congress on Formal Methods (FM'99)",
 volume       = "LNCS 1708",
 publisher    = "Springer",
 pages        = "96 -- 115",
 doi          = "10.1007/3-540-48119-2\_8",
)
@incollection(Schaetz:Kluwer2004,
 author       = "B. Sch\"atz",
 year         = "2004",
 title        = "{Mastering the Complexity of Reactive Systems: the \textsc {AutoFocus} Approach}",
 booktitle    = "{Formal Methods for Embedded Distributed Systems: How to Master the Complexity}",
 publisher    = "{Kluwer Academic Publishers}",
 pages        = "215--258",
)
@phdthesis(Schirmer:PhD,
 author       = "N. Schirmer",
 year         = "2006",
 title        = "{Verification of Sequential Imperative Programs in {I}sabelle/{HOL}}",
 school       = "TU M\"unchen",
)
@phdthesis(spichkova,
 author       = "M.\ Spichkova",
 year         = "2007",
 title        = "{Specification and Seamless Verification of Embedded Real-Time Systems: FOCUS on Isabelle}",
 school       = "{TU M{\"u}nchen}",
)
@techreport(dentum_focus_tb,
 author       = "M. Spichkova",
 year         = "2010",
 title        = "{From Semiformal Requirements To Formal Specifications via MSCs}",
 type         = "Technical Report",
 number       = "{TUM-I1019}",
 institution  = "{TU M{\"u}nchen}",
)
@article(spichkova_tb_decomp,
 author       = "M. Spichkova",
 year         = "2011",
 title        = "Architecture: Requirements + Decomposition + Refinement",
 journal      = "Softwaretechnik-Trends",
 volume       = "31:4",
)
@techreport(isabelleExport,
 author       = "D. Trachtenherz",
 year         = "2009",
 title        = "{Ausf{\"u}hrungssemantik von AutoFocus-Modellen: Isabelle/HOL-Formalisierung und {\"A}quivalenzbeweis}",
 type         = "Tech. Rep.",
 number       = "TUM-I0903",
 institution  = "{TU M{\"u}nchen}",
)
@inproceedings(2006-01-1222,
 author       = "D. Wild and A. Fleischmann and J. Hartmann and C. Pfaller and M. Rappl and S. Rittmann",
 year         = "2006",
 title        = "{An Architecture-Centric Approach towards the Construction of Dependable Automotive Software}",
 booktitle    = "Proc. of the SAE 2006 World Congress",
 doi          = "10.4271/2006-01-1222",
)