Overview
Background
Associate Professor Graeme Smith has over 100 publications in the area of formal, i.e., mathematically based, design and analysis of software and software-based systems. His seminal work on formal object-oriented modelling has found application in the telecommunications and railways sectors, and that on real-time embedded systems in the Defence sector. He has worked at the Software Verification Research Centre (Australia), GMD First (Germany), the Technical University of Berlin (Germany), and the Centre de Recherche en Informatique de Nancy (France). Since his current appointment at The University of Queensland, he has led 3 ARC Discovery Grants on formal design and analysis of fault-tolerant systems, distributed autonomous systems, and lock-free concurrent algorithms, respectively. He currently leads a research cell of the Defence Science and Technology Group focussed on formal security analysis of concurrent code.
Availability
- Associate Professor Graeme Smith is:
- Available for supervision
- Media expert
Fields of research
Qualifications
- Bachelor (Honours) of Engineering, The University of Queensland
- Doctor of Philosophy, The University of Queensland
Research interests
-
Formal Methods
Formal, i.e., mathematically based, design and analysis of software and software-based systems. Primary expertise lies in the application of formal techniques to functional correctness and security of concurrent programs. In particular, techniques based on refinement for functional correctness, and information flow for security. Secondary expertise lies in the formal design and analysis of component-based systems, including highly distributed systems such as self-organising and multi-agent systems, and object-oriented programs where expertise extends to formal refactoring techniques for improving object-oriented designs.
Research impacts
Associate Professor Graeme Smith’s research has had the following impact outside of academia:
His research on formal obejct-oriented modelling has been used
-
to specify and verify the design of a fault-tolerant telecommunications platform for the Overseas Telecommunications Corporation, Australia, in 1989
-
in business process specifications at Bellcore, New Jersey, USA, in 1994
-
in the description of the ISO standard, PREMO (Presentation Environments for Multimedia Objects) in 1994
-
in software engineering projects at Motorola, Arizona, USA, in 1999
-
in a Queensland Rail project for documenting design specifications for interlocking systems in 2003
His research into modelling continuous, real-time systems was used to improve the quality of the documentation of requirements for the flight control unit of the Nulka Active Missile Decoy being developed by BAE Systems, Australia, in 2000.
His ARC Discovery Grant research on fault-tolerant systems was adopted by the Defence Signals Directorate, Australia, for verifying a fault-tolerant security device in 2007.
His ARC Discovery Grant research on model checking concurrent objects was the subject of a joint patent application with Oracle Labs, Australia, in 2016.
Works
Search Professor Graeme Smith’s works on UQ eSpace
2008
Journal Article
Preface
Boiten, Eerke, Derrick, John and Smith, Graeme (2008). Preface. Electronic Notes in Theoretical Computer Science, 201 (C), 1. doi: 10.1016/j.entcs.2008.02.012
2008
Conference Publication
Towards more flexible development of Z specifications
Fu, Z. and Smith, G. (2008). Towards more flexible development of Z specifications. 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering 2008 (TASE '08), Nanjing, China, 17-19 June 2008. Piscataway, NJ, U.S.A.: IEEE - Institute of Electrical Electronics Engineers Inc.. doi: 10.1109/TASE.2008.20
2008
Conference Publication
Formal ensemble engineering
Sanders, J. W. and Smith, Graeme (2008). Formal ensemble engineering. Springer Verlag. doi: 10.1007/978-3-540-89437-7_8
2008
Conference Publication
A Minimal Set of Refactoring Rules for Object-Z
McComb, T. and Smith, G (2008). A Minimal Set of Refactoring Rules for Object-Z. International Symposium on Formal Methods (FM 2008), Oslo, Norway, 4-6 June, 2008. Heidelberg, Germany: Springer. doi: 10.1007/978-3-540-68863-1_11
2008
Edited Outputs
Electronic Notes in Theoretical Computer Science: Proceedings of the BCS-FACS Refinement Workshop (REFINE 2007)
Boiten, E., Derrick J. and Smith, Graeme Paul eds. (2008). Electronic Notes in Theoretical Computer Science: Proceedings of the BCS-FACS Refinement Workshop (REFINE 2007). BCS-FACS Refinement Workshop (REFINE 2007), Oxford, England, 2 July 2007. Amsterdam, The Netherlands: Elsevier Science ..
2008
Book Chapter
Formal Ensemble Engineering
Sanders, J.W. and Smith, G. (2008). Formal Ensemble Engineering. Software-Intensive Systems and New Computing Paradigms: Challenges and Visions. (pp. 132-138) edited by Wirsing, M., Banâtre, J.P., Hölzl, M. and Rauschmayer, A.. Heidelberg, Germany: Springer. doi: 10.1007/978-3-540-89437-7-8
2008
Conference Publication
Introducing objects through refinement
McComb, T. and Smith, G (2008). Introducing objects through refinement. International Symposium on Formal Methods (FM 2008), Turku, Finland, 26-30 May, 2008. Heidelberg, Germany: Springer. doi: 10.1007/978-3-540-68237-0_25
2008
Conference Publication
Refactoring real-time specifications
Smith, Greame and McComb, Tim (2008). Refactoring real-time specifications. International Refinement Workshop (Refine 2008), Turku, Finland, 27 May, 2008. Amsterdam, The Netherlands: Elsevier. doi: 10.1016/j.entcs.2008.06.016
2008
Conference Publication
Extending formal methods for software-intensive systems
Smith, Graeme (2008). Extending formal methods for software-intensive systems. Springer Verlag. doi: 10.1007/978-3-540-89437-7_10
2008
Conference Publication
Using Model Checking to Automatically Find Retrieve Relations
Derrick, J. and Smith, G. (2008). Using Model Checking to Automatically Find Retrieve Relations. International Refinement Workshop (Refine 2007), Oxford, UK, 2 July, 2007. Amsterdam, The Netherlands: Elseiver. doi: 10.1016/j.entcs.2008.02.019
2008
Book Chapter
Extending Formal Methods for Software-Intensive Systems
Smith, G. (2008). Extending Formal Methods for Software-Intensive Systems. Software-Intensive Systems and New Computing Paradigms: Challenges and Visions. (pp. 146-161) edited by Wirsing, M., Banâtre, J.P., Hölzl, M. and Rauschmayer, A.. Heidleberg Berlin: Springer. doi: 10.1007/978-3-540-89437-7-10
2007
Journal Article
Simulation Machines for Checking Action System Refinements
Smith, Graeme and Winter, Kirsten (2007). Simulation Machines for Checking Action System Refinements. Electronic Notes in Theoretical Computer Science, 187, 75-90. doi: 10.1016/j.entcs.2006.08.045
2007
Conference Publication
A stepwise development process for reasoning about the reliability of real-time systems
Meinicke, L. and Smith, G. (2007). A stepwise development process for reasoning about the reliability of real-time systems. 6th International Conference: IFM 2007 - Integrated Formal Methods, Oxford, U.K., 2-5 July 2007. Berlin, Germany: Springer-Verlag. doi: 10.1007/978-3-540-73210-5_23
2007
Conference Publication
Simulation machines for checking action system refinements
Smith, G. and Winter, K. (2007). Simulation machines for checking action system refinements. 11th Refinement Workshop (REFINE 2006), Macao, China, 31 October 2006. USA: Elseiver BV. doi: 10.1016/j.entcs.2006.08.045
2007
Edited Outputs
Electronic notes in theoretical computer science: proceedings of the Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference (IFM 2005)
Judi Romijn, Graeme Smith and Jaco van de Pol eds. (2007). Electronic notes in theoretical computer science: proceedings of the Doctoral Symposium affiliated with the Fifth Integrated Formal Methods Conference (IFM 2005). IFM 2005: Fifth International Conference on Integrated Formal Methods. Doctoral Symposium, Eindhoven, Netherlands, 29 November 2005. Amsterdam, Netherlands: Elsevier.
2007
Edited Outputs
Proceedings of the BCS-FACS Refinement Workshop (REFINE 2007)
Eerke Boiten, John Derrick and Graeme Smith eds. (2007). Proceedings of the BCS-FACS Refinement Workshop (REFINE 2007). International Refinement Workshop (Refine 2007), Oxford, United Kingdom, 2 July, 2007. Amsterdam, The Netherlands: Elsevier.
2006
Conference Publication
Verifying data refinements using a model checker
Smith, Graeme and Derrick, John (2006). Verifying data refinements using a model checker. Surrey, United Kingdom: Springer U. K.. doi: 10.1007/s00165-006-0002-7
2006
Conference Publication
Compositional class refinement in object-Z
McComb, Tim and Smith, Graeme (2006). Compositional class refinement in object-Z. FM 2006: Formal Methods, Hamilton, Canada, 21-27 August 2006. Berlin, Germany: Springer. doi: 10.1007/11813040
2005
Journal Article
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface
Romijn, Judi, Smith, Graeme, Van De Pol, Jaco, Bert, Didier, Boiten, Eerke, Bowen, Jonathan, Butler, Michael, Curzon, Paul, Davies, Jim, Derrick, John, Dunne, Steve, Dong, Jin Song, Galloway, Andy, George, Chris, Grieskamp, Wolfgang, Habrias, Henri, Heisel, Maritta, Kim, Soon-Kyeong, Lemoine, Michel, Liu, Shaoying, Mery, Dominique, Merz, Stephan, Paige, Richard, Petre, Luigia, Santen, Thomas, Schneider, Steve, Schulte, Wolfram, Sere, Kaisa, Sinclair, Jane ... Woodcock, Jim (2005). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3771 LNCS
2005
Journal Article
Guest Editorial integrated formal methods
Boiten, E., Derrick, J. and Smith, G. (2005). Guest Editorial integrated formal methods. Formal Aspects of Computing, 17 (4), 389-389. doi: 10.1007/s00165-005-0078-5
Funding
Supervision
Availability
- Associate Professor Graeme Smith is:
- Available for supervision
Before you email them, read our advice on how to contact a supervisor.
Supervision history
Current supervision
-
Doctor Philosophy
Verified Secure Compilation for C-like Programs
Principal Advisor
Other advisors: Associate Professor Mark Utting
Completed supervision
-
2012
Master Philosophy
FORMAL PROPERTY PRESERVATION AND TRANSFORMATION IN SOFTWARE EVOLUTION
Principal Advisor
Other advisors: Emeritus Professor Ian Hayes
-
2007
Doctor Philosophy
Formal Derivation of Object-Oriented Designs
Principal Advisor
-
2007
Doctor Philosophy
A Behaviour-based methodology for fault tree generation.
Associate Advisor
-
2005
Doctor Philosophy
ANIMATION AND VISUALISATION OF REFINEMENTS
Associate Advisor
Media
Enquiries
Contact Associate Professor Graeme Smith directly for media enquiries about:
- Formal methods
- Mathematical modelling
- Multi-agent systems
- Self-adaptive systems
- Software-intensive systems
Need help?
For help with finding experts, story ideas and media enquiries, contact our Media team: