Seminaire Oasis

Stephen Fickas

University of Oregon

Lundi 8 Avril 2002, salle ???

Title : Getting past "no": what to do when your model checker says nyet
Abstract :
the traditional view of formal analysis is that you turn up errors and then fix them, long before they make their way into code. I'd like to consider an alternative view: you turn up errors but then dismiss them. I will argue that this happens often in real systems. When an error is found through formal analysis (e.g., model checking), domain experts may say one of the following: (a) the error is unlikely and not worth dealing with, or (b) the error is inconsequential and not worth dealing with. My project looks at what we can do about errors that are dismissed in this way. In particular, we are interested in (1) identifying assumptions that are made during analysis, and (2) carrying them down to runtime for monitoring. Once we have assumption monitors in place, we can begin to imagine interesting uses in terms of failure handling/recovery and system adaptation. I will talk about my group's work with several case studies. Stephen Fickas Full Professor, Computer Science University of Oregon Eugene, OR http://www.cs.uoregon.edu/~fickas

Retour au sommaire / Back to schedule

Eric Madelaine

Last modified: Fri Feb 1 16:55:34 MET 2002