@book(abrial:96,
 author       = "J-R. Abrial",
 year         = "1996",
 title        = "{The {B}-Book: Assigning Programs to Meanings}",
 publisher    = "Cambridge University Press",
 doi          = "10.1017/CBO9780511624162",
)
@book(abrial:10,
 author       = "J-R. Abrial",
 year         = "2010",
 title        = "{Modeling in Event-B: System and Software Engineering}",
 publisher    = "Cambridge University Press",
)
@book(ahmed:06,
 author       = "N. Ahmed",
 year         = "2006",
 title        = "Dynamic Systems and Control With Applications",
 publisher    = "World Scientific",
)
@inproceedings(AlCouHenHo:93,
 author       = "R. Alur and C. Courcoubetis and T. Henzinger and P-H. Ho",
 year         = "1993",
 title        = "{Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems}",
 booktitle    = "Proc. Workshop on Theory of Hybrid Systems",
 series       = "LNCS",
 volume       = "736",
 publisher    = "Springer",
 pages        = "209--229",
)
@article(AlurDill:94,
 author       = "R. Alur and D. Dill",
 year         = "1994",
 title        = "{A Theory of Timed Automata}",
 journal      = "Theor. Comp. Sci.",
 volume       = "126",
 pages        = "183--235",
 doi          = "10.1016/0304-3975(94)90010-8",
)
@book(Ants:06,
 author       = "P. Antsaklis and A. Michel",
 year         = "2006",
 title        = "Linear Systems",
 publisher    = "Birkhauser",
)
@article(Ban:09a,
 author       = "R. Banach",
 title        = "{Model Based Refinement and the Design of Retrenchments.}",
 note         = "Available from \cite {RET}.",
)
@article(BaJe:09,
 author       = "R. Banach and C. Jeske",
 title        = "{Retrenchment and Refinement Interworking: the Tower Theorems.}",
 note         = "Submitted",
)
@article(BJP:08,
 author       = "R. Banach and C. Jeske and M. Poppleton",
 year         = "2008",
 title        = "{C}omposition {M}echanisms for {R}etrenchment",
 journal      = "J. Log. Alg. Prog.",
 volume       = "75",
 pages        = "209--229",
 doi          = "10.1016/j.jlap.2007.11.001",
)
@article(BPJS:07a,
 author       = "R. Banach and M. Poppleton and C. Jeske and S. Stepney",
 year         = "2007",
 title        = "{E}ngineering and {T}heoretical {U}nderpinnings of {R}etrenchment",
 journal      = "Sci. Comp. Prog.",
 volume       = "67",
 pages        = "301--329",
 doi          = "10.1016/j.scico.2007.04.002",
)
@book(barnett:75,
 author       = "S. Barnett",
 year         = "1975",
 title        = "Introduction to Mathematical Control Theory",
 publisher    = "Oxford University Press",
)
@article(Boerger-ASMref03,
 author       = "E. B{\"o}rger",
 year         = "2003",
 title        = "{The ASM Refinement Method}",
 journal      = "{F.A.C.J.}",
 volume       = "15",
 pages        = "237--257",
)
@book(ASM,
 author       = "E. B{\"o}rger and R.F. St{\"a}rk",
 year         = "2003",
 title        = "Abstract State Machines. A Method for High Level System Design and Analysis",
 publisher    = "Springer",
)
@book(clarke:87,
 author       = "F. Clarke",
 year         = "1987",
 title        = "Optimization and Nonsmooth Analysis",
 publisher    = "Society for Industrial Mathematics",
)
@book(clarke:97,
 author       = "F. Clarke and Y. Ledyaev and R. Stern and P. Wolenski",
 year         = "1997",
 title        = "Nonsmooth Analysis and Control Theory",
 publisher    = "Springer",
)
@techreport(CoSl:08,
 author       = "J. Cohen and A. Slissenko",
 year         = "2008",
 title        = "Implementation of Timed Abstract State Machines with Instantaneous Actions by Machines with Delays",
 type         = "Technical Report",
 number       = "TR-LACL-2008-2",
 institution  = "LACL, University of Paris-12",
)
@inproceedings(COR:95,
 author       = "J. Crow and S. Owre and J. Rushby and N. Shankar and M. Srivas",
 year         = "1995",
 title        = "{A Tutorial Introduction to PVS}",
 editor       = "R. France and S. Gerhart and M. Larrondo-Petrie",
 booktitle    = "WIFT'95: Workshop on Industrial-Strength Formal Specification Techniques",
 publisher    = "IEEE Computer Society Press",
)
@book(DadHou:95,
 author       = "J. D'Azzo and C. Houpis",
 year         = "1995",
 title        = "Linear Control System Analysis and Design: Conventional and Modern",
 publisher    = "McGraw Hill",
)
@book(boiten:01,
 author       = "J Derrick and E Boiten",
 year         = "2001",
 title        = "{Refinement in {Z} and Object-{Z}: Foundations and Advanced Applications}",
 publisher    = "Springer-Verlag UK",
 doi          = "10.1007/978-1-4471-0257-1",
)
@book(DorBish:10,
 author       = "R. Dorf and R. Bishop",
 year         = "2010",
 title        = "Modern Control Systems",
 publisher    = "Pearson",
)
@inproceedings(Dut:96,
 author       = "B. Dutertre",
 year         = "1996",
 title        = "Elements of Mathematical Analysis in {PVS}",
 booktitle    = "TPHOLS 1996",
 series       = "LNCS",
 volume       = "1125",
 publisher    = "Springer",
)
@book(DutThBa:97,
 author       = "K. Dutton and S. Thompson and B. Barraclough",
 year         = "1997",
 title        = "The Art of Control Engineering",
 publisher    = "Addison Wesley",
)
@book(FaVi:09,
 author       = "M. Fadali and A. Visioli",
 year         = "2009",
 title        = "Digital Control Engineering: Analysis and Design",
 publisher    = "Academic Press",
)
@book(FrPoWo:98,
 author       = "G. Franklin and J. Powell and M. Workman",
 year         = "1996",
 title        = "Digital Control Systems",
 publisher    = "Prentice Hall",
)
@inproceedings(He:94,
 author       = "J. He",
 year         = "1994",
 title        = "{From CSP to hybrid systems}",
 editor       = "A.W. Roscoe",
 booktitle    = "A Classical Mind, Essays in Honour of C.A.R. Hoare",
 publisher    = "Prentice-Hall International",
 pages        = "171--189",
)
@inproceedings(Henz:06,
 author       = "T. A. Henzinger",
 year         = "1996",
 title        = "{The Theory of Hybrid Automata}",
 booktitle    = "Proc. IEEE LICS-96",
 publisher    = "IEEE",
 pages        = "278--292",
 note         = "{See also \url {http://mtc.epfl.ch/ tah/Publications/the\_theory\_of_hybrid_automata.pdf}}",
)
@misc(CBTC,
 author       = "{IEEE Standard 1474}",
 note         = "IEEE Standard for Communications-Based Train Control (CBTC) Performance and Functional Requirements: IEEE Std 1474.1-2004; IEEE Standard for User Interface Requirements in Communications-Based Train Control (CBTC) Systems: IEEE Std 1474.2-2003; IEEE Recommended Practice for Communications-Based Train Control (CBTC) System Design and Functional Allocations: IEEE Std 1474.3-2008",
)
@phdthesis(Jes:05,
 author       = "C. Jeske",
 year         = "2005",
 title        = "Algebraic Integration of Retrenchment and Refinement",
 school       = "University of Manchester",
)
@book(Kuo:92,
 author       = "B. Kuo",
 year         = "1992",
 title        = "Digital Control Systems",
 publisher    = "Oxford University Press",
)
@book(KAOS,
 author       = "A. van Lamsweerde",
 year         = "2009",
 title        = "{Requirements Engineering: From System Goals to UML Models to Software Specifications}",
 publisher    = "Wiley",
)
@phdthesis(Let:01,
 author       = "{Letier, E.}",
 year         = "2001",
 title        = "{Reasoning about Agents in Goal-Oriented Requirements Engineering}",
 school       = "{D\'{e}pt. Ing\'{e}nierie Informatique, Universit\'{e} Catholique de Louvain}",
)
@book(Ogata:08,
 author       = "K. Ogata",
 year         = "2008",
 title        = "Modern Control Engineering",
 publisher    = "Pearson",
)
@book(Para:96,
 author       = "P. Paraskevopoulos",
 year         = "1996",
 title        = "Digital Control Systems",
 publisher    = "Prentice Hall",
)
@book(potter:96,
 author       = "B Potter and J Sinclair and D Till",
 year         = "1996",
 title        = "{An Introduction to Formal Specification and Z}",
 edition      = "2nd.",
 publisher    = "Prentice Hall",
)
@misc(PVS,
 author       = "{PVS Homepage}",
 note         = "\url {http://pvs.csl.sri.com}",
)
@article(RET,
 author       = "{Retrenchment Homepage}",
 note         = "\url {http://www.cs.man.ac.uk/retrenchment}",
)
@book(roever:98,
 author       = "W P de Roever and K Engelhardt",
 year         = "1998",
 title        = "Data Refinement: Model-Oriented Proof Methods and their Comparison",
 publisher    = "Cambridge University Press",
)
@book(sekerinski:98,
 author       = "E Sekerinski and K Sere",
 year         = "1998",
 title        = "{Program Development by Refinement: Case Studies Using the {B}-Method}",
 publisher    = "Springer",
)
@article(SlVa:08,
 author       = "A. Slissenko and P. Vasilyev",
 year         = "2008",
 title        = "{Simulation of Timed Abstract State Machines with Predicate Logic model Checking}",
 journal      = "J.U.C.S.",
 volume       = "14",
 pages        = "1984--2006",
)
@book(sontag:98,
 author       = "E. Sontag",
 year         = "1998",
 title        = "Mathematical Control Theory",
 publisher    = "Springer",
)
@inproceedings(Su:11,
 author       = "W. Su and F. Yang and X. Wu and J. Gou and H. Zhu",
 year         = "2011",
 title        = "{Formal Approaches to Mode Conversion and Positioning for Vehicle Systems}",
 booktitle    = "{Proc. 3rd IEEE International Workshop on Security Aspects of Process and Services Engineering}",
 note         = "To appear",
)
@book(Tab:09,
 author       = "P. Tabuada",
 year         = "2009",
 title        = "Verification and Control of Hybrid Systems: A Symbolic Approach",
 publisher    = "Springer",
)
@book(woodcock:96,
 author       = "J Woodcock and J Davies",
 year         = "1996",
 title        = "{Using Z, Specification, Refinement and Proof}",
 publisher    = "Prentice Hall",
)