< Mark Lawford - Research and Publications

Research Interests

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 Software Certification, Formal Methods for Real-Time Systems (synthesis, verification, and model reduction), rigorous, practical, tool supported development processes for software engineering of safety critical systems and Supervisory Control of probabilistic DES, and Hybrid Systems.

Selected Papers and Publications

Click on the download link or where available the title of a paper for a brief abstract and a link to download the full paper.

Nicholas Moore, Mark Lawford, "Correct Safety Critical Hardware Descriptions via Static Analysis and Theorem Proving", Proceedings of the Fifth FME Workshop on Formal Methods in Software Engineering (Formalise '17), LNCS, Springer, 2017 (Accepted for publication) (download)

S Vakili, NK Singh, M Lawford, A Wassyng, B Breimer, "Stop-and-Go Adaptive Cruise Control: A Case Study of Automotive Cyber Physical Systems", In Alexander Romanovsky, Fuyuki Ishikawa (eds), Trustworthy Cyber-Physical Systems Engineering, CRC Press, 2017, 237-270. (download)

K Singh, M Lawford, TSE Maibaum, A Wassyng, "Verifying Trustworthy Cyber-Physical Systems Using Closed-Loop Modeling", In Alexander Romanovsky, Fuyuki Ishikawa (eds), Trustworthy Cyber-Physical Systems Engineering, CRC Press, 2017, 199-236. (download)

K Singh, M Lawford, TSE Maibaum, A Wassyng, "New Standards for Trustworthy Cyber-Physical Systems", In Alexander Romanovsky, Fuyuki Ishikawa (eds), Trustworthy Cyber-Physical Systems Engineering, CRC Press, 2017, 337-367. (download)

Monika Bialy, Vera Pantelic, Jason, Jaskola, Alexander Schaap, Lucian Patcas, Mark Lawford, Alan Wassyng, "Software Engineering for Model Based Design by Domain Experts", In Edward Griffor (editor): Handbook of System Safety and Security: Cyber Risk and Risk Management, Cyber Security, Threat Analysis, Functional Safety, Software Systems, and Cyber Physical Systems, 1st Edition, Elsevier, October 2016, 39-64. (download)

Mark Lawford, "Stupid Tool Tricks for Smart Model Based Design", In S. Blazy and M. Chechik (Eds.): Verified Software. Theories, Tools, and Experiments (VSTTE 2016), LNCS 9971, Springer International Publishing AG, 2016, 1-7. (download)

Joshua Newell, Linna Pang, David Tremaine, Alan Wassyng, Mark Lawford, "Formal Translation of IEC 61131-3 Function Block Diagrams to PVS with Nuclear Application", In NASA Formal Methods: 8th International Symposium, NFM 2016, Minneapolis, MN, USA, LNCS 9690, Springer International Publishing Switzerland, June 7-9, 2016, 206-220. (download)

Archana Mallya, Vera Pantelic, Morayo Adedjouma, Mark Lawford, Alan Wassyng, "Using STPA in an ISO 26262 Compliant Process", In Proceedings of SAFECOMP'2016, LNCS 9922, Springer, 2016, 117-129. (download)

Alan Wassyng, Neeraj Kumar Singh, Mischa Geven, Nicholas Proscia, Hao Wang, Mark Lawford, Tom Maibaum, "Can Product-Specific Assurance Case Templates Be Used as Medical Device Standards?", Design & Test, IEEE, Volume 32, number 5, IEEE, 2015, 45-55. (download)

Neeraj Kumar Singh, Mark Lawford, Tom Maibaum, Alan Wassyng, "Stateflow to Tabular Expressions", In Proceedings of the Sixth International Symposium on Information and Communication Technology, SoICT 2015, Hue City, Viet Nam, ACM, 2015, 312-319. (download)

Linna Pang, Chen-Wei Wang, Mark Lawford, Alan Wassyng, "Formal verification of function blocks applied to IEC 61131-3", Science of Computer Programming, 113, Part 2, 1 December 2015 149 - 190. (download)

Marc Bender, Karen Laurin, Mark Lawford, Vera Pantelic, Alexandre Korobkine, Jeff Ong, Bennett Mackenzie, Monika Bialy, Steven Postma, "Signature required: Making Simulink data flow and interfaces explicit", Science of Computer Programming, Volume 113, Part 1, 1 December 2015, 29 - 50. (download)

Lucian M. Patcas, Mark Lawford, Tom Maibaum, "Implementability of requirements in the four-variable model", Science of Computer Programming, Volume 111, Part 2, 1 November 2015, 339-362. (download)

B. Bilgin, P. Magne, P. Malysz, Yinye Yang, V. Pantelic, M. Preindl, A. Korobkine, Weisheng Jiang, M. Lawford, A. Emadi, "Making the Case for Electrified Transportation," in Transportation Electrification, IEEE Transactions on , vol.1, no.1, June 2015, 4-17. (download)

V. Cassano, S. Grigorova, N.K. Singh, M. Adedjouma, M. Lawford, T. Maibaum, A. Wassyng, "Is Current Incremental Safety Assurance Sound?", In F. Koornneef and C. van Gulijk (eds.), Computer Safety, Reliability, and Security, Lecture Notes in Computer Science, Volume 9338, Springer International Publishing, 2015, 397-408. (download)

Neeraj Kumar Singh, Hao Wang, Mark Lawford, Tom Maibaum, Alan Wassyng, "Stepwise Formal Modelling and Reasoning of Insulin Infusion Pump Requirements", In V.G. Duffy (ed.) Digital Human Modeling. Applications in Health, Safety, Ergonomics and Risk Management: Ergonomics and Health, Lecture Notes in Computer Science, Volume 9185, Springer International Publishing, 2015, 387-398. (download)

Linna Pang, Chen-Wei Wang, Mark Lawford, Alan Wassyng, Josh Newell, Vera Chow, David Tremaine, "Formal Verification of Real-Time Function Blocks Using PVS", 4th International Workshop on Engineering Safety and Security Systems 2015 (ESSS’15) Volume 184, Electronic Proceedings in Theoretical Computer Science, 2015, 65–79. (download)

Monika Bialy, Mark Lawford, Vera Pantelic, Alan Wassyng, "A Methodology for the Simplification of Tabular Designs in Model-based Development", Proceedings of the Third FME Workshop on Formal Methods in Software Engineering (Formalise '15), Florence, Italy, IEEE Press, 2015, 47--53. (download)

Vera Pantelic, Steven Postma, Mark Lawford, Alexandre Korobkine, Bennett Mackenzie, Jeff Ong, Marc Bender, "A Toolset for Simulink: Improving Software Engineering Practices in Development with Simulink," Proceedings of 3rd International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2015), SCITEPRESS, 2015, 50-61. (download) (Best Paper Award)

Lucian M. Patcas, Mark Lawford, Tom Maibaum, "A Separation Principle for Embedded System Interfacing," In E. Albert and E. Sekerinski (Eds.): IFM 2014, LNCS 8739, Springer, 373–388, 2014. (download)

Vera Pantelic, Mark Lawford, Steven Postma, "A Framework for Supervisory Control of Probabilistic Discrete Event Systems," In Proceedings of 12th IFAC - IEEE Workshop on Discrete Event Systems (WODES 2014), École Normale Supérieure de Cachan, France, 14 - 16 May 2014, IFAC/IEEE, 2014, 477-484. (download).

Marc Bender, Karen Laurin, Mark Lawford, Jeff Ong, Steven Postma, Vera Pantelic, "Signature Required - Making Simulink Dataflow and Interfaces Explicit," Proceedings of 2nd International Conference on Model-Driven Engineering and Software Development (MODELSWARD 2014), SCITEPRESS, 2014, 119-131. (Nominated for Best Paper Award) (download)

Linna Pang, Chen-Wei Wang, Mark Lawford, Alan Wassyng, "Formalizing and Verifying Function Blocks using Tabular Expressions and PVS," In Proceedings of FTSCS 2013, Communications in Computer and Information Science, Volume 419, Springer, 2014, 163-178. (Download: paper and Additional files)

Yihai Chen, Mark Lawford, Hao Wang, Alan Wassyng, "Insulin Pump Software Certification," In J. Gibbons and W. MacCaull (Eds.): FHIES 2013, LNCS 8315, Springer-Verlag Berlin Heidelberg, 2014, 87-106. (download)

Lucian Patcas, Mark Lawford, Tom Maibaum, "From System Requirements to Software Requirements in the Four-Variable Model," In Proceedings of the Automated Verification of Critical Systems (AVoCS 2013), Electronic Communications of the EASST, Volume 66, 2014. (download).

Wen Chen, Asif Iqbal, Akbar Abdrakhmanov, Jay Parlar, Chris George, Mark Lawford, Tom Maibaum, Alan Wassyng, "Large-Scale Enterprise Systems: Changes and Impacts," In Enterprise Information Systems, Lecture Notes in Business Information Processing (LNBIP), Volume 141, 2013, 274-290. (download)

Alan Wassyng, Mark Lawford, Tom Maibaum, "Separating Safety and Control Systems to Reduce Complexity," In M. Hinchey and L. Coyle (Eds), Conquering Complexity, Springer London, 2012, 85-102. (download).

Vera Pantelic, Mark Lawford, ``A pseudometric in supervisory control of probabilistic discrete event system,'' Discrete Event Dynamic Systems: Theory and Applications, Vol. 22, No. 4, Springer Netherlands, May 2012, 479-510. (download).

Vera Pantelic, Mark Lawford, ``Optimal Supervisory Control of Probabilistic Discrete Event Systems,'' IEEE Transactions on Automatic Control, Vol. 56, No. 5 May, 2012, 1110-1124. (download).

Wassyng, Alan and Lawford, Mark S. and Maibaum, Thomas S.E., "Software certification experience in the canadian nuclear industry: lessons for the future," In Proceedings of the ninth ACM international conference on Embedded software (EMSOFT '11), Taipei, Taiwan, ACM, 2011, 219--226. (download).

Marc Bender, Tom Maibaum, Mark Lawford and Alan Wassyng, "Positioning Verification in the Context of Software/System Certification", In Proceedings of the 11th International Workshop on Automated Verification of Critical Systems (AVoCS 2011), Electronic Communications of the EASST (European Association of Software Science and Technology), Volume 46, 2013. (15 pages) (download)

C. Eles, M. Lawford, "A tabular expression toolbox for Matlab/Simulink," NASA Formal Methods, Lecture Notes in Computer Science Vol. 6617, Springer, 2011, 494-499 (download).

Alan Wassyng, Tom Maibaum, Mark Lawford and Hans Bherer, ``Software Certification: Is There a Case against Safety Cases?,'' Foundations of Computer Software. Modeling, Development, and Verification of Adaptive Systems, Lecture Notes in Computer Science, Volume 6662, 2011, 206-227 (download).

Alan Wassyng and Mark Lawford, ``Integrated software methodologies - An engineering approach,'' Transactions of the Royal Society of South Africa, Vol. 65, No. 2, October 2010, 125-136 (download).

Vera Pantelic and Mark Lawford, ``Use of a Metric in Supervisory Control of Probabilistic Discrete Event Systems,'' In Proceedings of 10th IFAC Workshop on Discrete Event Systems (WODES 2010), August 30- September 1, 2010, Berlin, Germany, 2010, 227-232 (download).

Alan Wassyng, Tom Maibaum, and Mark Lawford, ``On Software Certification: We Need Product-Focused Approaches, C. Choppy and O. Sokolsky (Eds.): Monterey Workshop 2008, LNCS Vol. 6028, Springer, 2010, 250-274. (download)

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 (download).

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, 85-90. (download)

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, 119-134, 2009. (download)

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, 11-17, 2009. (download)

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 (download)

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. (download)

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, 654-668, Jul. 2006. (download)

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. (download)

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. (download)

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. (download)

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. (download)

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. (download)

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. (download)

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. (download)

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. (download)

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. (download)

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. (download)

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. (download)

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.) (download)

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). (download)

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, 1145-1154. (download)

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 7--88. (download)

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, TP1-13--TP1-17, 2000. (download)

M. Lawford, ``Model Reduction of Discrete Real-Time Systems,'' PhD. Thesis, Dept. of Electrical and Computer Engineering, University of Toronto, January 1997. (download)

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, 263-278. Chapman & Hall, 1996. (download)

M. Lawford and W.M. Wonham, ``Equivalence preserving transformations for timed transition models,'' IEEE Transactions on Automatic Control, vol. 40, no. 7, 1167-1179, 1995. (download)

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, 3642-3648. (download)

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, 327-331. (download)

[ CAS | ML | Papers ]