| the \emph{CompCert} project \cite{CompCert,BDL-fm06,Le-popl06}. There |
the \emph{CompCert} project \cite{CompCert,BDL-fm06,Le-popl06}. There |
| is also a rich body of work on the related approaches of |
is also a rich body of work on the related approaches of |
| \emph{translation validation} |
\emph{translation validation} |
| \cite{Pnueli98a,Pnueli98b,Ne-pldi00,\cite{ZaksPnueli08}}, |
\cite{Pnueli98a,Pnueli98b,Ne-pldi00,ZaksPnueli08}, |
| \emph{certifying compilation} |
\emph{certifying compilation} |
| \cite{NL-pldi98,Colby-etal-pldi00,BlechPoetzsch07}, and |
\cite{NL-pldi98,Colby-etal-pldi00,BlechPoetzsch07}, and |
| \emph{proof-carrying code} \cite{Ne-popl97,AF-popl00,FNSG-tlfi07}. |
\emph{proof-carrying code} \cite{Ne-popl97,AF-popl00,FNSG-tlfi07}. |
| However, an integratedly verified compiler, which is optimizing and |
However, an integratedly verified compiler, which is optimizing and |
| ensures non-functional program properties such as on time and space |
ensures non-functional program properties such as on time and space |
| ressources required by the compiled program is still |
resources required by the compiled program is still |
| missing. Complementary to these approaches are approaches focusing on |
missing. Complementary to these approaches are approaches focusing on |
| frameworks for verifying compiler optimizations |
frameworks for verifying compiler optimizations |
| \cite{781156,1040335,Kundu+09} or the verification of specific |
\cite{781156,1040335,Kundu+09} or the verification of specific |
| compiler optizations, such as the \emph{Lazy Code Motion} |
compiler optimizations, such as the \emph{Lazy Code Motion} |
| \cite{TristanLeroy09} or instruction scheduling |
\cite{TristanLeroy09} or instruction scheduling |
| \cite{TristanLeroy08}. By far more ambitious and a grand challenge for |
\cite{TristanLeroy08}. By far more ambitious and a grand challenge for |
| computing research is Tony Hoare's vision of a \emph{verifying |
computing research is Tony Hoare's vision of a \emph{verifying |
| compiler} which proves properties of the translated program |
compiler} which proves properties of the translated program |
| \cite{Hoare03}. |
\cite{Hoare03}. |
| |
|
| \emph{Resource analysis}, especially worst-case execution time analysis $($WCET$)$} for real-time systems, which are often safety-critical, is a vibrant field of research in academia and industry and of fast growing economical relevance, |
\emph{Resource analysis}, especially worst-case execution time analysis $($WCET$)$ for real-time systems, which are often safety-critical, is a vibrant field of research in academia and industry and of fast growing economical relevance, |
| especially in the avionics and automotive industry. A survey on |
especially in the avionics and automotive industry. A survey on |
| state-of-the-art tools and methods for WCET analysis has recently been |
state-of-the-art tools and methods for WCET analysis has recently been |
| given by Wilhelm et al.~\cite{Wilhelm:TECS2008}. The outcomes of the |
given by Wilhelm et al.~\cite{Wilhelm:TECS2008}. The outcomes of the |
| providing hints on resource consumption and (2) the compiler to |
providing hints on resource consumption and (2) the compiler to |
| optimize for resource consumption. In our previous work we focused on |
optimize for resource consumption. In our previous work we focused on |
| compiler support for |
compiler support for |
| \emph{worst-case execution time analysis $($WCET$)$} \cite{Prantl:WCET2009,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657}. Based on this work and expertise we will extend this research towards |
\emph{worst-case execution time analysis $($WCET$)$} \cite{Prantl:WCET2009,Prantl:WLPE2008,prantl_et_al:DSP:2008:1661,kirner_et_al:DSP:2008:1657}. Based on this work we will extend this research towards |
| other quantitive aspects of resource consumption, especially storage |
other quantitive aspects of resource consumption, especially storage |
| usage, towards these two global objectives, using the programming |
usage, towards these two global objectives, using the programming |
| environment used there as testbed for implementation |
environment used there as testbed for implementation |
| {\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 & verified compilation & 4 years \\ |
NN2 & PhD & verified compilation & 4 years \\ |
| NN3 & PhD & Resource analysis & 4 years \\ |
NN3 & PhD & resource analysis & 4 years \\ |
| \hline |
\hline |
| \end{tabular} |
\end{tabular} |
| |
|
| Links to specification and modeling of timing properties, to execution |
Links to specification and modeling of timing properties, to execution |
| models, hardware and software models. |
models, hardware and software models. |
| \item PP Composition and Predictability in RES Architectures |
\item PP Composition and Predictability in RES Architectures |
| [E182/Puschner]: Links to hard- and software models for time |
[E182.1/Puschner]: Links to hard- and software models for time |
| predictable systems, verification of timing behaviour. |
predictable systems, verification of timing behaviour. |
| \item PP Formal Verification for Robustness [E184/Veith]: Links to software |
\item PP Formal Verification for Robustness [E184/Veith]: Links to software |
| model-checking and testing of code (on source code and intermediate |
model-checking and testing of code (on source code and intermediate |
| code levels), support for program analysis and transformation. |
code levels), support for program analysis and transformation. |
| \item PP Modeling \& Analysis of Robust Distributed Systems [E182/Schmid]: |
\item PP Modeling \& Analysis of Robust Distributed Systems [E182.2/Schmid]: |
| Links to functional and non-functional system requirements, |
Links to functional and non-functional system requirements, |
| distribution, concurrency. |
distribution, concurrency. |
| \end{itemize} |
\end{itemize} |
