Formal Verification and Automated Testing for Diagnostic and Monitoring Systems

Bruno Dutertre, Cesar Munoz, John Rushby, Radu Siminiceanu and Ashish Tiwari

AIAA Guidance, Navigation and Control Conference, Honolulu HI, August 2008

AIAA paper 2008-6802

Abstract

Formal methods offer the unique benefit that it is possible to examine all possible circumstances within a given scope, rather than merely sample them as with testing and simulation. This is possible even when huge numbers of discrete possibilities must be considered, such as in fault scenarios, and in the presence of real-time and continuous behavior, and when both these sources of difficulty are combined. Formal methods achieve this by using symbolic methods of analysis, and it is the computational complexity of these symbolic methods that limits and complicates their application.

Recently, new methods and tools for symbolic analysis have been developed that are far more efficient and effective in practice than earlier methods. These include solvers for "satisfiability modulo theories" (SMT solvers) and methods for using these to analyze discrete and hybrid (i.e., mixed discrete and continuous) systems. In addition, new ways to apply these capabilities have been developed, such as their use for test generation, and controller synthesis, in addition to analysis.

In this paper, we outline these new methods, and describe a project to extend and apply them in combination to issues in verification and testing of diagnostic and monitoring systems.

PDF

BibTeX Entry

@string{aiaa = {American Institute of Aeronautics and Astronautics}}

@inproceedings{Rushby:GNC08-verification,
	AUTHOR = {Bruno Dutertre and C\'{e}sar Mu{\~{n}}oz and John Rushby
		and Radu Siminiceanu and Ashish Tiwari},
	TITLE = {Formal Verification and Automated Testing for Diagnostic
		and Monitoring Systems},
	BOOKTITLE = {AIAA Guidance, Navigation and Control Conference},
	YEAR = 2008,
	NOTE = {AIAA paper 2008-6802},
	ORGANIZATION = aiaa,
	ADDRESS = {Honolulu HI},
	MONTH = aug
}
Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page