|
|
RISE
|
Home PageNewsProject Description
Publications
DemonstratorFinal Report |
Publications
Paul
Caspi and Albert Beveniste. Toward an Approximation Theory for
Computerised Control. EMSOFT'02, Volume 2491, Issue, pp
294-304, Lecture Notes in Computer Science Abstract. This
paper addresses the question of extending the usual approximation and
sampling theory of continuous signals and systems to those encompassing
discontinuities, such as found in modern complex control systems (mode
switches for instance). We provide some evidence that the Skorokhod topology is
a good candidate for dealing with those cases in a uniform manner by showing that, in the boolean case,
Skorokhod uniformly continuous signals are exactly the signals with uniform
bounded variability. Albert
Benveniste, Fellow, IEEE, Paul Caspi, Stephen A. Edwards, Member,
IEEE, Nicolas Halbwachs, Paul Le Guernic, and Robert de Simone. The Synchronous Languages
Twelve Years Later. Proceedings of the IEEE , Volume: 91 Issue: 1 ,
Jan 2003 Abstract.
Twelve years ago, Proceedings of the IEEE devoted a special section to the
synchronous languages. This article discusses the improvements, difficulties,
and successes that have occured with the synchronous languages since then.
Today, synchronous languages have been established as a technology of choice
for modeling, specifying, validating, and implementating real-time embedded
applications. The paradigm of synchrony has emerged as an engineer-friendly
design method based on mathematically-sound tools. Florence
Maraninchi and Yann Remond. Mode-Automata: a
new domain-specific construct for the development of safe critical systems Abstract. Over
the past ten years, the family of synchronous languages (Special Section of
the Proc. IEEE 79 (9) (1991)) has been very successful in offering
domain-specific, formally defined languages and programming environments for
safety-critical Systems. Among them, Lustre is well-suited for the
development of regulation systems, which are first designed by control
engineers, and can then be programmed as block-diagrams. Automatic generation
of C code provides the embedded software. The success of Lustre showed
that it is a good idea to offer domain-specific languages and constructs to
reduce the gap between the first design of a system (for instance a control
law) and the program written for it. When the structure of the first design
has to be encoded into the available constructs of a general-purpose
programming language, the interesting information is likely to be lost
somewhere on the way from the original design to the actual implementation.
This may have consequences on the efficiency of the code produced, or even on
the correctness of the design. Working with the systems
Lustre is well-suited for, we observed that they are often specified
informally using the notion of running modes. However, there seemed to exist
no language in which the mode-structure of a complex system could be
expressed directly. Following the approach of domain-specific languages, we
proposed to extend Lustre with a new construct, called mode-automaton,
devoted to the description of these running modes of regulation systems. In this paper, we define the
language of mode-automata and its semantics, give some ideas on the
compilation process, illustrate the approach with the example of the
production cell, and comment on the benefits of the approach, in general.
design method based on mathematically-sound tools. Bernard Dion, Thierry Le Sergent, Bruno Martin, Herbert Griebel. Model-based development for
time-triggered architectures Abstract. Time-Triggered
Architectures (TTA) and SCADE are both well-established technologies and
tools for building safety-critical embedded software. Both are based on the
same time-triggered approach; TTA for the communication infrastructure and
SCADE for the application components. This paper presents the
integration of these two technologies and tools for the design of distributed
systems. When completed, the breakthrough of this solution will be that it
provides a single framework to: ·
Specify behavior, timing constraints, and mapping
of tasks onto hardware. ·
Generate all the code needed to build
communicating executables. ·
Simulate and perform formal verification of
properties both for each individual task and also for the global model. Specification is accomplished
with a graphical view that allows the definition of hardware nodes and
mapping of any set of subsystems (a subsystem consists of several
communicating tasks, all located on the same node) on these nodes.
Replication is authorized and handled by the Fault Tolerant Communication
(FT-COM) layer. Code generation is supported
by add-ons to the two toolsets: the complete architecture and timing
information is generated from SCADE and passed to the TTPPlan and TTPBuild
functions that compute respectively the communication scheduling and the task
scheduling for each node. The SCADE Code Generator generates certifiable C
code for each task. TTPBuild generates the code for the scheduling of the
tasks on each node. A simple wrapper code is generated to handle data
transfer between the FT-COM layer and task interfaces. Simulation and formal
verification is possible thanks to the same underlying paradigm for both
technologies: as both the application tasks and the communication infrastructure
are time-triggered, with complete determinism, a global system model can be
represented and formally verified. A. Köhler; D. Kant. Use of formal verification
for the software development in the automotive area Abstract. The
method of Formal Verification is getting more and more important for the
software development in the automotive industry because of completeness and
the support of Frontloading. This has been investigated for real applications
in the context of established tools in the area. Integrating this method in
to the software development process requires further improvements on the
performance, interfaces and supported language of the tools. But in the
context of deterministic time triggered architectures there are additional possibilities
to support Frontloading in the development process for software. These
interesting topics are represented in this paper. >> more
publications by Verimag |
|
|
|
