From: Simon Foster via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
Applications are invited for a Research Associate to carry out research on
application of formal verification technology to safety assurance of
autonomous robots. This position will be funded by the EPSRC for three
years in the context of the recently awarded CyPhyAssure project.
You will assist in the development of a computerised platform for arguing
the safety of autonomous robots by application of multi-model based
assurance cases. We will build this platform within the Isabelle/HOL proof
assistant, and utilise the Structured Assurance Case Metamodel (SACM). The
platform, as conceived, will support formal modelling of individual modular
components of a robot and its environment, the combination of these models
to describe the overall system’s behaviour, the description of formal
requirements of the overall system, and decomposition and apportionment of
these requirements to the constituent models.
You will liaise with academic and the industrial partners and participate
in the writing of research papers. You will have a PhD in the area of
formal methods, experience in modelling and formal refinement, and
understanding of hybrid and/or probabilistic systems. You will have
substantial experience in the application of the Isabelle/HOL theorem
prover. Experience in the areas of assurance cases, safety processes, and
robotics are all highly desirable.
For more information on this position, please visit https://jobs.york.ac.uk/
wd/plsql/wd_portal.show_job?p_web_site_id=3885&p_web_page_
id=356469&p_vacancy=research-associate-university-of-york
Thanks,
-Simon Foster.
Last updated: Nov 21 2024 at 12:39 UTC