...
Workshops/Seminars:
[SYNCHRON’12] Sequentially Constructive Concurrency: A Conservative Extension of the Synchronous Model of Computation. (slides)
...
Summary: A presentation of the [DATE’13] publication.
[PDAY’13-1] Is timing analysis a refinement of causality analysis? (slides)
J. Aguado.
PRET Day (PDAY'13), INRIA 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.
[PDAY’13-2] Constructive Boolean Networks and the Exactness of Timed Ternary Simulation. (slides)
[D-CON'13] Constructive Boolean Netwroks Circuits and the Exactness of Timed Ternary Simulation. (slides)
M. Mendler.
PRET Day (PDAY'13), INRIA Grenoble France, March 2013.
...
Simulation.
[ECERS'13] Constructive Circuits and the Synchrony Hypothesis.
M. Mendler.
- PRET Day (PDAY'13), Inria Grenoble Rhône-Alpes France, March 2013.
- German Chapter Concur Meeting (D-CON'13), Institute for Software Engineering and Programming Languages, University of Lübeck, Germany, March 2013.
- Joint Electrical Engineering and Computer Science Departmental Seminar (ECERS'13), Auckland University, New Zealand, January 2014.
...
Summary: Presentations of materials included in the [FMSD’12] publication.
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.
[PTCONF’13] SCCharts: Sequentially Constructive Charts. (poster)
...
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.
...
Summary: This presents ...
[RePP’14-2] The WCRT analysis of synchronous programs: Studying the tick alignment problem. (slides)
...