@misc(DO178C,
 year         = {2011},
 title        = {{DO-178C: Software Considerations in Airborne Systems and Equipment Certification}},
 howpublished = {Special Committee 205 of RTCA},
)
@article(so38269,
 author       = {Ed {Brinksma} and Angelika {Mader} and Ansgar {Fehnker}},
 year         = {2002},
 title        = {Verification and optimization of a PLC control schedule},
 journal      = {International Journal on Software Tools for Technology Transfer (STTT)},
 volume       = {4},
 number       = {1},
 pages        = {21--33},
 url          = {http://dx.doi.org/10.1007/s10009-002-0079-0},
)
@article(Ding2013,
 author       = {Zhijun Ding and Changjun Jiang and Mengchu Zhou},
 year         = {2013},
 title        = {Design, Analysis and Verification of Real-Time Systems Based on Time Petri Net Refinement},
 journal      = {ACM Trans. Embed. Comput. Syst.},
 volume       = {12},
 number       = {1},
 pages        = {4:1--4:18},
 url          = {http://dx.doi.org/10.1145/2406336.2406340},
)
@phdthesis(Hu08,
 author       = {Xiayong Hu},
 year         = {2008},
 title        = {Proving implementability of timing properties with tolerance},
 school       = {McMaster University, Department of Computing and Software},
)
@inproceedings(HuLawfordWassyng2008,
 author       = {Xiayong Hu and Mark Lawford and Alan Wassyng},
 year         = {2009},
 title        = {Formal Verification of the Implementability of Timing Requirements},
 booktitle    = {FMICS},
 series       = {{LNCS}},
 volume       = {5596},
 publisher    = {Springer},
 pages        = {119--134},
 url          = {http://dx.doi.org/10.1007/978-3-642-03240-0\_12},
)
@book(IEC:2003:IEP,
 author       = {{IEC}},
 year         = {2003},
 title        = {61131-3 Ed. 2.0 en:2003: Programmable Controllers --- Part 3: Programming Languages},
 publisher    = {International Electrotechnical Commission},
)
@article(Jin2010980,
 author       = {Ying Jin and David Lorge Parnas},
 year         = {2010},
 title        = {Defining The Meaning of Tabular Mathematical Expressions},
 journal      = {Science of Computer Programming},
 volume       = {75},
 number       = {11},
 pages        = {980 -- 1000},
 url          = {http://dx.doi.org/10.1016/j.scico.2009.12.009},
)
@inproceedings(LMFM00,
 author       = {Mark Lawford and Jeff McDougall and Peter Froebel and Greg Moum},
 year         = {2000},
 title        = {Practical application of functional and relational methods for the specification and verification of safety critical software},
 booktitle    = {Proc.\ of AMAST 2000},
 series       = {LNCS},
 volume       = {1816},
 publisher    = {Springer},
 pages        = {73--88},
 url          = {http://dx.doi.org/10.1007/3-540-45499-3\_8},
)
@inproceedings(Owre1992,
 author       = {Sam Owre and John M. Rushby and Natarajan Shankar},
 year         = {1992},
 title        = {{PVS: A Prototype Verification System}},
 booktitle    = {CADE},
 series       = {LNCS},
 volume       = {607},
 pages        = {748--752},
 url          = {http://dx.doi.org/10.1007/3-540-55602-8\_217},
)
@inproceedings(PangWangLawfordWassyng2013,
 author       = {Linna Pang and Chen-Wei Wang and Mark Lawford and Alan Wassyng},
 year         = {2013},
 title        = {{Formalizing and Verifying Function Blocks using Tabular Expressions and PVS}},
 booktitle    = {FTSCS},
 series       = {Communications in Computer and Information Science},
 volume       = {419},
 publisher    = {Spring},
 pages        = {163--178},
 url          = {http://dx.doi.org/10.1007/978-3-319-05416-2\_9},
)
@techreport(PangWangLawfordWassyngTechReport2014,
 author       = {Linna Pang and Chen-Wei Wang and Mark Lawford and Alan Wassyng and Josh Newell and Vera Chow and David Tremaine},
 year         = {2014},
 title        = {{Formal Verification of Real-Time Function Blocks using PVS}},
 type         = {Technical Report},
 number       = {16},
 institution  = {McSCert},
 note         = {\url{https://www.mcscert.ca/index.php/documents/mcscert-reports?view=publication&task=show&id=16}},
)
@article(Parnas:1994:PDW:203102.203107,
 author       = {David Lorge Parnas and Jan Madey and Michal Iglewski},
 year         = {1994},
 title        = {Precise Documentation of Well-Structured Programs},
 journal      = {IEEE Transactions on Software Engineering},
 volume       = {20},
 pages        = {948--976},
 url          = {http://dx.doi.org/10.1109/32.368133},
)
@incollection(shrinktech,
 author       = {Ocan Sankur},
 year         = {2013},
 title        = {Shrinktech: A Tool for the Robustness Analysis of Timed Automata},
 booktitle    = {Computer Aided Verification},
 series       = {{LNCS}},
 volume       = {8044},
 publisher    = {Springer},
 pages        = {1006--1012},
 url          = {http://dx.doi.org/10.1007/978-3-642-39799-8\_72},
)
@inproceedings(WasLaw:2003,
 author       = {Alan Wassyng and Mark Lawford},
 year         = {2003},
 title        = {Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project},
 booktitle    = {FME 2003},
 series       = {LNCS},
 volume       = {2805},
 publisher    = {Springer},
 pages        = {133--153},
 url          = {http://dx.doi.org/10.1007/978-3-540-45236-2\_9},
)
@inproceedings(Wassyng05,
 author       = {Alan Wassyng and Mark Lawford and Xiaoyong Hu},
 year         = {2005},
 title        = {Timing Tolerances in Safety-Critical Software},
 booktitle    = {FM 2005},
 series       = {LNCS},
 volume       = {3582},
 publisher    = {Springer},
 pages        = {157 -- 172},
 url          = {http://dx.doi.org/10.1007/11526841\_12},
)
@incollection(Wijs0213,
 author       = {Anton Wijs and Luc Engelen},
 year         = {2013},
 title        = {Efficient Property Preservation Checking of Model Refinements},
 booktitle    = {TACAS},
 series       = {LNCS},
 volume       = {7795},
 publisher    = {Springer},
 pages        = {565--579},
 url          = {http://dx.doi.org/10.1007/978-3-642-36742-7\_41},
)
@article(Wulf05,
 author       = {Martin De Wulf and Laurent Doyen and Jean-François Raskin},
 year         = {2005},
 title        = {Almost {ASAP} semantics: from timed models to timed implementations},
 journal      = {FAC},
 volume       = {17},
 number       = {3},
 pages        = {319--341},
 url          = {http://dx.doi.org/10.1007/978-3-540-24743-2\_20},
)