From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id DA9277F0EF for ; Wed, 27 Jan 2016 13:57:22 +0100 (CET) IronPort-PHdr: 9a23:YzSu0R/0PiZAh/9uRHKM819IXTAuvvDOBiVQ1KB90OMcTK2v8tzYMVDF4r011RmSDdqds6gP17KempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lRciK1Y/rj6ibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MdFVeD+fr8kZb1eFjUvdW4vt+PxshyW7BeO630aXy0/lBZSgkCRwQ37U5H3v23TsOZn1QGePNXwC74uD2fxp5x3QQPl3X9UfwUy93va35R9 Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Etienne.Andre@lipn.fr; spf=None smtp.mailfrom=Etienne.Andre@lipn.fr; spf=None smtp.helo=postmaster@mail.lipn.univ-paris13.fr Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of Etienne.Andre@lipn.fr) identity=pra; client-ip=194.254.163.35; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="Etienne.Andre@lipn.fr"; x-sender="Etienne.Andre@lipn.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of Etienne.Andre@lipn.fr) identity=mailfrom; client-ip=194.254.163.35; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="Etienne.Andre@lipn.fr"; x-sender="Etienne.Andre@lipn.fr"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail.lipn.univ-paris13.fr) identity=helo; client-ip=194.254.163.35; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="Etienne.Andre@lipn.fr"; x-sender="postmaster@mail.lipn.univ-paris13.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0BeAgBwvahWlyOj/sJIFhaDdm2IV7ItgWIYCocyOhIBAQEBAQEBARABAQEBAQgWB0+CLYIZJQ8BPgc2AgUWCwILAwIBAgFYBgIBAYgbCp44j1uPVgR7jVIHEQGCZwstE4EnBZZ7hUeID4RQhFeFU45DJwmBdVEjgTZpAQGHEoExAQEB X-IPAS-Result: A0BeAgBwvahWlyOj/sJIFhaDdm2IV7ItgWIYCocyOhIBAQEBAQEBARABAQEBAQgWB0+CLYIZJQ8BPgc2AgUWCwILAwIBAgFYBgIBAYgbCp44j1uPVgR7jVIHEQGCZwstE4EnBZZ7hUeID4RQhFeFU45DJwmBdVEjgTZpAQGHEoExAQEB X-IronPort-AV: E=Sophos;i="5.22,354,1449529200"; d="scan'208";a="199693901" Received: from mail.lipn.univ-paris13.fr ([194.254.163.35]) by mail2-smtp-roc.national.inria.fr with ESMTP; 27 Jan 2016 13:57:22 +0100 Received: from [192.168.43.143] (unknown [37.165.116.47]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) (Authenticated sender: andre@lipn.univ-paris13.fr) by mail.lipn.univ-paris13.fr (Postfix) with ESMTPSA id DEF5326180E for ; Wed, 27 Jan 2016 13:57:22 +0100 (CET) To: caml-list@inria.fr From: =?UTF-8?B?w4l0aWVubmUgQW5kcsOp?= Organization: LIPN Message-ID: <56A8BEB5.8080206@lipn.fr> Date: Wed, 27 Jan 2016 13:57:25 +0100 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:38.0) Gecko/20100101 Thunderbird/38.5.1 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Validation-by: etienne.andre@lipn.fr Subject: [Caml-list] =?UTF-8?Q?PhD_position_on_formal_verification_at_Univ?= =?UTF-8?Q?ersit=C3=A9_Paris_13_/_=C3=89cole_Centrale_Nantes_=28France=29?= ************************************************************ PhD position Title : Formal verification of parametric real-time systems with preemption Laboratory 1: LIPN, CNRS UMR 7030, Université Paris 13, Sorbonne Paris Cité, France Laboratory 2: IRCCyN, École Centrale Nantes, France Contact : Étienne André and Didier Lime application.phd.pacs@lipn.univ-paris13.fr ************************************************************ *** Full subject available at https://lipn.univ-paris13.fr/~andre/sujets/2016-PhD-PACS.pdf ************************************************************ Context of the subject ************************************************************ Real-time systems have become ubiquitous in the past few years. Some of them (automated plane and unmanned systems control, banking systems, etc.) are critical in the sense that no error must occur. Testing these systems can possibly detect the presence of bugs, but not guarantee their absence. It is thus necessary to use formal methods such as model checking so as to formally prove their correctness. Real-time systems are characterized by a set of timing constants, such as the reading period of a sensor on an unmanned aircraft system, the traversal time of a circuit by the electric current, or the delay before retransmitting data in a cellphone. Although numerous techniques to verify a system for one set of constants exist, formally verifying the system for numerous values of these constants can require a very long time, or even infinite if one aims at verifying dense sets of values. It is therefore interesting to use parameterized techniques, by considering that these constants are unknown, i.e. parameters, and synthesize a constraint on these parameters guaranteeing the system correctness. Parametric timed automata have been proposed to model and verify parametric timed systems, and tools such as Romeo and IMITATOR were developed to perform efficient analyses. This formalism extends finite state automata with clocks (real-valued variables) that are compared with parameters in linear inequalities. Parameter synthesis can also be used to study the "implementability" of a system, i.e. its robustness w.r.t. infinitesimal variations of the timing constants. The goal of this PhD is to: 1) study parameter synthesis for parametric timed automata and hybrid systems; 2) devise efficient algorithms reusing recent concepts such as the integer hulls; 3) implement all algorithms in state-of-the art tools. Keywords: Formal methods, model checking, real-time systems, parameter synthesis One or several of the following skills would be appreciated (though not compulsory): - formal methods; - model checking; - (parametric) timed automata, (parametric / timed) Petri nets; - C++ or OCaml programming. ************************************************************ Context: The PACS Project ************************************************************ This post-doctoral position is funded by national project ANR PACS (Parametric Analyses of Concurrent Systems) 2014--2019. ANR PACS involves four laboratories: LIPN (Paris 13), IRIF (Paris 7), IRCCyN (École Centrale Nantes) and LINA (Université de Nantes). In addition, Kim Larsen's group in Aalborg (Denmark) acts as a foreign partner. LIPN is a high-quality laboratory involving about 80 professors, associate professors and full-time researchers, and many more students. Université Paris 13 is located less than 30 minutes from central Paris. IRCCyN is a leading laboratory in the domain of cyber-physical systems and robotics, with about a hundred researchers. It is located in Nantes, on the west coast of France, two hours from Paris by a direct, high-speed train. ************************************************************ Conditions and Application ************************************************************ The PhD position is for three years, and can start anytime (the sooner the better), and in any case before October 1st, 2016. The monthly salary is 1400€ + an additional 250€ if teaching 64h/year (netto, but before income tax, about 5,5%). Local transportation fees (Paris métro) are subsidized by half by the employer. Applications shall be made by email to Didier Lime and Étienne André, enclosing a fully detailed curriculum, and any other relevant document (recommendations, etc.). Contact : Étienne André and Didier Lime application.phd.pacs@lipn.univ-paris13.fr