The Mobius Demonstrator Case Study
Nov. 15, 2010 – 6 years, 5 months ago, by woj
The Mobius Demonstrator Quiz Game has been annotated with JML to specify the so-called mildet navigation graph property. Then it has been verified with ESC/Java2.
The complete case study can be downloaded from:
The code is specified with JML annotations in the Java files of the project.
A thorough description of the case study can be found in the technical report:
Wojciech Mostowski and Erik Poll, Midlet Navigation Graphs in JML
This is about to be published in the 13th Brazilian Symposium on Formal Methods, SBMF2010 LNCS proceedings too.