Versions Compared


  • This line was added.
  • This line was removed.
  • Formatting was changed.


The PRETSY project is a project funded by the German Research Foundation (DFG HA 4407/6-1, ME 1427/6-1), running 2011 2012 - 20142015.


Embedded reactive real-time systems are ubiquitous today, and provide increasingly complex functionality for example in modern automotive, avionics or medical products. This rising complexity makes it important to apply high-level design approaches, which, however, traditionally make critical low-level aspects such as timing hard to control. This project investigates a novel, holistic approach for the design of timing-predictable, efficient reactive systems, which considers the modelling and programming level as well as the execution platform.

A key aim is to combine a formal semantical basis, which is provided by the synchronous model of computation and which results in predictable reactive control flow, with recent architectural developments that offer predictable timing at the instruction level. Compared to typical design approaches today, based on C-like languages and processors that optimise the average case at the expense of predictability, the objective is to reduce timing uncertainties at the control-flow level as well as the architectural level. On the practical side the project is developing a model-based design flow and tool chain for implementing timing-predictable, reactive systems, including a synchronous modelling and programming language, a compiler, a timing analyser, and a predictable execution platform derived from the Berkeley/Columbia PRET architecture.


  • 19th International Workshop on Synchronous Programming (SYNCHRON'12), Le Croisic, France. November 2012
  • Electrical Engineering Research Seminar “PRETzel Forum”  (PRETzel'14), Auckland University, New Zealand, January 2014.


[PDAY’13] Is timing analysis a refinement of causality analysis? (slides)

J. Aguado.

PRET Day (PDAY'13), Inria Grenoble Rhône-Alpes  France, March 2013.

Summary: 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. It has been recognised that the synchronous model of computation together with a suitable execution platform (precision-timed, or PRET architectures) facilitates system-level timing predictability. This talk discusses a logical and game-theoretic framework for capturing worst-case reaction time (WCRT) for Esterel-style synchronous reactive programming. This framework will provide a formal grounding for the WCRT problem, and allow to improving upon earlier heuristics by accurately and modularly characterising timing interfaces. This approach will not only allows verifying the correctness of WCRT analyses methods, but also will allow capturing functionality and timing together.


Summary: This poster describes Sequentially Constructive Charts (SCCharts), the visual language for specifying safety-critical reactive systems employed in the [PLDI’14] publication.


[SYNCHRON’13-1] Compiling SCCharts (and other Sequentially Constructive Programs) to Hardware and Software.


Summary: SCCharts extend SyncCharts with sequential constructiveness (SC) and other features. We developed a compilation chain that first, in a high-level compilation phase, performs a sequence of model-to-model transformations at the SCCharts-level such that they can be mapped directly to SC Graphs (SCGs). Then two alternative low-level compilation approaches allow mapping to hardware and software; the circuit approach generates a netlist, the priority approach simulates concurrency with interleaved threads.


[SYNCHRON’13-2] SCCharts – Sequentially Constructive Charts. (slides)


On the one hand this eases the compilation and makes it more robust because it reduces its complexity. On the other hand, using Extended SCCharts features, a modeler is able to abstract away complexity of his or her SCCharts model which increases robustness and readability of a model. This approach enables a simple yet efficient compilation strategy and aids verification and certification.


[SYNCHRON’13-3] Berry-Constructive Programs are Sequentially Constructive, or: Synchronous Programming from a Scheduling Perspective. (slides)


Summary: We introduce an abstract value domain I(D) and associated fixed point semantics for reasoning about concurrent and sequential variable valuations within a synchronous cycle-based model of computation. We use this domain for a new behavioural definition of Berry’s causality analysis for Esterel in terms of approximation intervals. This gives a compact and more uniform understanding of causality and generalises to other data-types. We also prove that Esterel’s ternary domain and its semantics is conservatively extended by the recently proposed sequentially constructive (SC) model of computation. This opens the door to a direct mapping of Esterel’s signal mechanism into boolean variables that can be set and reset arbitrarily within a tick. We illustrate the practical usefulness of this mapping by discussing how signal reincarnation is handled efficiently by this transformation, which is of complexity that is linear in program size, in contrast to earlier techniques that had, at best, potentially quadratic overhead.


[RePP’14-1] Towards Interactive Timing Analysis for Designing Reactive Systems. (slides)


Summary: Reactive systems are increasingly developed using high-level modeling tools. Such modeling tools may facilitate formal reasoning about concurrent programs, but provide little help when timing-related problems arise and deadlines are missed when running a real system. In these cases, the modeler has typically no information about timing properties and costly parts of the model; there is little or no guidance on how to improve the timing characteristics of the model. Here, we propose a design methodology where interactive timing analysis is an integral part of the modeling process. This methodology concerns how to aggregate timing values in a user-friendly manner and how to define timing analysis requests. We also introduce and formalize a new timing analysis interface that is designed for communicating timing information between a high-level modeling tool and a lower-level timing analysis tool.


[RePP’14-2] Worst Case Reaction Time analysis of Synchronous Programs: Studying the Tick Alignment Problem. (slides)


Summary: Synchronous programs are ideally suited for the design of safety critical systems as they provide guarantees on determinism and deadlock freedom. In addition to such functional guarantees, guarantees on timing are also necessary. In this talk, we study the problem of static worst case reaction (WCRT) time analysis of synchronous programs. While, there have been many recent attempts at addressing this problem from the point of view of scalability and precision, one crucial aspect is yet to be examined from a fundamental viewpoint. Concurrent threads in a synchronous program must align during every reaction, a problem that has been termed as the tick alignment problem (TAP), i.e., infeasible ticks that never align in practice must be ruled out for precision. We, for the first time, study TAP in the guise of a number theoretic formulation in order to not only explore its lower bound complexity, but also to develop heuristics that work well in practice.



Technical Reports:

[TR1308] Sequentially Constructive Concurrency. A Conservative Extension of the Synchronous Model of Computation. (pdf)


Technical Report No. UCB/EECS-2014-26, University of California, Berkeley, EECS Department, April 2014.


 [TR94] Grounding Synchronous Deterministic Concurrency in Sequential Programming. (pdf)


[TR95] WCRT analysis of Synchronous Programs: Studying the Tick Alignment Problem (pdf)

M. Mendler, B. Bodin, P. S. Roop, J.-J. Wang.