@inproceedings(abdullah-multirate,
 author       = "A. Al-Nayeem and L. Sha and D. D. Cofer and S. M. Miller",
 year         = "2012",
 title        = "Pattern-Based Composition and Analysis of Virtually Synchronized Real-Time Distributed Systems",
 booktitle    = "Proc. ICCPS'12",
 publisher    = "IEEE",
 pages        = "65--74",
 doi          = "10.1109/ICCPS.2012.15",
)
@book(anderson2005introduction,
 author       = "J.D. Anderson",
 year         = "2005",
 title        = "Introduction to flight",
 publisher    = "McGraw-Hill",
)
@unpublished(ftscs12-techrep,
 author       = "K. Bae and J. Krisiloff and J. Meseguer and P. C. {\"O}lveczky",
 year         = "2012",
 title        = "PALS-Based Analysis of an Airplane Multirate Control System in {R}eal-{T}ime {M}aude (Extended Version)",
 note         = "Manuscript available at \url {http://formal.cs.illinois.edu/kbae/airplane/}",
)
@inproceedings(bae-facs12,
 author       = "K. Bae and J. Meseguer and P. C. {\"O}lveczky",
 year         = "2012",
 title        = "Formal Patterns for Multi-Rate Distributed Real-Time Systems",
 booktitle    = "Proc.\ FACS'12",
 series       = "LNCS",
 publisher    = "Springer",
 note         = "To appear",
)
@inproceedings(icfem11,
 author       = "K. Bae and P. C. {\"O}lveczky and A. Al-Nayeem and J. Meseguer",
 year         = "2011",
 title        = "Synchronous {AADL} and its Formal Analysis\tmspace +\thickmuskip {.2777em} in {R}eal-{T}ime {M}aude",
 booktitle    = "Proc.\ ICFEM'11",
 series       = "LNCS",
 volume       = "6991",
 publisher    = "Springer",
 pages        = "651--667",
 doi          = "10.1007/978-3-642-24559-6\_43",
)
@book(maude-book,
 author       = "M. Clavel and F. Dur\'an and S. Eker and P. Lincoln and N. Mart\'\i -Oliet and J. Meseguer and C. Talcott",
 year         = "2007",
 title        = "All About {Maude} -- A High-Performance Logical Framework",
 series       = "LNCS",
 volume       = "4350",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-71999-1",
)
@book(collinson1996introduction,
 author       = "R. P. G. Collinson",
 year         = "1996",
 title        = "Introduction to avionics",
 publisher    = "Chapman \& Hall",
)
@inproceedings(lepri-wrla12,
 author       = "D. Lepri and E. {\'A}brah{\'a}m and P.C. Olveczky",
 year         = "2012",
 title        = "Timed CTL Model Checking in Real-Time Maude",
 booktitle    = "Proc. WRLA'12",
 series       = "LNCS",
 volume       = "7571",
 publisher    = "Springer",
 pages        = "182--200",
 doi          = "10.1007/978-3-642-34005-5\_10",
)
@inproceedings(icfem10,
 author       = "J. Meseguer and P. C. {\"O}lveczky",
 year         = "2010",
 title        = "Formalization and Correctness of the {PALS} Architectural Pattern for Distributed Real-Time Systems",
 booktitle    = "Proc.\ ICFEM'10",
 series       = "LNCS",
 volume       = "6447",
 publisher    = "Springer",
 pages        = "303--320",
 doi          = "10.1007/978-3-642-16901-4\_21",
)
@article(pals-tcs,
 author       = "J. Meseguer and P. C. {\"O}lveczky",
 year         = "2012",
 title        = "Formalization and correctness of the {PALS} architectural pattern for distributed real-time systems",
 journal      = "Theor.\ Comp.\ Sci.",
 volume       = "451",
 pages        = "1--37",
 doi          = "10.1016/j.tcs.2012.05.040",
)
@inproceedings(dasc09,
 author       = "S. P. Miller and D. D. Cofer and L. Sha and J. Meseguer and A. Al-Nayeem",
 year         = "2009",
 title        = "Implementing Logical Synchrony in Integrated Modular Avionics",
 booktitle    = "Proc.\ DASC'09",
 publisher    = "IEEE",
 doi          = "10.1109/DASC.2009.5347579",
)
@article(journ-rtm,
 author       = "P. C. {\"O}lveczky and J. Meseguer",
 year         = "2007",
 title        = "Semantics and Pragmatics of {Real-Time Maude}",
 journal      = "Higher-Order and Symbolic Computation",
 volume       = "20",
 number       = "1-2",
 pages        = "161--196",
 doi          = "10.1007/s10990-007-9001-5",
)
@inproceedings(steiner2011tta,
 author       = "W. Steiner and J. Rushby",
 year         = "2011",
 title        = "TTA and PALS: Formally verified design patterns for distributed cyber-physical systems",
 booktitle    = "Proc. DASC'11",
 organization = "IEEE",
 doi          = "10.1109/DASC.2011.6096120",
)