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
2002
Conference Publication
Encoding Object-Z in Isabelle/HOL
Smith, G. P., Kammuller, F. and Santen, T. (2002). Encoding Object-Z in Isabelle/HOL. ZB 2002: Formal Specification and Development in Z and B, Grenoble, France, 23-25 January, 2002. Heidelberg: Springer-Verlag. doi: 10.1007/3-540-45648-1_5
2002
Conference Publication
An integration of real-time object-Z and CSP for specifying concurrent real-time systems
Smith, G. P. (2002). An integration of real-time object-Z and CSP for specifying concurrent real-time systems. IFM 2002, Turku, Finland, 15-18 May, 2002. Berlin: Springer-Verlag. doi: 10.1007/3-540-47884-1_15
2001
Conference Publication
Model checking object-Z classes: Some experiments with FDR
Kassel, Geoff and Smith, Graeme (2001). Model checking object-Z classes: Some experiments with FDR. doi: 10.1109/apsec.2001.991513
2001
Other Outputs
Specification, refinement and verification of concurrent systems: an integration of Object-Z and CSP
Smith, G. P. and Derrick, J. (2001). Specification, refinement and verification of concurrent systems: an integration of Object-Z and CSP. Brisbane: Software Verification Research Cen. Univ of Qld.
2001
Other Outputs
State-based formal methods for distributed processing: from Z to Object-Z
Smith, G. P. (2001). State-based formal methods for distributed processing: from Z to Object-Z. Brisbane: Software Verification Research Cen. Univ of Qld.
2001
Book Chapter
State-Based Approaches: From Z to Object-Z
Smith, G. P. (2001). State-Based Approaches: From Z to Object-Z. Formal Methods for Distributed Processing: A Survey of Object-Orientated Approaches. (pp. 105-125) edited by H. Bowman and J. Derrick. Cambridge, UK: Cambridge University Press.
2001
Other Outputs
Model checking Object-Z classes: Some experiments with FDR
Kassel, G. D. and Smith, G. P. (2001). Model checking Object-Z classes: Some experiments with FDR. Brisbane: Software Verification Research Cen. Univ of Qld.
2001
Journal Article
Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP
Smith, G and Derrick, J (2001). Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP. Formal Methods In System Design, 18 (3), 249-284. doi: 10.1023/A:1011269103179
2001
Other Outputs
Specifying mode requirements for embedded systems
Smith, G. P. (2001). Specifying mode requirements for embedded systems. Brisbane: Software Verification Research Cen. Univ of Qld.
2001
Conference Publication
Introducing parallel composition to the timed refinement calculus
Smith, G. P. (2001). Introducing parallel composition to the timed refinement calculus. PART 2000, Sydney, 29-30 November 2000. Hong Kong: Springer Verlag.
2001
Other Outputs
Encoding Object-Z in Isabelle-HOL
Smith, G. P., Kammuller, F and Santen, T (2001). Encoding Object-Z in Isabelle-HOL. Brisbane: Software Verification Research Cen. Univ of Qld.
2000
Conference Publication
Structural refinement in Object-Z / CSP
Derrick, J. and Smith, G. P. (2000). Structural refinement in Object-Z / CSP. Integrated Formal Methods: Second International Conference, IFM 2000, Schloss Dagstuhl, Germany, 1-3 November, 2000. Berlin: Springer Verlag. doi: 10.1007/3-540-40911-4_12
2000
Journal Article
Incremental development of real-time requirements: The light control case study
Smith, G. P. and Fidge, C. J. (2000). Incremental development of real-time requirements: The light control case study. Journal of Universal Computer Science, 6 (7), 704-730.
2000
Conference Publication
Stepwise development from ideal specifications
Smith, Graeme (2000). Stepwise development from ideal specifications. ACSC 2000, Canberra, 31 January - 3 February 2000. Los Alamitos, California, USA: IEEE Computer Society. doi: 10.1109/ACSC.2000.824408
2000
Conference Publication
Structuring real-time Object-Z specifications
Smith, G and Hayes, I (2000). Structuring real-time Object-Z specifications. Integrated Formal Methods: Second International Conference, IFM 2000,, Dagstuhl Castle, Germany, November 2000. Berlin, Germany: Springer. doi: 10.1007/3-540-40911-4_7
2000
Conference Publication
Safety assurance of Commercial-Off-The-Shelf software
Lindsay, P. A. and Smith, G. P. (2000). Safety assurance of Commercial-Off-The-Shelf software. 5th Australian Workshop on Safety Critical Systems & Software, Melbourne, Australia, 24 November, 2000. Melbourne, Australia: Australian Computer Society.
2000
Conference Publication
Recursive schema definitions in Object-Z
Smith, G. P. (2000). Recursive schema definitions in Object-Z. International Conference of B and Z Users (ZB 2000), York, UK, 29 August - 2 September 2000. Berlin: Springer Verlag.
1999
Book
Stepwise development from ideal specifications
Smith, Graeme (1999). Stepwise development from ideal specifications. SVRC Technical Report, 99-35. Software Verification Research Centre, School of Information Technology and Electrical Engineering, The University of Queensland.
1999
Book
Towards real-time object-Z
Smith, Graeme and Hayes, Ian (1999). Towards real-time object-Z. Technical Report SSE, 99-10. Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland.
1999
Conference Publication
Specification and refinement of a real-time control system
Smith, G. P. (1999). Specification and refinement of a real-time control system. 22nd Australasian Computer Science Conference, Auckland, NZ, 18-21 Jan, 1999. Auckland, NZ: Springer Verlag.
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: