SyVeRLo: Syntesis and Verification of Real-time Logics
PDR FNRS

Research goals

Ensuring the correctness of critical computer systems is imperative. Today, the use of formal methods is widely advocated as adequate methodologies to obtain the strong guarantees that are requested by critical applications. In the current state of the art, those methods can be split in two categories: verification and synthesis methods. Roughly speaking, verification techniques are a posteriori methods, which allow to detect bugs in already existing models of a controller; and synthesis techniques are a priori methods which outputs a model of the controller that is guaranteed to be correct by construction. The development of those two families of techniques is nowadays quite advanced when the models and properties are purely qualitative. Nevertheless in order to faithfully model computer systems and their specifications, real-time aspects are of capital importance. Unfortunately, the theoretical and practical results are still partial when real-time aspects of the system must be taken into account. In the untimed case, the success of verification and synthesis methods can arguably be attributed to the fact that they rely on (Büchi) automata as an adequate model to express the system's behaviours, and on powerful yet natural languages to specify the properties (e.g. LTL). In the timed case, and while timed automata are a well-established and well-studied automaton model, the picture is not so clear. Real-time extensions of LTL are either highly undecidable (MTL), or studied mainly from a theoretical point of view (ECL,MITL), and the algorithms to perform verification with those logics are not easily amenable to implementation. Thus, the present research project aims at defining efficient algorithmic techniques to solve verification and synthesis problems when the specification languages are real-time linear logics.

People

• Prof. Thomas Brihaye, Université de Mons, Mathématiques effectives.
• Prof. Gilles Geeraerts, Université libre de Bruxelles, Vérification et méthodes formelles.
• Mr. Hsi-Ming Ho, PhD, post-doc researcher, Université de Mons, Mathématiques effectives.