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
2014
Conference Publication
A formal development approach for self-organising systems
Li, Q. and Smith, G. (2014). A formal development approach for self-organising systems. 8th International Symposium on Theoretical Aspects of Software Engineering, TASE 2014, Changsha, Hunan, China, 1-3 September 2014. Los Alamitos, CA United States: IEEE Computer Society. doi: 10.1109/TASE.2014.11
2014
Conference Publication
MAZE: An extension of object-Z for multi-agent systems
Smith, Graeme and Li, Qin (2014). MAZE: An extension of object-Z for multi-agent systems. 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014, Toulouse, France, June 2, 2014-June 6, 2014. Heidelberg, Germany: Springer. doi: 10.1007/978-3-662-43652-3_6
2013
Conference Publication
Using bounded fairness to specify and verify ordered asynchronous multi-agent systems
Li, Qin and Smith, Graeme (2013). Using bounded fairness to specify and verify ordered asynchronous multi-agent systems. ICECCS 2013: 18th International Conference on Engineering of Complex Computer Systems, Mt Elizabeth, Singapore, 17-19 July, 2013. Piscataway, NJ, United States: IEEE Computer Society Conference Publishing Services (CPS). doi: 10.1109/ICECCS.2013.24
2013
Conference Publication
A refinement framework for autonomous agents
Li, Qin and Smith, Graeme (2013). A refinement framework for autonomous agents. SBMF 2013: 16th Brazilian Symposium on Formal Methods, Brasilia, Brazil, 29 September-4 October, 2013. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-41071-0_12
2012
Journal Article
Temporal-logic property preservation under Z refinement
Derrick, John and Smith, Graeme (2012). Temporal-logic property preservation under Z refinement. Formal Aspects of Computing, 24 (3), 393-416. doi: 10.1007/s00165-011-0177-4
2012
Conference Publication
Using conventional reasoning techniques for self-organising systems
Smith, Graeme and Sanders, J. W. (2012). Using conventional reasoning techniques for self-organising systems. 2012 Tenth Annual International Conference on Privacy, Security and Trust, Paris, France, 16-18 July 2012. Piscataway, NJ, United States: IEEE. doi: 10.1109/PST.2012.6297952
2012
Conference Publication
Reasoning about adaptivity of agents and multi-agent systems
Smith, Graeme, Sanders, J. W. and Winter, Kirsten (2012). Reasoning about adaptivity of agents and multi-agent systems. IEEE Intenational Conference on Engineering of Complex Computer Systems, Paris, France, 18-20 July 2012. Piscataway, NJ, United States: IEEE Computer Society. doi: 10.1109/ICECCS.2012.32
2012
Conference Publication
Incremental development of multi-agent systems in Object-Z
Smith, Graeme and Winter, Kirsten (2012). Incremental development of multi-agent systems in Object-Z. Software Engineering Workshop (SEW-35), Heraklion, Crete, Greece, 12-13 October 2012. Piscataway, NJ, United States: IEEE Computer Society Press. doi: 10.1109/SEW.2012.19
2011
Journal Article
Property transformation under specification change
Fu, Zheng and Smith, Graeme (2011). Property transformation under specification change. Frontiers of Computer Science in China, 5 (1), 1-13. doi: 10.1007/s11704-010-0112-5
2011
Conference Publication
Refactoring object-oriented specifications with inheritance-based polymorphism
Smith, Graeme and Helke, Steffen (2011). Refactoring object-oriented specifications with inheritance-based polymorphism. 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011, Xi'an, Shaanxi, China, 29-31 August 2011. Piscataway, NJ, United States: IEEE. doi: 10.1109/TASE.2011.31
2010
Conference Publication
Assuring adaptive behaviour in self-organising systems
Sanders, J.W. and Smith, Graeme (2010). Assuring adaptive behaviour in self-organising systems. Workshop on Trustworthy Self-Organizing Systems, Budapest, Hungary, 27-28 September, 2010. Piscatawa, NJ, U.S.A.: IEEE - Computer Society. doi: 10.1109/SASOW.2010.36
2010
Conference Publication
Gravity points in potential-field approaches to self organisation
Sampson, Aaron and Smith, Graeme (2010). Gravity points in potential-field approaches to self organisation. SASO 2010: Fourth IEEE International Conference on Self-Adaptive and Self-Organizing Systems, Budapest, Hungary, 27-28 September 2010. Piscataway, NJ, U.S.A.: Institute of Electrical and Electronic Engineers (IEEE). doi: 10.1109/SASOW.2010.24
2010
Conference Publication
An approach to formal verification of free-flight separation
Eder, Sebastian and Smith, Graeme (2010). An approach to formal verification of free-flight separation. Fourth IEEE International Conference on Self-Adaptive and Self-Organizing Systems 2010, Budapest, Hungary, 27-28 September 2010. Piscataway, NJ, United States: IEEE. doi: 10.1109/SASOW.2010.35
2010
Journal Article
Formal Aspects of Computing: Editorial
Boiten, Eerke, Butler, Michael, Derrick, John and Smith, Graeme (2010). Formal Aspects of Computing: Editorial. Formal Aspects of Computing, 22 (1), 1-1. doi: 10.1007/s00165-009-0147-2
2009
Journal Article
Refining Emergent Properties
Sanders, J. W. and Smith, Graeme (2009). Refining Emergent Properties. Electronic Notes in Theoretical Computer Science, 259 (C), 207-223. doi: 10.1016/j.entcs.2009.12.026
2009
Conference Publication
Refining emergent properties
Sanders, J. W. and Smith, Graeme (2009). Refining emergent properties. International Refinement Workshop (Refine 2009), Eindhoven, The Netherlands, 3 November 2009. Amsterdam , The Netherlands: Elsevier.
2009
Conference Publication
Formal development of self-organising systems
Smith, Graeme and Sanders, J. W. (2009). Formal development of self-organising systems. 6th International Conference on Autonomic and Trusted Computing (ATC 2009), Brisbane, Australia, 7 - 9 July 2009. Heidelberg, Germany: Springer. doi: 10.1007/978-3-642-02704-8_8
2009
Journal Article
Model checking action system refinements
Smith, Graeme and Winter, Kirsten (2009). Model checking action system refinements. Formal Aspects of Computing, 21 (1-2), 155-186. doi: 10.1007/s00165-007-0053-4
2008
Journal Article
Refactoring Real-time Specifications
Smith, Graeme and McComb, Tim (2008). Refactoring Real-time Specifications. Electronic Notes in Theoretical Computer Science, 214 (C), 359-380. doi: 10.1016/j.entcs.2008.06.016
2008
Journal Article
Using Model Checking to Automatically Find Retrieve Relations
Derrick, John and Smith, Graeme (2008). Using Model Checking to Automatically Find Retrieve Relations. Electronic Notes in Theoretical Computer Science, 201 (C), 155-175. doi: 10.1016/j.entcs.2008.02.019
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: