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