@inproceedingsBie1999, Author = {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.}, Title = {Formal Verification of an Avionics Application using Abstraction and Symbolic Model Checking}, Year = {1999}, Pages = {150-173}, Month = {01}, Editor = {Springer}, Publisher = {Springer}, Booktitle = {Towards System Safety - Proceedings of the Seventh Safety-critical Systems Symposium, Huntingdon, UK}, Organization = {Safety-Critical Systems Club}, type = {inproceedings}, note = {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., US}, Abstract = {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.} @COMMENTBibtex file generated on