Known "Z notation" applications?

Question

I was just remembering back my university classes and was wondering to know if anyone out here even used the "Z notation" in a professional environment. I honestly must say that it was the single most boring class that I have ever attended in my life. Maybe because of the teacher, but at the time we really all thought it was a big waste of time. I might have been wrong, which is why I'd like to hear you about it.

If you are using it or some derived language (Z++), I'd just like to know how is it useful for you. Just curious to know some commonly-known applications of Z or your application.

For those who are not familiar : http://staff.washington.edu/jon/z/z-examples.html

Stacte

I suspect it only could really get a field day in automotive control systems (factory, marine, space exploration, robotics, and other specialist areas) where there is less of a focus on dynamic memory allocation: not an area where Z and perhaps anything imperative based excels. Anyone know of apps built or at least designed with Z in those areas? I remember reading IBM used Python for some control systems but I have never read a newspaper magazine atricle about companies using Z. – Abib

I'd be interested in knowing more about this. I was under the impression that Z was sort of an academic language, and industries concerned with correctness (safety-critical) had their own languages and tools. – Handspike

Answer 1

It's worth looking at the B Method (http://en.wikipedia.org/wiki/B-Method). It's a slightly more pragmatic descendent of Z. The idea is that you can actually discharge a bunch of proof obligations through refinements steps (with the help of a theorem prover that is hiding behind the scenes) and then eventually generate code directly from your specification. I believe it has been used in a number of "real world" projects.

Skutchan

Answer 2

Z is (as you pointed out) a specification notation and not a programming language intended to facilitate formal verification.

One of the larger (publicly known) projects specified using the notation was the protocol used in the Mondex smart card platform. There was recently a revival to determine the correctness of the original manual proofs with mechanical checking by multiple teams that included verification of the original Z specifications. Not surprisingly, no new fundamental errors were detected, although a number of assumptions were shown invalid by most of the teams.

The National Security Agency Tokeneer project was specified in Z before implementation in the Spark Ada subset.

Given the expressiveness of the notation it is unlikely that it will be extended. This would also make proofs more complex and be counter-productive.

Unthankful

gresham.ac.uk/lectures-and-events/… (2nd May 2017) covers this as well – Harlot

Answer 3

I first encountered Z notation when I read that XCB (a replacement for the original Xlib API in X11) was proven correct with Z-notation .

Pedant

Answer 4

The Web Services Description Language (WSDL) was developed using the Z notation. You can find the specification with the Z notation here: http://www.w3.org/TR/wsdl20/wsdl20-z.html. The specification states that

The Z Notation was used to improve the quality of the normative text that defines the Component Model, and to help ensure that the test suite covered all important rules implied by the Component Model.

Disputatious

Answer 5

I had to do Z back in uni! Brings back memories, if you have a Linux install handy try this application CADiZ...

Eleaseeleatic

Answer 6

'Z++' is called object-Z. I haven't been active in Z since the early-'90s (working in part on a Windows port of CADiZ, which appears to have vanished), so have no idea if its current community, but some more recent papers have been published on using object-Z to formalise UML.

Repute