@inproceedings(musab-fase09,
 author       = "M. AlTurki and D. Dhurjati and D. Yu and A. Chander and H. Inamura",
 year         = "2009",
 title        = "Formal Specification and Analysis of Timing Properties in Software Systems",
 booktitle    = "FASE'09",
 series       = "Lecture Notes in Computer Science",
 volume       = "5503",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-00593-0\_18",
)
@article(timedautomata,
 author       = "R. Alur and D. L. Dill",
 year         = "1994",
 title        = "A theory of timed automata",
 journal      = "Theoretical Computer Science",
 volume       = "126",
 number       = "2",
 pages        = "183--235",
 doi          = "10.1016/0304-3975(94)90010-8",
)
@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 in {R}eal-{T}ime {M}aude",
 booktitle    = "Proc.\ ICFEM'11",
 series       = "Lecture Notes in Computer Science",
 note         = "To appear",
)
@article(ptolemy-journal,
 author       = "K. Bae and P. C. {\"O}lveczky and T. H. Feng and E. A. Lee and S. Tripakis",
 year         = "2011",
 title        = "Verifying hierarchical {Ptolemy II} discrete-event models using {Real-Time Maude}",
 journal      = "Science of Computer Programming",
 doi          = "10.1016/j.scico.2010.10.002",
 note         = "To appear",
)
@inproceedings(boronat-heckel-meseguer-fase09,
 author       = "A. Boronat and R. Heckel and J. Meseguer",
 year         = "2009",
 title        = "Rewriting Logic Semantics and Verification of Model Transformations",
 booktitle    = "Proc.\ FASE'09",
 series       = "Lecture Notes in Computer Science",
 volume       = "5503",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-00593-0\_2",
)
@inproceedings(boronat-meseguer-fase08,
 author       = "A. Boronat and J. Meseguer",
 year         = "2008",
 title        = "An Algebraic Semantics for {MOF}",
 booktitle    = "Proc.\ FASE'08",
 series       = "Lecture Notes in Computer Science",
 volume       = "4961",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-78743-3\_28",
)
@inproceedings(boronat-meseguer-tools09,
 author       = "A. Boronat and J. Meseguer",
 year         = "2009",
 title        = "Algebraic Semantics of {OCL}-Constrained Metamodel Specifications",
 booktitle    = "TOOLS-EUROPE'09",
 series       = "LNBIP",
 volume       = "33",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-02571-6\_7",
)
@inproceedings(fase10,
 author       = "A. Boronat and P. C. {\"O}lveczky",
 year         = "2010",
 title        = "Formal Real-Time Model Transformations in {MOMENT2}",
 booktitle    = "Proc.\ FASE'10",
 series       = "Lecture Notes in Computer Science",
 volume       = "6013",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-12029-9",
)
@article(timedPetri,
 author       = "A. Cerone and A. Maggiolo-Schettini",
 year         = "1999",
 title        = "Time-Based Expressivity of Time {P}etri Nets for System Specification",
 journal      = "Theoretical Computer Science",
 volume       = "216",
 number       = "1-2",
 pages        = "1--53",
 doi          = "10.1016/S0304-3975(98)00008-5",
)
@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       = "Lecture Notes in Computer Science",
 volume       = "4350",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-71999-1",
)
@article(ptolemy,
 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      = "Proceedings of the IEEE",
 volume       = "91",
 number       = "2",
 pages        = "127--144",
 doi          = "10.1109/JPROC.2002.805829",
)
@misc(erlang,
 title        = "{Erlang} home page",
 howpublished = "\url {http://www.erlang.org/}",
)
@inproceedings(mike-wsn,
 author       = "M. Katelman and J. Meseguer and J. Hou",
 year         = "2008",
 title        = "Redesign of the {LMST} Wireless Sensor Protocol through Formal Modeling and Statistical Model Checking",
 booktitle    = "Proc.\ FMOODS'08",
 series       = "Lecture Notes in Computer Science",
 volume       = "5051",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-68863-1\_10",
)
@misc(lepri-tctl,
 author       = "D. Lepri and P. C. {\"O}lveczky and E. \'Abrah\'am",
 title        = "Timed {CTL} Model Checking in {Real-Time Maude}",
 howpublished = "Submitted for publication",
)
@inproceedings(norm-paper,
 author       = "E. Lien and P. C. {\"O}lveczky",
 year         = "2009",
 title        = "Formal Modeling and Analysis of an {IETF} Multicast Protocol",
 booktitle    = "Proc.\ SEFM'09",
 publisher    = "IEEE Computer Society",
 doi          = "10.1109/SEFM.2009.11",
)
@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       = "Lecture Notes in Computer Science",
 volume       = "6447",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-16901-4\_21",
)
@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",
)
@inproceedings(phuket08,
 author       = "P. C. {\"O}lveczky",
 year         = "2008",
 title        = "Towards Formal Modeling and Analysis of Networks of Embedded Medical Devices in {Real-Time Maude}",
 booktitle    = "Proc.\ SNPD'08",
 publisher    = "IEEE",
 doi          = "10.1109/SNPD.2008.42",
)
@inproceedings(fmoods10,
 author       = "P. C. {\"O}lveczky and A. Boronat and J. Meseguer",
 year         = "2010",
 title        = "Formal Semantics and Analysis of Behavioral {AADL} Models in {R}eal-{T}ime {M}aude",
 booktitle    = "Proc.\ FMOODS/FORTE'10",
 series       = "Lecture Notes in Computer Science",
 volume       = "6117",
 publisher    = "Springer",
 pages        = "47--62",
 doi          = "10.1007/978-3-642-13464-7\_5",
)
@unpublished(aadl-techrep,
 author       = "P. C. {\"O}lveczky and A. Boronat and J. Meseguer and E. Pek",
 year         = "2010",
 title        = "Formal Semantics and Analysis of Behavioral {AADL} Models in {R}eal-{T}ime {M}aude",
 note         = "Report, \url {http://www.ifi.uio.no/RealTimeMaude/AADL/}",
)
@inproceedings(fase06,
 author       = "P. C. {\"O}lveczky and M. Caccamo",
 year         = "2006",
 title        = "Formal Simulation and Analysis of the {CASH} Scheduling Algorithm in {R}eal-{T}ime {M}aude",
 booktitle    = "Proc.\ FASE'06",
 series       = "Lecture Notes in Computer Science",
 volume       = "3922",
 publisher    = "Springer",
 doi          = "10.1007/11693017\_26",
)
@inproceedings(tacas08,
 author       = "P. C. {\"O}lveczky and J. Meseguer",
 year         = "2008",
 title        = "The {R}eal-{T}ime {M}aude Tool",
 booktitle    = "Proc.\ TACAS'08",
 series       = "Lecture Notes in Computer Science",
 volume       = "4963",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-78800-3\_23",
)
@article(aer-journ,
 author       = "P. C. {\"O}lveczky and J. Meseguer and C. L. Talcott",
 year         = "2006",
 title        = "Specification and Analysis of the {AER/NCA} Active Network Protocol Suite in {R}eal-{T}ime {M}aude",
 journal      = "Formal Methods in System Design",
 volume       = "29",
 number       = "3",
 pages        = "253--293",
 doi          = "10.1007/s10703-006-0015-0",
)
@article(ogdc-tcs,
 author       = "P. C. {\"O}lveczky and S. Thorvaldsen",
 year         = "2009",
 title        = "Formal Modeling, Performance Estimation, and Model Checking of Wireless Sensor Network Algorithms in {R}eal-{T}ime {M}aude",
 journal      = "Theoretical Computer Science",
 volume       = "410",
 number       = "2-3",
 pages        = "254--280",
 doi          = "10.1016/j.tcs.2008.09.022",
)
@phdthesis(rivera-thesis,
 author       = "J. E. Rivera",
 year         = "2010",
 title        = "On the Semantics of Real-Time Domain Specific Modeling Languages",
 school       = "Universidad de M\'alaga",
)
@inproceedings(emotions,
 author       = "J. E. Rivera and F. Dur{\'a}n and A. Vallecillo",
 year         = "2010",
 title        = "On the Behavioral Semantics of Real-Time Domain Specific Visual Languages",
 booktitle    = "Proc.\ WRLA'10",
 series       = "Lecture Notes in Computer Science",
 volume       = "6381",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-16310-4\_12",
 note         = "See also the e-Motions web page \url {http://atenea.lcc.uma.es/index.php/Main_Page/Resources/E-motions}",
)
@misc(aadl,
 author       = "{SAE AADL Team}",
 year         = "2009",
 title        = "{AADL} Homepage",
 note         = "\url {http://www.aadl.info/}",
)
@inproceedings(srba,
 author       = "J. Srba",
 year         = "2008",
 title        = "Comparing the Expressiveness of Timed Automata and Timed Extensions of {P}etri Nets",
 booktitle    = "Proc.\ FORMATS'08",
 series       = "Lecture Notes in Computer Science",
 volume       = "5215",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-85778-5\_3",
)
@article(farn-wang-survey,
 author       = "F. Wang",
 year         = "2004",
 title        = "Formal Verification of Timed Systems: A Survey and Perspective",
 journal      = "Proceedings of the IEEE",
 volume       = "92",
 number       = "8",
 pages        = "1283--1307",
 doi          = "10.1109/JPROC.2004.831197",
)