Mark Lawford has industrial experience as a real-time systems verification consultant performing Formal Verification of the Darlington Nuclear Generating Station Shutdown System Trip Computer Software at Ontario Power Generation (formerly Ontario Hydro). He has also worked as a real-time simulator consultant for a Hardware in the Loop (HITL) simulator project at Honeywell (formerly AlliedSignal Aerospace).
His PhD on compositional model reduction of real-time systems was completed under the supervision of Prof. W.M. Wonham at the Systems Control Group in the Department of Electrical and Computer Engineering at the University of Toronto.
He joined the Department of Computing And Software in August 1998 as an Assistant Professor where he has been helping to design and implement the new programs (B.Eng., M.A.Sc. and Ph.D.) in Software Engineering. Since becoming an Associate Professor he has helped create the Mechatronics Engineering B.Eng. and M.Eng. programs. His research interests fall under the general heading of Control of Discrete Event Systems (DES) and in particular Formal Methods for Real-Time Systems (synthesis, verification, and model reduction), Supervisory Control of both nondeterministic and probabilistic DES, and Hybrid Systems.
Click on the title of a paper for a brief abstract and a link to download the full paper.
Vera Pantelic, Steven Postma, and Mark Lawford, ``Probabilistic Supervisory Control of Probabilistic Discrete Event Systems,'' IEEE Transactions on Automatic Control, Vol. 54, No. 8 August, 2009, 2013-2018.
Vera Pantelic and Mark Lawford, ``Towards Optimal Supervisory Control of Probabilistic Discrete Event Systems,'' In Proceedings of 2nd IFAC Workshop on Dependable Control of Discrete Systems (DCDS09), June 10-12, 2009, Bari, Italy, 2009.
Xiayong Hu, Mark Lawford and Alan Wassyng, ``Formal Verification of the Implementability of Timing Requirements,'' In D. Cofer and A. Fantechi (Eds) Proceedings of FMICS 2008: International Workshop on Formal Methods in Industry Critical Systems, LNCS 5596, pp. 119-134, 2009.
John Hatcliff, Mats Heimdahl, Mark Lawford, Tom Maibaum, Alan Wassyng, Fred Wurden, ``A Software Certification Consortium and its Top 9 Hurdles,'' In Proceedings of the First Workshop on Certification of Safety-Critical Software Controlled Systems (SafeCert 2008), Electronic Notes in Theoretical Computer Science, Vol. 238, No. 4, pp. 11-17, 2009.
Peters, D. K., Lawford, M., and Widemann, B. T. ``An IDE for software development using tabular expressions. In Proceedings of the 2007 Conference of the Center For Advanced Studies on Collaborative Research (Richmond Hill, Ontario, Canada, October 22 - 25, 2007). CASCON '07. ACM, New York, NY, 248-251. DOI= http://doi.acm.org/10.1145/1321211.1321238
T. Arbuckle, A. Balaban, D. K. Peters, and M. Lawford. ``Software documents: Comparison and measurement,'' In Proc. 18th Int. Conf. on Software Engineering and Knowledge Engineering, pages 740--745, July 2007.
R.J. Leduc, M. Lawford, and P. Dai, ``Hierarchical Interface-Based Supervisory Control of Flexible Manufacturing System,'' IEEE Transactions on Control Systems Technology, Vol. 14, No. 4, pp. 654-668, Jul. 2006.
V. Pantelic, X. Jin, M. Lawford, and D. Parnas, ``Inspection of concurrent systems:Combining tables, theorem proving and model checking,'' in SERP'06: Proceedings of the International Conf. on Software Engineering Research and Practice, 2, Las Vegas, 2006, 629-635.
M. Lawford, V. Pantelic and H. Zhang, ``Towards Integrated Verification of Timed Transition Models,'' Fundamenta Informaticae, Vol. 70, No. 1-2, January 2006, 155-164.
Alan Wassyng and Mark Lawford, ``Software tools for safety-critical software development'', International Journal on Software Tools for Technology Transfer (STTT), 8(4-5), Springer, 2006, 337-354.
S.E. Bourdon, M. Lawford, and W.M. Wonham, ``Robust Nonblocking Supervisory Control of Discrete Event Systems,'' IEEE Transactions on Automatic Control, Vol. 50, No. 12 December, 2005, 2015-2020.
R.J. Leduc, B.A. Brandin, M. Lawford, and W.M. Wonham, ``Hierarchical Interface-based Supervisory Control Part I: Serial Case,'' IEEE Transactions on Automatic Control, Vol. 50, No. 9 September, 2005, 1322-1335.
R.J. Leduc, M. Lawford, and W.M. Wonham, ``Hierarchical Interface-based Supervisory Control Part II: Parallel Case,'' IEEE Transactions on Automatic Control, Vol. 50, No. 9 September, 2005, 1336-1348.
A. Wassyng, M. Lawford and X. Hu, ``Timing Tolerances in Safety-Critical Software,'' In J. Fitzgerald, I.J. Hayes, and A. Tarlecki, eds. FM 2005: Formal Methods: International Symposium of Formal Methods Europe Proceedings, Newcastle, UK, LNCS Vol. 3582, Springer-Verlag, July, 2005, 157-172.
S. Postma and M. Lawford, ``Computation of Probabilistic Supervisory Controllers for Model Matching,'' In Venu Veeravalli and Geir Dullerud, eds., Proceedings of the 42nd Annual Allerton Conference on Communication, Control, and Computing, Monticello, Illinois, Oct., 2004.
M. Lawford and H. Zhang, ``Equivalence Verification of Timed Transition Models,'' In 4th International Conference on Application of Concurrency to System Design (ACSD 2004) Proceedings, Hamilton, ON, Canada, IEEE Computer Society, June 2004, 155-164.
A. Wassyng and M. Lawford, ``Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project,'' In K. Arakai, S. Gnesi, and D. Mandrioli, eds. FME 2003: International Symposium of Formal Methods Europe Proceedings, Pisa, Italy, LNCS Vol. 2805, Springer-Verlag, September 2003, 133-153.
D.L. Parnas and M. Lawford, ``The Role of Inspection in Software Quality Assurance,'' Guest Editor's Introduction, IEEE Transactions on Software Engineering, Vol. 29, No. 8, August 2003, 674-676.
D.L. Parnas and M. Lawford, ``Inspection's Role in Software Quality Assurance,'' Guest Editor's Introduction, IEEE Software, Vol. 20, No. 4, July/August 2003, 16-20. (NOTE: Mostly identical contents to the above IEEE TSE article due to nature of joint special issues on Software Inspection.)
M. Lawford and D.L. Parnas (Editors), WISE'01: Proceedings of the 1st Workshop on Inspection in Software Engineering, Paris, France, Software Quality Research Lab, McMaster University, Hamilton, Canada, July 23, 2001, 162 pages. Also available online at http://www.cas.mcmaster.ca/wise/wise01.
M. Lawford, P. Froebel, and G. Moum, ``Application of Tabular Methods to the Specification and Verification of a Nuclear Reactor Shutdown System,'' Submitted to Formal Methods in System Design (Accepted subject to minor revision June 2004).
S.E. Bourdon, W.M. Wonham, and M. Lawford, ``Invariance Under Scaling of Time Bounds in Timed Discrete-Event Systems,'' In R.S. Sreenivas and D.L. Jones, eds., Proceedings of the 38th Annual Allerton Conference on Communication, Control, and Computing, Vol. 2, Monticello, Illinois, Oct., 2000, pp. 1145-1154.
M. Lawford, J. McDougall, P. Froebel and G. Moum ``Practical application of functional and relational methods for the specification and verification of safety critical software,'' In T. Rus, editor, Proceedings of Algebraic Methodology and Software Technology, 8th International Conference, AMAST 2000, LNCS 1816, Springer, Iowa City, Iowa, USA, May 2000, pp. 7--88.
M. Lawford and H. Wu, ``Verification of Real-Time Control Software Using PVS,'' In P. Ramadge and S. Verdu, eds., Proceedings of the 2000 Conference on Information Sciences and Systems, vol. 2, Dept. of Electrical Engineering, Princeton University, Princeton, NJ, pp. TP1-13--TP1-17, 2000.
M. Lawford, ``Model Reduction of Discrete Real-Time Systems,'' PhD. Thesis, Dept. of Electrical and Computer Engineering, University of Toronto, January 1997.
M. Lawford, J.S. Ostroff, and W.M. Wonham, ``Model reduction of modules for state-event temporal logics,'' In R. Gotzhein and J. Bredereke, eds., Formal Description Techniques IX: Theory, application and tools, Proceedings of FORTE/PSTV'96, pp. 263-278. Chapman & Hall, 1996.
M. Lawford and W.M. Wonham, ``Equivalence preserving transformations for timed transition models,'' IEEE Transactions on Automatic Control, vol. 40, no. 7, pp. 1167-1179, 1995.
M. Lawford, W.M. Wonham, and J.S. Ostroff, ``State-event observers for labeled transition systems,'' in Proc. of the 33rd IEEE Conference on Decision and Control, Orlando, FL, Dec. 1994, pp. 3642-3648.
M. Lawford and W.M. Wonham, ``Supervisory control of probabilistic discrete event systems,'' in Proc. of the 36th IEEE Midwest Symposium on Circuits and Systems, Detroit, MI, Aug. 1993, pp. 327-331.