Research interests: a brief history

My interest in research started early; I enrolled in an MSc. by research as soon as I finished my undergraduate course, and immediately afterwards, I took up a position in a technological institute in Brazil: ITEP. In that post, I was part of the leading team that spread the use of the Internet in Brazil, and worked in a research project that aimed at combining formal specification techniques with the emerging object-oriented programming technology.

(1990--1993) An object-oriented extension of Z.

With Prof. Silvio Meira, Universidade Federal de Pernambuco, Brazil, we proposed MooZ, an object-oriented extension
to a popular specification notation: Z. A simple and powerful treatment of messages and inheritance gave it an edge over other proposals for modularisation in Z. Our results stimulated further work by other members of our group on the definition of a formal semantics and the development of support tools for MooZ.  The main publication that describes MooZ is the following.

S. R. L. Meira and A. L. C. Cavalcanti. Modular Object-Oriented Z Specifications. In J. Nicholls, editor, Z User Workshop, Workshops in Computing, pages 173 - 192, Oxford - UK, 1990. Springer-Verlag.
[ bib ]

During my PhD, I addressed program verification.

(1993--1997) A refinement calculus for Z.

We presented and formalised ZRC, a refinement calculus that incorporates the Z notation and follows its style and conventions. We constructed a weakest precondition semantics for Z based on a relational model proposed by the standards panel, and proved an extensive set of laws consistent with the style of Z. Our work gives a definitive account of a refinement by calculation technique based on Z. My PhD thesis is available as a Technical Monograph in the Oxford University Computing Laboratory.

A. L. C. Cavalcanti. A Refinement Calculus for Z. PhD thesis, Oxford University Computing Laboratory, Oxford - UK, 1997. Technical Monograph TM-PRG-123, ISBN 00902928-97-X.
[ bib ]

The main publications that came out of my thesis are as follows. 

  • A. L. C. Cavalcanti and J. C. P. Woodcock. ZRC-A Refinement Calculus for Z. Formal Aspects of Computing, 10(3):267-289, 1999.
    [ bib ]
  • A. L. C. Cavalcanti, A. C. A. Sampaio, and J. C. P. Woodcock. An Inconsistency in Procedures, Parameters, and Substitution the Refinement Calculus. Science of Computer Programming, 33(1):87 - 96, 1999.
    [ bib ]
  • A. L. C. Cavalcanti and J. C. P. Woodcock. A Weakest Precondition Semantics for Z. The Computer Journal, 41(1):1 - 15, 1998.
    [ bib ]
  • A. L. C. Cavalcanti, A. C. A. Sampaio, and J. C. P. Woodcock. Procedures and Recursion in the Refinement Calculus. Journal of the Brazilian Computer Society, 5(1):1 - 15, 1998.
    [ bib ]

Afterwards I conclude the doctorate, I went back to Brazil and started working as lecturer in Centro de Informatica, Universidade Federal de Pernambuco. In my reasearch, I concentrated on the application of my results on verification to a programming technology that was by then very much favoured in industry.

(1998--2002) A calculus for object-oriented programming.

We designed and formalised a refinement calculus of object-oriented programs. This work was conducted in collaboration with Prof. Augusto Sampaio, Universidade Federal de Pernambuco, Brazil, with Dr David Naumann, Stevens Institute of Technology, USA. Our language was a subset of sequential Java, that includes inheritance, dynamic binding, recursion, and visibility control. We provided a weakest precondition semantics for this language, explored techniques of class refinement, and proposed and proved a complete set of programming laws for object-orientation. To address practical issues, we formalised refactoring rules as refinement laws, and formulated laws for compilation by means of correctness-preserving
transformation.

The language and its weakest precondition semantics are described in the paper below.

A. L. C. Cavalcanti and D. A. Naumann. A Weakest Precondition Semantics for Refinement of Object-oriented Programs. IEEE Transactions on Software Engineering, 26(8):713 - 728, 2000.
[ bib ]

A comprehensive set of laws for object-oriented programming is given in the following paper. 

P. H. M. Borba, A. C. A. Sampaio, A. L. C. Cavalcanti, and M. L. Cornélio. Algebraic Reasoning for Object-Oriented Programming. Science of Computer Programming, 52:53-100, 2004.
[ bib ]

My current focus is on concurrency and reactivity, which are common features of modern systems.

(2000--now) A calculus for concurrent programs.

With Prof. Jim Woodcock, University of York, and Prof. Augusto Sampaio, we proposed and formalised Circus: a refinement language that combines two popular notations, Z and CSP; its semantics is based on the Unifying Theories of Programming (UTP). We are currently working on tools and extensions of Circus. We have established the foundations of Circus, made progress on a timed and an object-oriented language, and addressed industrial case studies. Detailed information about Circus, including all the associated projects and publications can be found in its website; there we also list our sponsors and main collaborators.  

In 2002, I moved to England in the hope to intensify my collaboration with industry. In 2003, I was awarded a Royal Society Industry Fellowship which allowed me to work closely with QinetiQ. Together, we have proposed techniques that make the use of Circus appealing to industry: we have taken the language and its semantics forward to support new techniques for verification of control systems. We are now addressing tool development and widening of the scope of our techniques to cover a larger number of system specifications and programs.

Interaction with industry has also awakened my interest in testing and its relationship to refinement.

(2006--now) Testing based on Circus.

With Prof. Marie-Claude Gaudel, from the Universite de Paris-Sud, we have been exploring the use of Circus to support a practical test-case generation technique. Our objective is to combine and extend current techniques to support testing of large-scale state-rich reactive systems.

Groups

Previous projects