My PhD research was mainly concerned with handling inconsistencies in Z specifications. I applied non-classical logics, such as paraconsistent logics, in order to allow reasoning about specifications in the presence of inconsistency. Related to this is also the problem of undefinedness. We considered undefinedness as a possibility to give the specifier more freedom while writing specifications.
Previously I investigated the degree of support that can be given to the process of living with inconsistencies in Z specifications, rather than eradicating inconsistencies early in the development process. I applied Anthony Hunter’s quasi-classical logic to analyse inconsistent Z specifications. As part of my research, I am also concerned with the process of refinement of inconsistent Z specifications.
Inconsistency and Underdefinedness in Z Specifications. Ralph Miarka. Ph.D. Thesis, University of Kent, Canterbury, Kent CT2 7NF, UK, December 2002.
(Postscript (1.5MB): Thesis.ps.gz, PDF (157MB): Thesis.pdf, PDF ZIP’ed (26MB): Thesis.pdf.zip)
Handling Inconsistencies in Z using Quasi-Classical Logic. Ralph Miarka, John Derrick and Eerke Boiten. In Didier Bert, Jonathan P. Bowen, Martin C. Henson, Ken Robinson, editors, ZB2002: Formal Specification and Development in Z and B / Second International Conference of B and Z Users, volume 2272 of Lecture Notes in Computer Science, pages 204-225. Springer-Verlag Berlin, January 2002.
(Postscript: ZB2002.ps.gz, PDF (15MB): ZB2002.pdf, PDF ZIP’ed (2.5MB): ZB2002.pdf.zip)
Guards, Preconditions, and Refinement in Z. Ralph Miarka, Eerke Boiten, and John Derrick. In Jonathan P. Bowen, Steve Dunne, Andy Galloway, and Steve King, editors, ZB2000: Formal Specification and Development in Z and B / First International Conference of B and Z Users, volume 1878 of Lecture Notes in Computer Science, pages 286-303. Springer-Verlag Berlin, August 2000.
(Postscript: ZB2000.ps.gz, PDF (11MB): ZB2000.pdf, PDF ZIP’ed (2MB): ZB2000.pdf.zip)