Jean-Pierre lets us know that he is still looking for an excellent master student to start a PhD in Rennes on the following topics (in French, sorry).
TRACK: typage par raffinement et algébre de contrats des kernels modulaires Un système cyber-physique (automobile, avionique, automatisme industriel, etc) est constitué d'une architecture matériel-logiciel controllant un phénomène physique. Sa conception repose sur des modèles mathématiques spécifiques assurant une représentation fidèle du phénoméne physique, conforme des composants matériels (capteurs, réseau, calculateur, actuateurs), et déterministe du logiciel. Ces modèles sont, a priori, hétérogènes, car leurs domaines de définition en fonction du temps sont usuellement distinct: temps logique pour le logiciel, temps réel discret pour l'architecture, temps continu pour la physique. Pourtant, un convergence de travaux en logique mathématique: logique d'ordre supérieure, logique temporelle, logique dynamique et différentielle, offre la perspective de pouvoir raisonner sur de tels ensembles. Le projet TRACK vise à utiliser la théorie du typage par raffinement comme support analytique à la vérification modulaire et à la synthèse de controleurs (ou de moniteurs, ou de code défensif) de systèmes (cyber-physiques), ou plus exactement d'application-systèmes ou unikernels: logiciel de controle et librairies système. Le typage par raffinement consiste à associer les eléments d'un système: fonction, service, composant matériel, voir physique, avec un type caractérisant son état et ses entrées-sorties (une monade), ainsi qu'une proposition logique, précisant sémantiquement ce domaine et la transformation d'état réalisée par la fonction. L'idée est ici de formuler ainsi le contrat d'un elément (hypothèse et garantie) en logique de séparation (pré- et post-conditions). L'objectif du doctorat est de développer une telle algèbre de contrat pour représenter de manière analytique les propriétés de modules logiciels (possiblement inférées par inférence de type, par analyse statique) et d'eléments matériels (par la spécification formelle de leur documentation, faute de mieux). Ensuite, il est question de vérifier la bonne composition de ces eléments, comme conforme aux contrats présentés, par la génération d'obligation de preuve en, e.g. logique de 1er ordre modulo théorie (preuve automatique), en logique d'ordre supérieur (preuve interactive), voir en logique dynamique (différentielle). En complément, lorsque la vérification ne peut pas être complête (ex.: interface attendu d'un composant matériel, physique) on utilisera alors des techniques de synthèse de controleurs (propriétés temporelles) ou bien la génération de moniteurs ou de code défensif (propriétés de 1er ordre) afin de garantir le respect des contrats pendant l'exécution du système. L'ordonnancement temp-réel peut être dans ce cadre vu comme un cas particulier de synthèse de controleur. Un modèle d'architecture, sous la forme d'une hiérarchies de graphe, permetttra de mettre en relation les composants hétérogènes du système, vus au travers de l'abstraction de leurs contrats. Les études théoriques et leur mise en oeuvre, au moyen de preuve de concept, attendues dans ce doctorat, ouvre à de nombreuse perspectives et application dans le domaine très général des systèmes cyber-physiques. En particulier, il ouvre à la capacité d'une intégration virtuelle de ces systèmes, la vérification a priori de leur bon fonctionnement sur la base de modèles, avant même que le système proprement dit soit fabriqué et testé, résultant en des gains de productivité potentiellement considérables. On Sun, May 7, 2017 at 1:16 PM, Catalin Hritcu <catalin.hri...@gmail.com> wrote: > Dear F* folks, > > Jean-Pierre Talpin, one of our Inria colleagues who is located in > Rennes (in CC), is looking for PhD students on several refinement > types projects that could include the use of F* and Low*. If you know > anyone who could be interested in this please let them know. > > Regards, > Catalin > > PhD - Refinement types for stream processing languages > https://www.inria.fr/en/centre/rennes/overview/offers/phd/campaign-2017/(view)/details.html?id=PNGFK026203F3VBQB6G68LOE1&LOV5=4509&LOV28=7840&LG=EN&Resultsperpage=10&nPostingID=11169&nPostingTargetID=17755&option=52&sort=DESC&nDepartmentID=28 > > PhD - Refinement types for cyber-physical system design > https://www.irisa.fr/fr/offres-theses/refinement-types-cyber-physical-system-design > > PostDoc - From liquid types to certified code (deadline passed) > https://www.inria.fr/en/institute/recruitment/offers/post-doctoral-research-fellowships/post-doctoral-research-fellowships/(view)/details.html?id=PNGFK026203F3VBQB6G68LOE1&LOV5=4508&LG=EN&Resultsperpage=20&nPostingID=11122&nPostingTargetID=17707&option=52&sort=DESC&nDepartmentID=19 _______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
