Graeme Smith
 

Senior Lecturer (part-time)
School of Information Technology and Electrical Engineering
The University of Queensland 4072 
Australia 
Tel: +61 7 3365 1625
Fax: +61 7 3365 4999
email: smith@itee.uq.edu.au
Me (left) with John Derrick from the University of Sheffield (atop Mt Maroon).

Professional Activities

Member of ERCIM InterLink Working Group on Software-Intensive Systems and New Computing Paradigms

Co-chair of International Refinement Workshop (Refine 2007)
Co-chair of 4th and 5th International Conferences on Integrated Formal Methods (IFM 2004, IFM 2005)

Programme Committee of International Conference on Integrated Formal Methods (IFM99, IFM2000, IFM2002, IFM 2004, IFM 2005, IFM 2007, iFM 2009)
Programme Committee of International Z User Meeting (ZUM 2006)
Programme Committee of International Conference of Z and B Users (ZB2002, ZB2003, ZB 2005)
Programme Committee of International Conference on Formal Engineering Methods (ICFEM 2003, ICFEM 2004)
Programme Committee of International Conference on Software Engineering and Formal Methods (SEFM 2003)

Editor for special issue of Formal Aspects of Computing, 2009. (To appear.)
Editor for special issue of Electronic Notes in Theoretical Computer Science (volume 191), 2007. 
Editor for special issue of Formal Aspects of Computing (volume 17, number 4), 2005.
Editor for special issue of  L'Objet (volume 6, number 1), 1999.

Z Standardisation Review Committee

Object-Z page of the WWW Virtual Library

Obejct-Z tutorial given at ZB2000

Publications

Book

  1. G. Smith. The Object-Z Specification Language. Advances in Formal Methods Series. Kluwer Academic Publishers, 2000.

Edited Proceedings

  1. E. Boiten, J. Derrick and G. Smith, editors, International Refinement Workshop (Refine 2007), volume 201 of Electronic Notes Theoretical Computer Science. Elsevier, 2008.
  2. J. Romijn, G. Smith and J. van de Pol, editors, Integrated Formal Methods: 5th International Conference, IFM 2005, volume 3771 of Lecture Notes in Computer Science. Springer-Verlag, 2005.
  3. E.A. Boiten, J. Derrick and G. Smith, editors, Integrated Formal Methods: 4th International Conference, IFM 2004, volume 2999 of Lecture Notes in Computer Science. Springer-Verlag, 2004.

Book Chapters

  1. J.W. Sanders and G. Smith. Formal ensemble engineering. In M. Wirsing, J.-P. Banâtre, M. Hölzl and A. Rauschmayer, editors, Challenges for Software-Intensive Systems and New Computing Paradigms, volume 5380 of Lecture Notes in Computer Science, pp. 132-138. Springer-Verlag. 2008.
  2. G. Smith. Extending formal methods for software-intensive systems. In M. Wirsing, J.-P. Banâtre, M. Hölzl and A. Rauschmayer, editors, Challenges for Software-Intensive Systems and New Computing Paradigms, volume 5380 of Lecture Notes in Computer Science., pp.146-161. Springer-Verlag, 2008.
  3. G. Smith. State-based approaches: From Z to Object-Z. In H. Bowman and J. Derrick, editors, Formal Methods for Distributed Processing: A Survey of Object-Oriented Approaches, chapter 6, pages 105-125. Cambridge University Press, 2001.

Journal Publications

  1. G. Smith and K. Winter. Model checking action system refinements. Formal Aspects of Computing, 21(1):155-186. Springer-Verlag, 2009.
  2. G. Smith and J. Derrick. Verifying data refinements using a model checker. Formal Aspects of Computing, 18(3):264-287. Springer-Verlag, 2006.
  3. J. Derrick and G. Smith. Structural refinement of systems specified in Object-Z and CSP. Formal Aspects of Computing, 15(1):1-27. Springer-Verlag, 2003.
  4. G. Smith and I.J. Hayes. An introduction to Real-Time Object-Z. Formal Aspects of Computing, 13(2):128-141. Springer-Verlag, 2002.
  5. G. Smith and J. Derrick. Specification, refinement and verification of concurrent systems - an integration of Object-Z and CSP. Formal Methods in System Design, 18(3):249-284. Kluwer Academic Publishers, 2001.
  6. G. Smith and C. Fidge. Incremental Development of Real-Time Requirements: The Light Control Case Study. Journal of Universal Computer Science, 6(7):704-730. Springer-Verlag, 2000.
  7. R. Duke, C. Bailes and G. Smith. A Blocking Model for Reactive Objects. Formal Aspects of Computing, 8(3):347-368. Springer-Verlag, 1996.
  8. R. Duke, C. Bailes and G. Smith. A Fully Abstract Model of Reactive Objects. Formal Aspects of Computing, 8(D):184-243. Springer-Verlag, 1996.
  9. G. Smith. A Fully Abstract Semantics of Classes for Object-Z. Formal Aspects of Computing, 7(3):289-313. Springer-Verlag, 1995.
  10. G. Smith. A Fully Abstract Semantics of Classes for Object-Z (full paper). Formal Aspects of Computing, 7(E):30-66. Springer-Verlag, 1995.
  11. R. Duke, G. Rose and G. Smith. Object-Z: a Specification Language Advocated for the Description of Standards. Computer Standards and Interfaces, 17:511-533. North-Holland, 1995. (Available as tech report.)
  12. R. Duke and G. Smith. Temporal Logic and Z Specifications. Australian Computer Journal, 21(2):62-66, 1989.

Fully Refereed Conference Publications

  1. G. Smith and J.W. Sanders. Formal development of self-organising systems. To appear in International Conference on Autonomic and Trusted Computing (ATC-09), Lecture Notes in Computer Science. Springer-Verlag, 2009.
  2. G. Smith and T. McComb. Refactoring Real-Time Specifications. In International Refinement Workshop (Refine 2008), volume 214 of Electronic Notes in Theoretical Computer Science, pp. 359-380. Elsevier, 2008.

  3. Z. Fu and G. Smith. Towards More Flexible Development of Z Specifications. In IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2008), pp. 281-288. IEEE Computer Society Press, 2008. 

  4. T. McComb and G. Smith. A Minimal Set of Refactoring Rules for Object-Z. In International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2008), volume 5051 of Lecture Notes in Computer Science, pp. 170-184. Springer-Verlag, 2008.

  5. T. McComb and G. Smith. Introducing objects through refinement. In International Conference on Formal Methods (FM 2008), volume 5014 of Lecture Notes Computer Science, pp. 358-373. Springer-Verlag, 2008.       

  6. J. Derrick and G. Smith. Using model checking to automatically find retrieve relations. In E. Boiten, J. Derrick and G. Smith, editors, International Refinement Workshop (Refine 2007), volume 201 of Electronic Notes in Theoretical Computer Science, pp. 155-175. Elsevier, 2008.
  7. L. Meinicke and G. Smith. A stepwise development process for reasoning about the reliability of real-time systems. In 6th International Conference on Integrated Formal Methods (IFM 2007), volume 4591 of Lecture Notes in Computer Science, pp. 439-458. Springer-Verlag, 2007.
  8. G. Smith and K. Winter. Simulation machines for checking action system refinements. In B. Aichernig, E. Boiten, J. Derrick and L. Groves, editors, International Refinement Workshop (Refine 2006), volume 187 of Electronic Notes in Theoretical Computer Science, pp. 75-90. Elsevier, 2007.
  9. T. McComb and G.Smith. Compositional Class Refinement in Object-Z. In Formal Methods (FM 2006). volume 4085 of Lecture Notes in Computer Science, pp. 205-220. Springer-Verlag, 2006.
  10. G. Smith and J. Derrick. Model checking downward simulations. In J. Derrick and E. Boiten, editors, International Refinement Workshop (Refine 2005), Issue 2, volume 137 of Electronic Notes in Theoretical Computer Science, pp.205-224. Elsevier, 2005.
  11. G. Smith and L. Wildman. Model checking Z specifications using SAL.  In H. Treharne, S. King, M. Henson and S. Schneider, editors, International Conference of B and Z Users (ZB 2005), volume 3455 of Lecture Notes in Computer Science, pp.85-103. Springer-Verlag, 2005.
  12. J. Derrick and G. Smith. Linear Temporal Logic and Z Refinement. In Algebraic Methodology and Software Technology (AMAST 2004), volume 3116 of Lecture Notes in Computer Science. Springer-Verlag, 2004.
  13. T. McComb and G. Smith. Architectural Design in Object-Z. In Australian Software Engineering Conference (ASWEC 2004). IEEE Computer Society, 2004.
  14. G. Smith. A Formal Framework for Modelling and Analysing Mobile Systems. In Australasian Computer Science Conference (ACSC 2004), Australian Computer Society, 2004.
  15. T. McComb and G. Smith. Animation of Object-Z specifications using a Z animator. In International Conference on Software Engineering and Formal Methods (SEFM 2003), IEEE Computer Society, 2003.
  16. G. Smith and K. Winter. Proving temporal properties of Z specifications using abstraction. In D. Bert, J.P. Bowen, S. King and M. Waldén, editors, 3rd International Conference of Z and B Users (ZB 2003), volume 2561 of Lecture Notes in Computer Science, pages 260-279. Springer-Verlag, 2003.
  17. K. Winter and G. Smith. Compositional verification for Object-Z. In D. Bert, J.P. Bowen, S. King and M. Waldén, editors, 3rd International Conference of Z and B Users (ZB 2003), volume 2561 of Lecture Notes in Computer Science, pages 280-299. Springer-Verlag, 2003.
  18. G. Smith. Introducing Reference Semantics via Refinement. In C. George and Huaikou Miao, editors, 4th International Conference on Formal Engineering Methods (ICFEM 2002), volume 2495 of Lecture Notes in Computer Science, pages 588-599. Springer-Verlag, 2002.
  19. G. Smith and J. Derrick. Abstract Specification in Object-Z and CSP. In C. George and Huaikou Miao, editors, 4th International Conference on Formal Engineering Methods (ICFEM 2002), volume 2495 of Lecture Notes in Computer Science, pages 108-119. Springer-Verlag, 2002.
  20. G. Smith. An integration of Real-Time Object-Z and CSP for specifying concurrent real-time systems. In K. Sere and M. Butler, editors, 3rd International Conference on Integrated Formal Methods (IFM 2002), volume 2335 of Lecture Notes in Computer Science, pages 267-285. Springer-Verlag, 2002.
  21. G. Smith, F. Kammüller and T. Santen. Encoding Object-Z in Isabelle/HOL. In D. Bert, J.P. Bowen, M.C. Henson and K. Robinson, editors, 2nd International Conference of Z and B Users (ZB 2002), volume 2272 of Lecture Notes in Computer Science, pages 82-99. Springer-Verlag, 2002.
  22. G. Smith. Specifying mode requirements of embedded systems. In M. Oudshoorn, editor, 25th Australasian Computer Science Conference (ACSC 2002), Australian Computer Science Communications, volume 24(1): 251-258. Australian Computer Society, 2002.
  23. G. Kassel and G. Smith. Model Checking Object-Z Classes: Some Experiments with FDR. In 8th Asia-Pacific Software Engineering Conference (APSEC 2001), pages 445-452. IEEE Computer Society Press, 2001.
  24. G. Smith. Introducing Parallel Composition to the Timed Refinement Calculus. In H. ElGindy and C. Fidge, editors, Parallel and Real-Time Systems (PART 2000), pages 139-148, Springer-Verlag, 2001.
  25. G. Smith and I.J. Hayes. Structuring Real-Time Object-Z Specifications. In W. Grieskamp, T. Santen and B. Stoddart, editors, Integrated Formal Methods (IFM 00), volume 1945 of Lecture Notes in Computer Science, pages 97-115. Springer-Verlag, 2000.
  26. J. Derrick and G. Smith. Structural Refinement in Object-Z/CSP. In W. Grieskamp, T. Santen and B. Stoddart, editors, Integrated Formal Methods (IFM 00), volume 1945 of Lecture Notes in Computer Science, pages 194-213. Springer-Verlag, 2000.
  27. P. Lindsay and G. Smith. Safety Assurance of Commercial-Off-The-Shelf Software. In A. Griffiths, editor, 5th Australian Workshop on Safety Critical Systems and Software, pages 43-51. Australian Computer Society, 2000.
  28. G. Smith. Recursive Schema Definitions in Object-Z. In J.P. Bowen, S. Dunne, A. Galloway and S. King, editors, 1st International Conference of Z and B Users (ZB 2000), volume 1878 of Lecture Notes in Computer Science, pages 42-58. Springer-Verlag, 2000.
  29. G. Smith. Stepwise Development from Ideal Specifications. In J. Edwards, editor, 23rd Australasian Computer Science Conference (ACSC 2000), Australian Computer Science Communications, volume 22(1):227-233. IEEE Computer Society, 2000.
  30. G. Smith and I.J. Hayes. Towards Real-Time Object-Z. In K. Araki, A.Galloway and K. Taguchi, editors, Integrated Formal Methods (IFM 99), pages 49-65. Springer-Verlag, 1999.
  31. G. Smith. Specification and Refinement of a Real-Time Control System. In J. Edwards, editor, Australasian Computer Science Conference (ACSC'99), Australian Computer Science Communications, Vol. 21, No. 1, pages 360-371. Springer-Verlag, 1999.
  32. C. Fischer and G. Smith. Combining CSP and Object-Z: Finite Trace or Infinite Trace Semantics? In T. Mizuno, N. Shiratori, T. Higashino and A.Togashi, editors, Formal Description Techniques and Protocol Specification, Verification, and Testing (FORTE/PSTV'97), pages 503-518. Chapman & Hall, 1997.
  33. G. Smith and J. Derrick. Refinement and verification of concurrent systems specified in Object-Z and CSP. In First IEEE International Conference on Formal Engineering Methods (ICFEM'97), pages 293-302. IEEE Computer Press, 1997.
  34. G. Smith. A Semantic Integration of Object-Z and CSP for the Specification of Concurrent Systems. In J. Fitzgerald, C.B. Jones and P. Lucas, editors, Formal Methods Europe (FME'97), volume 1313 of Lecture Notes in Computer Science, pages 62-81. Springer-Verlag, 1997.
  35. G. Smith. Reasoning about Object-Z specifications. In Proceedings Asia-Pacific Software Engineering Conference (APSEC '95), pages 489-497, IEEE Computer Society Press, 1995.
  36. G. Smith. Extending W  for Object-Z. In J. Bowen and M. Hinchey, editors, 9th International Conference of Z Users (ZUM'95), volume 967 of Lecture Notes in Computer Science, pages 276-295. Springer-Verlag, 1995.
  37. G. Smith. Formal Definitions of Behavioural Compatibility for Active and Passive Objects. In Proceedings Asia-Pacific Software Engineering Conference (APSEC '94), pages 336-344, IEEE Computer Society Press, 1994.
  38. N. Lévy and G.Smith. A Language-Independent Approach to Specification Construction. In D. Wile, editor, Proceedings ACM SIGSOFT Symposium on the Foundations of Software Engineering, Software Engineering Notes, 19(5):76-86, ACM Press, 1994.
  39. G. Smith. An Object-Oriented Development Framework for Z. In J. Bowen and J. Hall, editors, 8th Z User Meeting (ZUM'94), pages 89-107. Workshops in Computing, Springer-Verlag, 1994.
  40. G. Smith. A Development Framework for Object-Oriented Specification and Refinement. In B. Magnusson, B. Meyer, J.-M. Nerson and J.-F. Perrot, editors, Proceedings Technology of Object-Oriented Languages and Systems (TOOLS EUROPE '94), pages 173-183, 1994.
  41. G. Smith and R. Duke. Specifying Concurrent Systems Using Object-Z. In Proceedings 15th Australian Computer Science Conference (ACSC-15), pages 859-871, 1992.
  42. R. Duke, P. King, G. Rose and G. Smith. The Object-Z Specification Language. In T. Korson, V. Vaishnavi and B. Meyer, editors, Technology of Object-Oriented Languages and Systems (TOOLS 5), pages 465-483. Prentice-Hall, 1991.
  43. R. Duke, P. King and G. Smith. Combining Formal Methods with Object-Oriented Design: An Emerging Trend in Software Engineering. In Proceedings Australian Computer Conference (ACC'91 MOSAIC), pages 181-194, 1991.
  44. R. Duke, P. King and G. Smith. Formalising Behavioural Compatibility for Reactive Object-Oriented Systems. In Proceedings 14th Australian Computer Science Conference (ACSC-14), pages 11/1-11/11, 1991.
  45. R. Duke, G. Rose and G. Smith. Transferring Formal Techniques to Industry: A Case Study. In J. Quemada, J. Mañas and E. Vazquez, editors, Formal Description Techniques (FORTE'90), pages 279-286. North-Holland, 1990.
  46. P. King and G. Smith. Formalisation of Behavioural and Structural Concepts for Communications Systems. In L. Logrippo, R. L. Probert and H. Ural, editors, Protocol Specification, Testing and Verification X (PSTV X), pages 1-18. North-Holland, 1990.
  47. D. Carrington and G. Smith. Extending Z for Object-Oriented Specifications. In Proceedings 5th Australian Software Engineering Conference (ASWEC'90), pages 9-14, 1990.
  48. G. Smith and R. Duke. Modelling a Cache Coherence Protocol using Object-Z. In Proceedings 13th Australian Computer Science Conference (ACSC-13), pages 352-361, 1990.
  49. D. Carrington, D. Duke, R. Duke, P. King, G. Rose and G. Smith. Object-Z: An Object-Oriented Extension to Z. In S. Voung, editor, Formal Description Techniques (FORTE'89), pages 281-296. North-Holland, 1990.
  50. G. Smith. A Formal Specification of Signalling System No. 7 Telephone User Part. In Proceedings 1989 Singapore International Conference on Networks (SICON'89), pages 50-55, 1989.
  51. R. Duke and G. Smith. Temporal Logic and Z Specifications. In Proceedings 12th Australian Computer Science Conference (ACSC-12), Appendix, pages 32-42, 1989. Selected by programme commitee for publication in the Australian Computer Journal.

Other Publications

  1. G. Smith. Incremental development of software-intensive systems. In, J.-P. Banâtre, M. Hölzl and M. Wirsing, editors, Opening InterLink Workshop: Thematic Area 1 (TA1/WG1) Software Intensive Systems and New Computing Paradigms. Technical Report, Institut für Informatik, Ludwig-Maximilians-Universität Munchen, 2007.
  2. J. Romijn, G. Smith and J. van de Pol, editors, IFM2005 Doctoral Symposium on Integrated Formal Methods. CS-Report 05-29, Department of Mathematics and Computer Science, Technische Universiteit Eindhoven, 2005.
  3. P. Lindsay and G. Smith. Safety Assurance of Commercial-Off-The-Shelf Software. In Software Engineering Australia (SEA 2000), 2000.
  4. G. Smith. From Ideal to Realisable Real-Time Specifications. In N. Leslie, editor, Fifth New Zealand Formal Program Development Colloquium, IIMS Technical Report 99-1, Institute of Information and Mathematical Sciences, Massey University at Albany, 1999.
  5. G. Smith. Integrating Object-Z and CSP for the Specification of Object-Oriented Concurrent Systems. In S. Mitchell and J. Bosch, editors, European Conference on Object-Oriented Programming (ECOOP'97) Workshop Reader, volume 1357 of Lecture Notes in Computer Science. Springer-Verlag, 1997.

PhD Thesis

  1. G. Smith. An Object-Oriented Approach to Formal Specification, Department of Computer Science, University of Queensland, 1992.

Selected Technical Reports (not published elsewhere)

  1. G. Smith. Formal Verification of Object-Z Specifications. Technical Report 95-55, Software Verification Research Centre, University of Queensland, 1995.
  2. G. Smith. A Logic for Object-Z (Additional Rules). Technical Report 95-26, Software Verification Research Centre, University of Queensland, 1995.

smith@itee.uq.edu.au
Last modified: March, 2009