Séminaires
Séminaire du 18 Juin 2010
Lieu
LIPN, amphi Darwin, bâtiment Galilée: comment y aller
Programme
14h00-15h00: Lori A. Clarke, Laboratory for Advanced Software Engineering Research, CS department, Univ Massachusetts, "Hiding the Formalism in Formal Methods"
Abstract: Despite great advances, formal verification is still not widely applied to software systems. Model checking approaches have lowered the barrier to using formal verification, but their use is still largely restricted to specialists. There are two major difficulties that are holding back more widespread use of model checkers: considerable insight is needed to formulate the abstract model that is to be analyzed so as to reduce the size of the state space that must be explored, and it is difficult for practitioners to formulate precise specifications of the properties that are to be verified. This talk will describe FLAVERS and PROPEL, two systems that the LASER team is developing to address both of these problems. FLAVERS (FLow Analysis VERification System) uses a relatively novel approach for automatically creating a concise model of the system to be analyzed and for automatically refining that model when necessary. The PROPEL (PROPerty ELucidation) system guides users in specifying properties to be verified by providing templates for commonly occurring property patterns. These templates highlight the different decisions that should be considered by the specifiers and can be viewed as both natural-language descriptions or as finite-state automata. This talk will present a high-level overview of both systems and report on some of our experiences and observations. .
15h00-15h30 : Mathieu Sassolas, LIP6 "Real Time Properties for Interrupt Timed Automata"
Abstract: Reasoning about the evolution of time in a system has been a flourishing subject since the introduction of Timed Automata (TA) and Stopwatch Automata (SWA) in the 1990's. SWA are much more expressive than TA, but suffer from undecidability of verification problems in the general case. Other subclasses of SWA have been introduced in the search for a trade-off between expressiveness and decidability. One of them, Interrupt Timed Automata (ITA) have been introduced to model multi-task systems with interruptions. In ITA, the real valued variables (with rate 0 or 1) are organized along priority levels. While reachability is undecidable with usual stopwatches, the problem was proved decidable for ITA. In this talk, we will present undecidability and decidability results obtained for verification of subsets of Timed CTL on ITA.