Post-doc position - IFSE working group (http://projects.laas.fr/IFSE/)
Title: Formal Contracts for a Component-Based Specification Language Profile: - Good knowledge of formal methods (concurrency semantics; temporal logics; ...). - Experience in specification and verification of critical systems . Duration: 12 to 18 months Scientific officers: - Silvano Dal Zilio (CNRS, LAAS) http://homepages.laas.fr/dalzilio/ - Jean-Baptiste Raclet (CNRS & Université Toulouse III, IRIT) http://www.irit.fr/~Jean-Baptiste.Raclet/ Contracts have recently been identified as key feature for the modular design of complex systems [1]. Basically, a contract explicitly handles pairs of properties of the form (A,G) where A represents assumptions on the environment of a component and G the guarantees provided by the component as long as its assumptions are met. From this simple concept, contract theories can be built addressing systems complexity design and certification while also managing heterogeneous requirements and cross-company risks. The objective of this position is to develop a contract-based theory in the context of the modeling language Fiacre [2], a component-based language developed at IRIT and LAAS. Fiacre is dedicated to the formal verification of real-time systems and can be used in the context of a model-checking toolbox for an extension of Time Petri Nets with data and priorities. The goal for defining a theory of contracts for Fiacre is to obtain new compositional verification methods for this specification language. We are also interested in using our model-checking toolbox in order to check or infer contracts on components. Practical information: this is a joint proposition between two Toulouse computer science labs: LAAS-CNRS and IRIT. Candidates are expected to be fluent in English or in French and should send a resume via email to [email protected] and [email protected]. Starting date is negotiable. The position is funded by RTRA STAE, the French space and aeronautics sciences & technologies fundation, as part of the IFSE project on formal system engineering. The expected gross salary is between 2500 and 3000 EUR. References: [1] Contracts for System Design. Albert Benveniste, Benoit Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, Philipp Reinkemeier, Alberto Sangiovanni-Vincentelli, Werner Damm, Thomas Henzinger, Kim G. Larsen. http://hal.inria.fr/hal-00757488/ [2] The Fiacre Language, http://projects.laas.fr/fiacre/ ---- [[ Petri Nets World: ]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]] [[ Mailing list FAQ: ]] [[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]] [[ Post messages/summary of replies: ]] [[ [email protected] ]]
