This paper demonstrates the use of model-checking based verification technology to establish safety critical properties for an industrial avionics application. The verification technology is tightly interated with the Statemate system of i-Lpgix Inc., USA. Key features of this technology are its scalalability to complete system verification, the powerful debugging capabilities, graphical entry for safety critical properties, and the capability to re-use verification results for design components. The paper describes the application, the Statemate verification environment, and its use to establish safety critical properties of a British Aerospace application. The technical focus is on the use of abstraction techniques, allowsing to focus verification on aspects of the design relevant to the propety under investigation.
展开▼
