Email Gateway (Aug 18 2022 at 18:53): Email Gateway (Aug 18 2022 at 18:53):From: Thomas Göthel <tgoethel@cs.tu-berlin.de>
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
our contact us by email: sabine.glesner@tu-berlin.de
Email Gateway (Aug 18 2022 at 18:54):From: Thomas Göthel <tgoethel@cs.tu-berlin.de>
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
our contact us by email: sabine.glesner@tu-berlin.de
Email Gateway (Aug 18 2022 at 19:14):From: Thomas Göthel <tgoethel@cs.tu-berlin.de>
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@tu-berlin.de
Last updated: Nov 21 2024 at 12:39 UTC