A case study of specification and verification using JML in an avionics application

James J. Hunt, Peter Schmitt, Isabel Tonin, Claus Wonnemann, Eric Jenn, Stéphane Leriche


11 Oct 2006
JTRES'06 - The 4th International Workshop on Java Technologies for Real-time and Embedded Systems, Paris, France



The literature for deductive formal verification is quite rich; however, very few case studies have been done. The authors present a case study of using deductive formal verification of a navigation system from the avionics domain. Both writing the specifications and their verification with a runtime assertion checker and KEY, a tool using automatic theorem proving techniques for verifying JAVA programs, are covered.

Download: PDF at ACM Digital Library