@techreport(Banphawatthanarak2000,
 author       = "C. Banphawatthanarak and B. H. Krogh",
 year         = "2000",
 title        = "Verification of stateflow diagrams using smv: sf2smv 2.0",
 type         = "Technical Report",
 number       = "CMU-ECE-2000-020",
 institution  = "Carnegie Mellon University",
)
@incollection(Bostrom2007,
 author       = "P. Bostr\"om et al.",
 year         = "2007",
 title        = "Stepwise Development of Simulink Models Using the Refinement Calculus Framework",
 booktitle    = "ICTAC 2007",
 series       = "LNCS",
 volume       = "4711",
 pages        = "79--93",
 doi          = "10.1007/978-3-540-75292-9\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}6",
)
@(BS2002,
 author       = "{BS EN 61508-3:2002}",
 year         = "2002",
 title        = "Functional safety of electrical/electronic/programmable electronic safety related systems -- {P}art 1: {G}eneral requirements",
)
@article(Caspi2003,
 author       = "P. Caspi et al.",
 year         = "2003",
 title        = "From Simulink to {SCADE/lustre} to {TTA}: a layered approach for distributed embedded applications",
 journal      = "ACM SIGPLAN Notices",
 volume       = "38",
 number       = "7",
 pages        = "153--162",
 doi          = "10.1145/780753.780754",
)
@article(Cavalcanti2011,
 author       = "A. L. C. Cavalcanti et al.",
 year         = "2011",
 title        = "From control law diagrams to Ada via {{\sf \slshape Circus}}",
 journal      = "FAC",
 pages        = "1--48",
 doi          = "10.1007/s00165-010-0170-3",
)
@article(Cavalcanti2003a,
 author       = "A. L. C. Cavalcanti et al.",
 year         = "2003",
 title        = "{A Refinement Strategy for {\sf \textsl {Circus}}}",
 journal      = "FAC",
 volume       = "15",
 number       = "2 - 3",
 pages        = "146--181",
 doi          = "10.1007/s00165-003-0006-5",
)
@inproceedings(Chen2010,
 author       = "C. Chen",
 year         = "2010",
 title        = "Formal Analysis for Stateflow Diagrams",
 booktitle    = "SSIRI-C '10",
 pages        = "102--109",
 doi          = "10.1109/SSIRI-C.2010.29",
)
@article(Dijkstra1975,
 author       = "E. W. Dijkstra",
 year         = "1975",
 title        = "Guarded commands, nondeterminacy and formal derivation of programs",
 journal      = "Commun. ACM",
 volume       = "18",
 number       = "8",
 pages        = "453--457",
 doi          = "10.1145/360933.360975",
)
@(DO178b,
 author       = "{DO-178b}",
 year         = "1992",
 title        = "Software Considerations in Airborne Systems and Equipment Certification",
)
@inproceedings(Hamon2005,
 author       = "G. Hamon",
 year         = "2005",
 title        = "A denotational semantics for {Stateflow}",
 booktitle    = "EMSOFT",
 publisher    = "ACM",
 pages        = "164--172",
 doi          = "10.1145/1086228.1086260",
)
@inproceedings(Hamon2004,
 author       = "G. Hamon and J. Rushby",
 year         = "2004",
 title        = "An Operational Semantics for {Stateflow}",
 booktitle    = "{FASE}",
 series       = "LCNS",
 volume       = "2984",
 publisher    = "Springer-Verlag",
 address      = "Barcelona, Spain",
 pages        = "229--243",
 doi          = "10.1007/s10009-007-0049-7",
)
@article(Harel1987,
 author       = "D. Harel",
 year         = "1987",
 title        = "Statecharts: {A} Visual Formalism for Complex Systems",
 journal      = "SCP",
 volume       = "8",
 number       = "3",
 pages        = "231--274",
 doi          = "10.1016/0167-6423(87)90035-9",
)
@inproceedings(Lublinerman2009,
 author       = "R. Lublinerman et al.",
 year         = "2009",
 title        = "Modular code generation from synchronous block diagrams: modularity vs. code size",
 booktitle    = "POPL' 09",
 publisher    = "ACM",
 pages        = "78--89",
 doi          = "10.1145/1480881.1480893",
)
@misc(Miyazawa2011b,
 author       = "A. Miyazawa and A. L. C. Cavalcanti",
 title        = "{Refinement of the $AbsoluteValue$ chart}",
 note         = "Available at \url {www.cs.york.ac.uk/ alvarohm/refinement}",
)
@techreport(Miyazawa2011,
 author       = "A. Miyazawa and A. L. C. Cavalcanti",
 year         = "2011",
 title        = "{A formal semantics of Stateflow charts}",
 type         = "Technical Report",
 number       = "YCS-2011-461",
 institution  = "{University of York}",
)
@article(Miyazawa2011a,
 author       = "A. Miyazawa and A. L. C. Cavalcanti",
 year         = "2011",
 title        = "{Refinement-oriented models of Stateflow charts}",
 journal      = "SCP",
 note         = "(to appear)",
)
@book(Morgan1994,
 author       = "C. C. Morgan",
 year         = "1994",
 title        = "Programming from Specifications",
 publisher    = "Prentice Hall International Series in Computer Science",
)
@book(Olderog1991,
 author       = "E.-R. Olderog",
 year         = "1991",
 title        = "Nets, terms and formulas: three views of concurrent processes and their relationship",
 publisher    = "Cambridge University Press",
 address      = "New York, NY, USA",
 doi          = "10.1017/CBO9780511526589",
)
@phdthesis(Oliveira2006a,
 author       = "M. V. M. Oliveira",
 year         = "2006",
 title        = "{Formal Derivation of State-Rich Reactive Programs using {\sf \textsl {Circus}}}",
 school       = "{Department of Computer Science - University of York}",
 address      = "UK",
 note         = "YCST-2006-02",
)
@inproceedings(Reeve2006,
 author       = "G. Reeve and S. Reeves",
 year         = "2006",
 title        = "Logic and refinement for charts",
 series       = "ACSC '06",
 address      = "Australia",
 pages        = "13--23",
)
@book(Roscoe1998,
 author       = "A. W. Roscoe",
 year         = "1998",
 title        = "The Theory and Practice of Concurrency",
 series       = "Prentice-Hall Series in Computer Science",
 publisher    = "Prentice-Hall",
 address      = "New York",
 note         = "{Oxford}",
)
@inproceedings(Scaife2004,
 author       = "N. Scaife et al.",
 year         = "2004",
 title        = "Defining and translating a {"}safe{"} subset of simulink/stateflow into lustre",
 booktitle    = "EMSOFT",
 publisher    = "ACM",
 pages        = "259--268",
 doi          = "10.1145/1017753.1017795",
)
@misc(RealTimeWorkshop,
 author       = "{The MathWorks,Inc.}",
 title        = "{Real-Time Workshop}",
 note         = "\url {www.mathworks.co.uk/products}",
)
@misc(Simulink,
 author       = "{The MathWorks,Inc.}",
 title        = "{Simulink}",
 note         = "\url {www.mathworks.co.uk/products}",
)
@misc(Stateflow,
 author       = "{The MathWorks,Inc.}",
 title        = "{Stateflow and Stateflow Coder 7 User's Guide}",
 note         = "\url {www.mathworks.co.uk/products}",
)
@techreport(Tiwari2002,
 author       = "A. Tiwari",
 year         = "2002",
 title        = "Formal semantics and analysis methods for {S}imulink {S}tateflow models",
 type         = "Technical Report",
 institution  = "SRI International",
 note         = "{\tt www.csl.sri.com/\-$\sim $tiwari/\-stateflow.html}",
)
@inproceedings(Toom2008,
 author       = "A. Toom et al.",
 year         = "2008",
 title        = "{G}ene-{A}uto: an {A}utomatic {C}ode {G}enerator for a safe subset of {S}imulink/{S}tateflow and {S}cicos",
 booktitle    = "{ERTS}'08",
)
@inproceedings(Toyn2005,
 author       = "I. Toyn and A. Galloway",
 year         = "2005",
 title        = "{Proving properties of Stateflow models using ISO Standard Z and CADiZ}",
 booktitle    = "ZB-2005, vol. 3455 of LNCS",
 pages        = "104--123",
 doi          = "10.1007/11415787\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}7",
)
@inproceedings(Woodcock2002,
 author       = "J. C. P. Woodcock and A. L. C. Cavalcanti",
 year         = "2002",
 title        = "{The Semantics of {{\sf \slshape Circus}}}",
 booktitle    = "ZB 2002: Formal Specification and Development in Z and B",
 series       = "LCNS",
 volume       = "2272",
 publisher    = "Springer-Verlag",
 pages        = "184--203",
 doi          = "10.1007/3-540-45648-1\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}10",
)
@book(Woodcock1996,
 author       = "J. C. P. Woodcock and J. Davies",
 year         = "1996",
 title        = "Using {Z}: specification, refinement, and proof",
 publisher    = "Prentice-Hall, Inc.",
)