[isabelle] Ph.D. Position at TU Berlin

Ph.D. Position in Research Project at TU Berlin on
Verification and Transformation of Embedded Systems (VATES)
Prof. Dr. Sabine Glesner, Technical University of Berlin


The aim of the VATES project, funded by the German Research Foundation (DFG), is the development of methods for the construction and verification of embedded real-time systems. Besides the complexity of such systems, a particular challenge is to cope with concurrency aspects and real-time requirements. A distinguishing feature of the VATES project is that we consider the whole development chain from abstract specifications through source code down to compiler-generated executable machine code. To ensure the correctness of our proofs and to gain a high degree of automatization, the verification is carried out with machine assistance, especially model checkers, SAT/SMT-solvers, and mechanical provers (like the interactive theorem prover Isabelle/HOL).

In the first phase of the VATES project, we developed a novel approach that allows us to formally relate an abstract process-algebraic specification formulated in the timed process calculus Timed CSP with its implementation given in the LLVM compiler intermediate representation. Using this relation, we are able to verify safety, liveness, and timing properties on the level of Timed CSP and transfer them to the level of executable code.

In the second phase of VATES, we extend our methodology in two directions. First, we aim at supporting the verification of multicore systems, which are more and more used in the context of embedded systems. To this end, we include directives that guide the transformation for multicore target architectures into our methodology on the specification level. These can then be exploited in subsequent verification steps. Second, our methodology is extended such that adaptive systems (which dynamically restructure themselves in changing environments) can be specified, verified, and transformed into executable, semantically equivalent code.

As a case study, we use the embedded real-time operating system BOSS, which was developed by Fraunhofer FIRST (Berlin). It is employed, for example, in satellites, medical applications and an electronic lottery system. Furthermore, it is well suited for verification purposes because of its comparatively simple structure and its relatively small size. In this phase, BOSS is extended to support multicore architectures and to directly include mechanisms that support adaptivity. Based on this, the methods to be developed are evaluated in the context of a practice-relevant case study.


The Technical University of Berlin is seeking for a researcher who will carry out research on methods for the design and verification of safety-critical real-time systems in the VATES project. The applicant should hold a Master's degree or equivalent in computer science, mathematics or similar field of study. The project will run for approximately 3 years and provides the opportunity to receive a Ph.D. during this period. To ensure equality of opportunity between men and women, applications from women with the relevant qualification are encouraged. Handicapped people with equal qualifications will be preferred.

For additional information concerning the VATES project and application, please visit our website: http://www.pes.tu-berlin.de/menue/forschung/projekte/vates2_-_verification_and_transformation_of_embedded_systems/parameter/en/
or contact us by email: sabine.glesner at tu-berlin.de

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.