List of talks with Abstracts

1. Gerard Berry (Esterel Technologies): Synchronous design and verification of critical embedded systems using SCADE and Esterel

abstract:
SCADE (Safety Critical Application Design Environment) is a design environment dedicated to safety-critical embedded software applications. It is widely used for avionics, railways, heavy industry, and automotive applications. For instance, most critical systems of the Airbus A380 have been developed with SCADE. The core element is the Scade synchronous formalism, which can be viewed as a graphical version of Lustre coupled with synchronous hierarchical state machines. The Scade to C compiler is certifiable at level A of DO-178B avionics norm, which removes the need for unit-testing the embedded C code and brings big savings in the certification process. The SCADE tools encompasses a simulator, a model coverage analyzer, a formal verifier, a display generator, and gateways to numerous other prototyping or software engineering tools. Esterel Studio is a similar hardware modeling, design, and verification environment based on the Esterel v7 formal synchronous language. Esterel Studio is used by major semiconductor companies to specify, verify, and synthesize complex hardware designs.
It can generate both an optimized circuit and a behaviorally equivalent software model from a single formal specification. It also supports simulation and formal verification, which is widely used in production applications. We discuss the advantages and limitations of the underlying synchronous concurrency model. We explain why the same core science and technology can be applied to such different domains, however with quite different integration in global system-level design flows according used in the different industries.

2. Tom Henzinger (EPFL Lausanne): The Embedded Systems Design Challenge (based on a joint position paper with Joseph Sifakis)

abstract: We summarize some current trends in embedded systems design and point out some of their characteristics, such as the chasm between analytical and computational models, and the gap between safety-critical and best-effort engineering practices. We call for a coherent scientific foundation for embedded systems design, and we discuss a few key demands on such a foundation: the need for encompassing several manifestations of heterogeneity, and the need for constructivity in design. We believe that the development of a satisfactory Embedded Systems Design Science provides a timely challenge and opportunity for reinvigorating computer science.

3. Sabine Glesner (TU Berlin): Verification of Optimizing Compilers

abstract:
Compiler correctness is a necessary prerequisite to ensure software correctness and reliability as most modern software is written in higher programming languages and needs to be translated into native machine code. In this talk, I report on results as well as on ongoing research concerning verification of optimizing compilers.

Starting from intermediate representations in static single assignment form, we consider optimizing program transformations and machine code generation. I demonstrate how such transformation algorithms can be formally verified. In particular, I address the issue of formalizing these proofs within the Isabelle/HOL theorem prover. Furthermore, I discuss the use of program checking to ensure the correctness of the corresponding compiler implementations. Concludingly, I also report on our research concerning compiler optimizations and provide an overview about our further research topics, especially about the deployment of the presented methods and techniques in embedded systems.

4. Arne Hamann, R. Ernst (TU Braunschweig): SymTA/S - Modeling system timing using abstract event streams

abstract:
Based on abstract event stream models and algebraic scheduling analysis, a fix point problem is formulated and solved using an iterative approach. This very fast but still accurate approach enables system sensitivity analysis and advanced system optimization. The presentation gives a coarse outline and some examples from realistic industrial designs.

5. Torsten Kempf, Rainer Leupers (RWTH Aachen): MPSoC modeling and simulation techniques

abstract: To cope with the increasing demands in embedded applications has prompted system architects to opt for Multi-Processor System-on-Chips (MPSoCs). The programmable cores within these MPSoCs provide high flexibility and can be optimized to the requirements of the application to deliver high performance as well (Application Specific Instruction set Processors). The inherent incorporation of parallelism by employing multiple cores increases the provided performance significantly, but poses many new challenges for system architects as well as for software and hardware designers. To cope with these challenges Electronic System-Level-Design (ESL design) seems to be the upcoming standard for simulation, development and verification of such systems.

The focus of this presentation will be placed on Electronic System-Level-Design, which is widely accepted in industry and academia to be the key enabling technique for future platform development. Different HW/SW cosimulation environments will be compared and it will be highlighted how hardware designers and system architects can utilize those for system development. Additionally it will be shown how software developers can program these MPSoC platforms and exploit the provided capabilities efficiently

6. Marc Pantel (IRIT, Toulouse): Model Driven Engineering: Bringing formal validation into the industrial process

abstract: MDE is a promising approach for integrating formal validation technologies into the current industrial practises, where an increasing number of Domain Specific Languages (DSL) are used for the expression of the user problems in a user friendly manner.

On the other hand, several formal verification tools may be required for achieving a satisfactory validation of the system under development. Formal validation tools represent a non negligable development effort and each method depends more on the kind of requirements to be verified rather than the DSL used.

Therefore, the development of efficient, flexible, yet reliable model transformation technologies is an important issue in the domain of embedded systems. A particular problem is the interpretation of the validation results by the user.

In this talk, we will show on an interesting Case study the complete Development Process, starting from a user defined DSL model to a PetriNet model and its validation; in particular, we will show how we can ensure the correctness of the transformations so as to guarantee the soundness of the approach.

7. Huascar Espinoza, Francois Terrier (CEA-List, France): Model Driven Engineering and Real-Time Analysis of Embedded Systems: The UML MARTE Standard and its Challenges

abstract: Recently, the Object Management Group (OMG) has performed important efforts to standardize a UML profile for Modeling and Analysis of Real-Time Embedded systems (MARTE), which provides language means to enable the verification of temporal properties based on the Model-Driven Engineering (MDE) paradigm. Applying MDE to the real-time analysis of embedded systems attempts to narrow down the complexity in the application of the underlying formal techniques, while focusing on the quantitative information (e.g., time measurements and constraints) and their effects w.r.t. different implementation decisions. In spite of the potential benefits of MARTE as a domain language, its widespread use entails further research to define specific development and analysis methodologies easing its usability in complex and heterogeneous systems, where generally, single methods can not support the analysis of entire systems. Current trends in MDE focus more on how to represent systems for particular analysis methods, than how to build these representations in a global design flow involving multiple analysis techniques and tools. There is indeed a need to have an analysis perspective sufficiently powerful to combine heterogeneous analysis information at different refinement levels, in a consistent, reusable and traceable form. In this talk, we describe some MDE challenges to represent complex analysis scenarios and, particularly, model preparation for sensitivity analysis.

8. Susanne Graf (Verimag, Grenoble): Contract-based modelling with BIP

abstract: BIP is a framework for component-based modelling of heterogeneous systems where componets and subsystems are described in a layered fashion, strictly separating behaviour, interaction and priority. We have shown how this structure can enable efficient verification of structural properties, such as absence of deadlock.
In the SPEEDS IP project, a notion of rich component has been defined, where interfaces are enriched with functional and non functional contracts, for enabling a more efficient system develeopment process. In this talk, we show how we use BIP for enabling contract-based validation in this context.

9. Kim Larsen (CISS Aalborg, DK), Michael R. Hansen, Jan Madsen (DTU, DK)

 Kim Larsen: Validation and Performance Analysis of Real-Time Systems in UPPAAL
abstract: UPPAAL is an integrated tool environment for modelling, validation and verification of real-time systems modelled as networks timed automata, extended with data types and user-defined functions. The tool is developed in collaboration between the Department of Information Technology at Uppsala University, Sweden and the Department of Computer Science at Aalborg University in Denmark. Applications include validation and performance analysis of real-time controllers and real-time communication protocols as well as synthesis of optimal (e.g. wrt. energy or memory) scheduling strategies for given applications

 Michael R. Hansen: Formalising the ARTS MPSOC Model in UPPAAL
abstract: ARTS is a MultiProcessor System-on-Chip modelling environment, developed at DTU. The ARTS model has been formalised in the UPPAAL which allows for formally reasoning about real-time issues of multiprocessor systems consisting of application software running under different RTOS on processors interconnected through an on-chip network (NoC). Industrial relevance will be shown, including links to a case study planned.

 Industrial presentation: Optimising a Memory Interface
abstract: TERMA is a Danish company producing radar sensors mainly used for traffic control in ports and airports and for coastal surveillance. The real-time processing of radar signals includes integration of several received signals, requiring the signals to be stored temporarily in memory. The interface between the signal processing hardware and the memory consists of an arbiter and a collection of 9 FIFO buffers. Within the European project AMETIST UPPAAL has been applied in verifying that the behaviour the scheduling algorithm used by the arbiter is correct in the sense that none of the buffers ever under- or overflows. Also, alternative, correct scheduling strategies has been automatically derived being optimalwrt the required size of buffers

• 

   

  PDF - 1.6 Mb
  

Réalisation Axome - Création de sites Internet