References

  1. (2011): DO-178C: Software Considerations in Airborne Systems and Equipment Certification. Special Committee 205 of RTCA.
  2. 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.
  3. 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.
  4. Xiayong Hu (2008): Proving implementability of timing properties with tolerance. McMaster University, Department of Computing and Software.
  5. 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.
  6. IEC (2003): 61131-3 Ed. 2.0 en:2003: Programmable Controllers — Part 3: Programming Languages. International Electrotechnical Commission.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org