Centre Fédéré en Vérification






Seminars for 2006-2007

  • Using Temporal Logic to Analyse Temporal Logic: A Hierarchical Approach Based on Intervals
    • Speaker: Ben Moszkowski (Software Technology Research Laboratory, de Montfort University, Leicester, UK)
    • Time: 1:30 PM
    • Date: June, 8th
    • Place: Solvay room, NO building, 5th floor
    • Abstract: Temporal logic has been extensively utilized in academia and industry to formally specify and verify behavioural properties of numerous kinds of hardware and software. We present a novel way to apply temporal logic to the study of a version of itself, namely, propositional linear-time temporal logic (PTL). This involves a hierarchical framework for obtaining standard results for PTL, including a small model property, decision procedures and axiomatic completeness. A large number of the steps involved are expressed in a propositional version of Interval Temporal Logic (ITL) which is referred to as PITL. It is a natural generalization of PTL and includes operators for reasoning about periods of time and sequential composition. Versions of PTL with finite time and infinite time are both considered and one benefit of the framework is the ability to systematically reduce infinite-time reasoning to finite-time reasoning. The treatment of PTL with the operator Until and past time naturally reduces to that for PTL without either one. The interval-oriented methodology differs from other analyses of PTL which typically use sets of formulas and sequences of such sets for canonical models. Instead we represent models as time intervals expressible in PITL. The analysis furthermore relates larger intervals with smaller ones. Being an interval-based formalism, PITL is well suited for sequentially combining and decomposing the relevant formulas. Consequently, we can articulate issues of equal significance in more conventional analyses of PTL but normally only considered at the metalevel. A good example of this is the existence of bounded models with periodic suffixes for PTL formulas which are satisfiable in infinite time. We also describe decision procedures based on binary decision diagrams and exploit some links with finite-state automata.

      Beyond the specific issues involving PTL, the research is a significant application of ITL and interval-based reasoning and illustrates a general approach to formally reasoning about sequential and parallel behaviour in discrete linear time. The work also includes some interesting representation theorems. In addition, it has relevance to hardware description and verification since the specification languages PSL/Sugar (IEEE Standard 1850) and 'temporal e' (part of IEEE Standard 1647) both contain temporal constructs concerning intervals of time as does the related SystemVerilog Assertion language contained in SystemVerilog (IEEE Standard 1800), an extension of the IEEE 1364-2001 Verilog language.

  • FNRS Contact Group Meeting on Synthesis and Verification

    • Date: October, 18th
    • Place: ULB, Campus plaine, building NO, level 9, local NO9.06
    The program of the day is given hereunder. Those who want to participate to the meeting must send before friday october 13 an email to : Jean-François Raskin (jraskin@ulb.ac.be) with subject : « FNRS day registration ». The lunch will be offered only to those that are registered.
    • 9h20 : Welcome.
    • 9h30-10h15 : Bernard Lambeau et Christophe Damas (UCL) Scenarios, Goals, and State Machines : a Win-Win Partnership for Model Synthesis
    • 10h15-10h45 : Coffee Break
    • 10h45-11h45 : Invited talk : Nicolas Markey (LSV - ENS de Cachan) Verification of Multi-Agent Systems with ATL . Abstract : Alternating-time Temporal Logic (ATL) is an extension of the well- known branching-time logic CTL geared towards the specification and verification of strategic abilities of (coalitions of ) agents to enforce some ob jective. During this talk, I will introduce the framework of multi-agent systems, and present some results on the expressiveness and complexity of ATL.
    • 11h45-14h: Lunch break
    • 14h-14h45 : Michel Sintzoff (UCL) Symbolic generation of optimal discrete systems
    • 14h45-15h30 : Martin De Wulf (ULB) A Lattice Theory for Solving Games of Imperfect Information
    • 15h30-16h : Coffee break
    • 16h-16h45 : Gilles Geeraerts (ULB) An efficient algorithm to compute the coverability set of Petri nets
    • 16h45-17h30 : Axel Legay (ULg) Handling liveness properties in (omega)-regular model checking
  • Monitoring and Fault Diagnosis for Real-Time Systems
    • Speaker: Franck Cassez, IRCCyN, Nantes, France
    • Date: November, 24th
    • Place: to be announced
    • Abstract: In this talk we review the fundamental results for the monitoring and fault diagnosis problems for finite state systems and timed systems. We also address the following more advanced topics: optimal monitoring and fault diagnosis for finite state systems and fault diagnosis for timed systems using digital clocks. We conclude with some open problems and directions for future work.
  • UPPAAL Tiga -- Controller Synthesis for Real-Time Systems
    • Speaker: Kim G. Larsen, Aalborg University, Denmark
    • Date: December, 8th
    • Place: Solvay room, NO building, 5th floor
    • Abstract: UPPAAL Tiga is a recent branch of the real-time verification tool UPPAAL allowing control programs to be synthesized from timed game automata models with respect to control purposes specified as CTL formulas. Thus both safety and reachability games are supported. The talk will present the efficient on-the-fly algorithm used for synthesizing winning strategies for timed games, emphasizing recent methods used for achieving signicant improvement of performance compared with the first implementation (CONCUR05). UPPAAL Tiga allows for winning strategies to be represented as BDD/CDDs useful for compact embedded control programs. In the talk we also show how UPPAAL Tiga itself may be used for checking refinements between timed games (useful in settings of partial observability) and how the on-the-fly algorithm UPPAAL-Tiga may be used (and extended) to generate testing strategies for real-time systems.
  • Subexponential algorithms for solving parity games
    • Speaker: Marcin Jurdziński, Universty of Warwick, United Kingdom
    • Date: Decembre, 15th (2PM)
    • Place: Plaine campus, NO building, 5th floor, room 2NO5.06
    • Abstract: Deciding the winner in a parity game is polynomial time equivalent to checking if a formula of the modal logic with fixpoint operators (aka. the modal mu-calculus) holds in a state of a Kripke structure. The exact computational complexity of the problem is an intriguing open problem: it is known to be in UP (unambiguous NP) and co-UP, but no polynomial time algorithm is known. This talk surveys a few recent algorithmic ideas which yield improved running time bounds for the problem. One is obtained by a reduction of parity games to the problem of finding the unique sink in a "unique sink orientation" of a hypercube and it yields a subexponential randomized algorithm. The other is a modification of a classical recursive algorithm for solving parity games that originates from the work of McNaughton and Zielonka and it yields a subexponential deterministic algorithm.
  • Monitoring and Fault-Diagnosis with Digital Clocks
    • Speaker: Franck Cassez, IRCCyN, Nantes, France
    • Date: Decembre, 15th (4PM)
    • Place: Plaine campus, NO building, 5th floor, room 2NO5.06
    • Abstract: We study the monitoring and fault-diagnosis problems for dense-time real-time systems, where observers (monitors and diagnosers) have access to digital rather than analog clocks. We show how, given a specification modeled as a timed automaton and a timed automaton model of the digital clock, a sound and optimal (i.e., as precise as possible) digital-clock monitor can be synthesized. We also show how, given plant and digital clock modeled as timed automata, we can check for the existence of a digital-clock diagnoser and, if one exists, how to synthesize it. Finally, we consider the problem of existence of a digital-clock such that a there is a digital-clock diagnoser.
  • A modest approach to practical formal methods
    • Speaker: Holger Hermanns (Saarland University)
    • Date: March, 9th
    • Place: Solvay room, NO building, 5th floor
    • Abstract: Stochastic timed systems and stochastic temporal logics have been proposed to express and check requiremnts like correctness, availability, survivability or performability of trustworthy real-time system designs. They are partially accompanied by model-checking algorithms which can be applied to certify these requirements on a component level.

      This talk gives an overview of recent achievements in this area. It will detail the achieved results in two related areas: After introducing the mathematical background and context, I will report on our efforts to link an industrial modelling tool to academic state-of-the-art model-checking algorithms. In a nutshell, we enable timed reachability analysis of uniform continuous-time Markov decision processes, which are generated from STATEMATE models. We give a detailed explanation of several construction, transformation, reduction, and analysis steps required to make this possible.

      With a slightly broader perspective, I am then going to introduce MoDeST (MOdeling and DEscription language for Stochastic Timed systems), a formalism to support (i) the compositional description of reactive systems' behavior while covering both (ii) functional and (iii) nonfunctional system aspects such as timing and quality-of-service constraints in a single compositional specification. This unique expressiveness has been exploited in three recent industrial case studies of rather different nature, ranging from (i) schedule synthesis and evaluation for a lacquer production plant, to (ii) energy efficiency assesment of ZigBee devices, and to (iii) dependability assessment of an emerging standard for future high-speed cross-European trains.

  • Development of Safe and Efficient Programs using Abstract Interpretation and the CiaoPP System
    • Speaker: Manuel Hermenegildo (Technical University of Madrid and University of New Mexico, Spain)
    • Date: May, 11th
    • Place: OF2070
    • Abstract: One of the fundamental challenges in program development, from large applications to embedded code, is to be able to develop, in the shortest time possible, programs that are efficient and correct. We argue that in order to achieve this goal, in addition to factors such as better programming languages, substantially improved functionality is needed from programming environments. We present a novel program development framework which uses "Abstract Interpretation" as a fundamental component. Abstract interpretation is a technique which has allowed the development of very sophisticated program analyzers and transformers, which are at the same time provably correct and highly practical. The framework that we present uses this type of program analysis to obtain information about the program. This information is then used to validate programs with respect to partial specifications written using assertions, to detect and locate bugs, to simplify run-time tests, to perform high-level program transformations (such as specialization, parallelization, or resource usage control), and to enrich mobile code with safety certificates. The system can reason with much richer information than, for example, traditional type declarations. This includes pointer aliasing, shapes, exceptions, determinacy, abounds on resource consumption (such as computational cost or sizes of data in the program), etc. CiaoPP, the preprocessor of the Ciao multi-paradigm programming system is an implementation of this framework and will be used to illustrate these ideas.



Tue Mar 27 16:29:00 CEST 2007