home > publications > Z > Formal Methods for Industrial Products

Susan Stepney and David Cooper.
Formal Methods for Industrial Products.

In Jonathan P. Bowen, Steve Dunne, Andy Galloway, Steve King, editors, ZB2000: First International Conference of B and Z Users, York, UK, August 2000 . LNCS 1878:374-393. Springer, 2000.

Abstract:

We have recently completed the specification and security proof of a large, industrial scale application. The application is security critical, and the modelling and proof were done to increase the client's assurance that the implemented system had no design flaws with security implications. Here we describe the application, specification structure, and proof approach.

One of the security properties of our system is of the kind not preserved in general by refinement. We had to perform a proof that this property, expressed over traces, holds in our state-and-operations style model.

More on the

Full paper : PDF 285K 

@inproceedings(SS-ZB2000b,
  author = "Susan Stepney and David Cooper",
  title = "Formal Methods for Industrial Products",
  pages = "374--393",
  crossref = "ZB2000"
)

@proceedings(ZB2000,
  title = "ZB2000: First International Conference of B and Z Users,
           York, UK, August 2000",
  booktitle = "ZB2000: First International Conference of B and Z Users,
               York, UK, August 2000",
  editor = "Jonathan P. Bowen and Steve Dunne and Andy Galloway and Steve King",
  series = "LNCS",
  volume = 1878,
  publisher = "Springer",
  year = 2000
)