| %\emph{Informal description of the purpose of the PP (3-5 lines)} |
%\emph{Informal description of the purpose of the PP (3-5 lines)} |
| Every embedded system consists of software which is written in a high |
Every embedded system consists of software which is written in a high |
| level language, compiled to machine language and executed on a |
level language, compiled to machine language and executed on a |
| processor. For robust embedded systems new verified compilation |
processor. For robust embedded systems new verified compilation, |
| techniques are necessary to optimize for performance, power, space, |
simulation and specification methods are necessary to optimize for |
| concurrency and reliability. |
performance, power, space, concurrency and reliability. |
| |
|
| \subsubsection*{State of the art and related work:} |
\subsubsection*{State of the art and related work:} |
| %\emph{Briefly describe the scientific state of the art (20-30 lines)} |
%\emph{Briefly describe the scientific state of the art (20-30 lines)} |
| %to also describe and (coarsely) quantify the resources (staff, cost of |
%to also describe and (coarsely) quantify the resources (staff, cost of |
| %special equipment) required for this work in a table. (20-30 lines)} |
%special equipment) required for this work in a table. (20-30 lines)} |
| |
|
| |
The project is divided into three work packages. |
| |
|
| |
\paragraph*{WP1 - Compilation and Simulation Techniques for Reliability} |
| |
|
| (1) Specification and efficient simulation of reliable processors (partial redundancy, |
(1) Specification and efficient simulation of reliable processors |
| ECC, lockstep etc) and compiler optimizations to exploit/balance reliabiliy features. |
(partial redundancy, ECC, lockstep etc) and compiler optimizations to |
| Connection with CESAR NN1 |
exploit/balance reliabiliy features. Connection with CESAR NN1 |
| |
|
| (2) translation verification, specification of semantics of IRs solving |
\begin{itemize} |
| subproblems. NN1 + NN2 |
\item Specification method to specify an energy consumption model in |
| |
a processor specification. |
| |
\item Specification method for redundancy and error correction in the |
| |
processor specification |
| |
\item Specification method for fault injection and fault checking in |
| |
the processor specification |
| |
\item Generation of optimized instruction set simulators from the |
| |
processor specification |
| |
\item Generation of optimizing compilers from the processor specification |
| |
\item Research into new compiler optimizations to increase reliability by |
| |
pure software solutions, mixed hardware/software solutions and |
| |
balancing performance, code space, reliability and energy consumption |
| |
\item Research of correctness proofs and validation of the new optimizations |
| |
|
| |
\end{itemize} |
| |
|
| |
\paragraph*{WP2 - Verified Compilation} |
| |
|
| |
translation verification, specification of semantics of IRs solving |
| |
subproblems. |
| |
|
| |
\paragraph*{WP3 - Worst Case Ececution Time Analysis} |
| |
|
| (3) WCET NN3 |
WCET |
| |
|
| |
|
| \begin{tabular}{llll} |
\begin{tabular}{llll} |
| |
\\ |
| \hline |
\hline |
| {\bf Pos} & {\bf Type} & {\bf Description} & {\bf Duration} \\ |
{\bf Pos} & {\bf Type} & {\bf Description} & {\bf Duration} \\ |
| NN1 & PhD & reliable compilation / simulation & 4 years \\ |
NN1 & PhD & reliable compilation / simulation & 4 years \\ |
| NN2 & PhD & compiler verificationi & 4 years \\ |
NN2 & PhD & verified compilation & 4 years \\ |
| NN3 & PhD & WCET & 4 years \\ |
NN3 & PhD & WCET & 4 years \\ |
| \hline |
\hline |
| \end{tabular} |
\end{tabular} |
