Agenda: We start at 9h50 am.

• 09h50 - 10h00: Alain Girault (INRIA Grenoble -- Spades team): Welcome and introduction.

• 10h00 - 11h00: Hokeun Kim (UC Berkeley, USA -- Ptolemy group): Current research topics and status of PRET at UC Berkeley.

  Recently, there are roughly four ongoing research topics of PRET at UC Berkeley. A new intermediate layer of abstraction called PRETIL (PRET Intermediate Language) to connect PRET ISA and higher level languages is being researched. FlexPRET, a new PRET machine architecture that supports flexibility in thread scheduling has been developed to achieve higher throughput compared to PTARM. To overcome limitations of static scratchpad memory allocation methods, we are also working on WCET-aware dynamic scratchpad memory management. Precise clock synchronization on PRET, which is the latest research topic in our group, is expected to enable extension of precision timed execution for distributed time-critical systems.

• 11h00 - 12h00: Sidharta Andalam (TUM CREATE, Singapore -- Embedded Systems research project RP3): Precise Timing Analysis for Direct-Mapped Caches.

  Safety-critical systems require guarantees on their worst-case execution times. This requires modelling of speculative hardware features such as caches that are tailored to improve the average-case performance, while ignoring the worst case, which complicates the WCET analysis problem. Existing approaches that precisely compute WCET suffer from state-space explosion. In this talk, we present a novel cache analysis technique for direct-mapped instruction caches with the same precision as the most precise techniques, while significantly improving analysis time. This improvement is achieved by analysing individual control points separately, and carrying out optimisations that are not possible with existing techniques.

• 12h00 - 13h00: Lunch

• 13h00 - 14h00: Eugene Yip (U. of Auckland, New Zealand -- Embedded Systems group): Parallel Programming and Timing Analysis on Embedded Multicores.

• 14h00 - 15h00: Michael Mendler (U. Bamberg, Germany -- Pretsy project): Constructive Boolean circuits and the exactness of timed ternary simulation.

  Cyclic boolean systems, such as those arising in asynchronous circuits the semantics of synchronous programming languages, do not admit a unique canonical execution semantics. Instead, different approaches impose different restrictions on their stabilization behavior. This talk concerns the class of constructive circuits, for which signals settle to a unique value in bounded time, for any input, under a simple conservative delay model, called the up-bounded non-inertial (UN) delay.

  The main result is that ternary simulation decides the class of constructive circuits. It shows that three-valued algebra is able to maintain correct and exact stabilization information under the UN-delay model, which thus provides an adequate electrical interpretation of ternary algebra, which has been missing in the literature. Previous work on combinational circuits used the up-bounded inertial (UI) delay to justify ternary simulation. It can be shown that the match is not exact and that stabilization under the UI-model, in general, cannot be decided by ternary simulation.

  As the corner-stone of our main results we introduce UN-Logic, an axiomatic specification language for UN-delay circuits that mediates between the real-time behavior and its abstract simulation in the ternary domain. We present a symbolic simulation calculus for circuit theories expressed in UN-logic and prove it sound and complete for the UN-model. This provides, for the first time, a correctness and exactness result for the timing analysis of cyclic circuits such as the timed extension of Malik's or Brzozowski and Seger's pure ternary algorithm or the timed algorithm proposed by Riedel and Bruck, which were not formally linked with real-time execution models.

• 15h00 - 16h00: Joaquin Aguado (U. Bamberg, Germany -- Pretsy project): Is timing analysis a refinement of causality analysis?

  We ask this question by means of examples constructed from a game-theoretic approach for the semantics of Esterel combined with an interface algebra for timing analysis.

• 16h00 - 17h00: Open discussions.