Formal Verification of an Avionics Application using Abstraction and Symbolic Model Checking

Bienmüller, T. and Brockmeyer, U. and Damm, W. and Döhmen, G. and Eßmann, C. and Holberg, H. J. and Hungar, H. and Josko, B. and Schlör, R. and Wittich, G. and Wittke, H. and Clements, G.
Towards System Safety - Proceedings of the Seventh Safety-critical Systems Symposium, Huntingdon, UK
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 integrated with the Statemate system of I-Logix Inc., USA. Key features of this technology are its scalability 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, allowing to focus verification on aspects of the design relevant to the property under investigation.
01 / 1999
Safety-Critical Systems Club