Model Checking Programs




Park


Dynamic Analysis


The majority of work carried out 
in the formal methods community throughout the 
last couple of decades has (for good 
reasons) been devoted to special purpose languages 
designed to make it easier to experiment 
with mechanized formal methods such as theorem 
provers and model checkers. In this paper 
we argue that attention now should be 
focused on real programs written in modern 
programming languages. Our argumentation is as follows. 
First of all, programs will always contain 
errors in spite of the existence of 
careful designs. Many deadlocks and critical section 
violations for example are introduced at a 
level of detail which designs typically do 
not deal with, if the designs are 
made at all. Second, focusing on real 
programs will force the community to deal 
with very hard problems, and this may 
drive the research into new areas, combining 
formal methods, program analysis and testing. Third, 
and finally, modern programming languages are the 
result of decades of research, and are 
the result of good language design principles. 
Hence, they may even be good design 
languages. As added value can be mentioned 
the possibility of comparing and integrating different 
tools working on the same language, and 
the increased availability of case studies and 
programmers willing try and drive our research. 
We have developed a verification and testing 
environment for Java, Java PathFinder (JPF), which 
integrates model checking, testing and static analysis. 
Part of this work has consisted of 
building a new Java Virtual Machine that 
interprets Java bytecode. JPF uses state compression 
to handle big states, and it uses 
partial order reduction, slicing, abstraction, and runtime 
analysis techniques to reduce the state space. 
JPF has been applied to a real-time 
avionics operating system developed at Honeywell, illustrating 
an intricate error, and to a model 
of a space craft controller, illustrating the 
combination of abstraction, runtime analysis, and slicing 
with model checking.