Formal Methods for Industrial Products

We have recently completed the specication 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 aws with security implications. Here we describe the application, specication structure, and proof approach. One of the security properties of our system is of the kind not preserved in general by renement. We had to perform a proof that this property, expressed over traces, holds in our state-and-operations style model.

• Type: Conference
• Year: 2000
• Where: ZUM
• Authors: Susan Stepney, David Cooper
• Keywords: Formal Methods, Industrial Scale Application, Security, Security Proof, ZUM 2000