ANSYS® SCADE Suite® is a development environment for safety critical embedded software used for more than twenty years in various application domains like avionics, nuclear plants, transportation, automotive. Its code generator is qualified for several industrial standards (DO-178C, IEC 61508, EN 50128, IEC 60880 and ISO 26262) to be used in the development of the most safety critical systems.
Scade is historically based on the synchronous language Lustre designed in Grenoble in the VERIMAG laboratory by its two mains authors Paul Caspi and Nicolas Halbwachs. In its early days, it was mainly seen as a graphical notation for this academic language.
In 2008, a major new version was released, based on the language Scade 6 that extended the dataflow point of view offered by Lustre to integrate new constructs inspired by Esterel and SyncCharts in order to allow more control oriented design style. This language is formally specified following the work of Marc Pouzet on the design of Lucid Synchrone, in particular on the static correction of programs. The formalized aspects cover mainly the static semantics i.e. the type systems that define what a correct program is; this correction is based on four type systems: Types (in the most classical sense), Clocks, Initialization analysis and Causality analyses.
As a formal language, Scade is also well suited to apply formal verification on the applications developed with it. Programs are guaranteed to run in finite memory which allows to use state of the art model checking techniques.
The talk will go through this history, giving some insights on the new Scade 6 constructs, its differences with Lustre and on the development of its qualified code generator.
The formal verification of Scade 6 programs will also be illustrated.
One rarely encounters programming languages and frameworks that provide general-purpose and type-safe hot code swap. It is demonstrated here that this is entirely possible in Haskell, by faithfully following the motto of live coding: "Change the program, keep the state."
With generic programming, one easily arrives at an automatic state migration function. The approach can be generalised to an arrowized Functional Reactive Programming framework that is parametrized by its side effects. It allows for building up complete live programs from reusable, modular components, and to separate data flow cleanly from control flow. Useful utilities for debugging and quickchecking are presented.
Many industrial IoT applications process sensor data over distributed networks to monitor devices in real-time. Since the sensor telemetries are transmitted over networks as events, imperative and event-driven programs are often used to handle IoT data. However, the inverted control flow and shared global states of these imperative programs make them difficult to interface with synchronized computation on IoT data. This problem is further complicated for high-frequency data such as electric signals, which may require dynamic adjustment to data sampling rate to operate under the constraints of network and system.
In this paper, we propose a push-pull reactive programming model for IoT application to address this challenge. This model uses push-streams for asynchronous computation such as data capturing and user controls and uses pull streams for synchronized computation such as data analysis. This model is simpler than push-based models by avoiding the complexity of glitch prevention through re-sampling in pull-streams. It is also more flexible than pull-based models by allowing dynamic adjustment of the sampling rate to maintain real-time speed of the IoT computation. The push-stream has a monadic interface, which converts to a pull stream through buffering. A pull stream converts to a push-stream when driven by a clock. The dynamic switching of our streams is based on a monadic abstraction called AsyncM that uses continuation passing style and a form of cancellation token for asynchronous control. Our model is simple and can use threads or event callbacks for concurrency.
Sorting is a central problem in computer science and one of the key components of many applications. To the best of our knowledge, no reactive programming implementation of sorting algorithms has ever been presented.
In this paper we present reactive implementations of so-called sorting networks. Sorting networks are networks of comparators that are wired up in a particular order. Data enters a sorting network along various input wires and leaves the sorting network on the same number of output wires that carry the data in sorted order.
This paper shows how sorting networks can be expressed elegantly in a reactive programming language by aligning the visual representation of a sorting network with the canonical DAG representation of reactive programs. We use our own experimental language called Haai to do so. With a limited number of built-in higher-order reactive programs, we are able to express sorting networks for bubble sort, insertion sort, bitonic sort, pairwise sort and odd-even merge sort.