Conférenciers invités

• - Sandeep K. Shukla (Biography, Abstract, Home page)
                Model Driven Embedded Software Generation:
                A Generative Approach to Safety

 

- Michel Raynal (Biography, Abstract, Home page)
                 Abstractions pour la communication et l'accord dans

              les systèmes répartis sujets à défaillances

 

- Nicolas Guelfi (Biography, Abstract, Home page)           

                 Dependability and Resilience from a Software

              Engineering Perspective

 

 

Model Driven Embedded Software Generation: A Generative Approach to Safety

 

Sandeep K. Shukla

Associate Professor of Computer Engineering

 

Deputy Director of Center for Embedded Systems for Critical Applications

Director of FERMAT Lab

Virginia Polytechnic and State University, USA

 

 

Sandeep K. Shukla is an associate professor of computer engineering at Virginia Tech. He is also a founder and deputy director of the center for embedded systems for critical applications (CESCA), and director of his research lab FERMAT. Sandeep was awarded the Presidential Early Career Award for Science at Engineering (PECASE) award for his research in design automation for embedded systems design, which in particular focuses on system level design languages, formal methods, formal specification languages, probabilistic modeling and model checking, dynamic power management, application of stochastic models and model analysis tools for defect-tolerant system design, and reliability measurement of defect-tolerant systems. Sandeep has published more than 125 articles in journals, books and conference proceedings. Sandeep  co-authored  three research monographs, and four edited volumes.  Sandeep has been elected as a College of Engineering Faculty Fellow at Virginia Tech. In 2008 Sandeep was  awarded the Alexander Humboldt Foundation’s Bessel Award. Sandeep also chaired a number of international conferences and workshops, edited a number of special issues for various journals, and are on the editorial board of IEEE Design & Test, IEEE Transactions on Computer, and IEEE Embedded Systems Letters. Sandeep is a senior member of IEEE and ACM.

He is also an IEEE Computer Society Distinguished visitor, and an ACM distinguished speaker.

Abstract
Avionics, automotive, power plant control, and many other safety-critical embedded systems require safe, predictable, and statically analyzable software. Moreover, as the complexity of these applications mounts, performance and safety both become increasingly important. This increasing performance requirement drives the current market trend of multi-core processors (single chip multiprocessors) in the desktop market. However, recently embedded processors have started to surface with multiple homogeneous or heterogeneous cores. Multi-threaded or concurrent applications seem to be the best way to exploit these available parallel processing resources.

Those with any experience with multi-threaded programming would admit that design and implementation of multi-threaded programs is extremely difficult and prone to subtle concurrency and synchronization bugs, even without the use of advanced techniques such as speculative hreading, or wait-free synchronization etc are.  The inherent synchronization and dependency issues and the possible non-determinism are difficult to resolve without extremely skilled programmers, and possibly with the help of extensive static analysis. Static analysis and/or formal verification of large concurrent applications are again capacity limited by today’s state-of-the-art tools and techniques. Nevertheless, given the importance of safety in the target application domains, one has to produce absolutely correct code which is deterministic or predictable, and no non-deterministic execution behavior should lead to disastrous consequences. 

Correct-by-construction multi-threaded program generation is therefore our methodology of choice. For this, we need a formal specification language with well defined semantics and proper characterizations as to when it is safe to generate guaranteed deterministic code. We have chosen Polychronous or multi-rate specification language borrowing from the French synchronous programming languages. Synchronous languages have so far proven useful for generating sequential (single-threaded) code for safety-critical applications. A particular characterization of polychronous specifications called the ‘endochrony’ is a sufficient condition for correct sequential code generation.  Therefore, one could generate multiple sequential threads separately from ‘endochronous’ specification fragments, and compose them by generating the synchronization glue code. Unfortunately, ‘endochrony’ is not compositional, and therefore, the synchronization code generation becomes non-trivial. We show that a particular generalization of ‘endochrony’ called the ‘weak endochrony’ is sufficient for directly generating multi-threaded code from such specifications. Moreover, ‘weak endochrony’ is compositional and hence provides us with a modular code generation technique from polychronous specification.

In this talk, first, we elaborate on multi-rate specification formalism Polychrony. Then we explain the difficulties of deterministic and semantics preserving code generation from such specifications.  Then we discuss endochrony, inadequacy of which leads to the weak endochrony concept, and how this provides a sufficient condition for safe multi-threaded code generation. Finally, we discuss future directions in our work on deterministic multi-threaded code generation for safety-critical applications. 

 

Abstractions pour la communication et l'accord dans les systèmes répartis sujets à défaillances

 

Michel Raynal

Professor of Computer Science

 

IRISA, Campus de Beaulieu
Université de Rennes1

France

 

 

 

 

Michel  Raynal est professeur d'informatique à l'IRISA-IFSIC (Université de Rennes, France). Les principes fondamentaux du calcul réparti constituent ses  principaux centres  d'intérêt. Michel Raynal  est l'auteur d'un très grand nombres d'articles sur ses sujets.. et un des leaders mondiaux  du  calcul réparti. Plusieurs de ses articles ont été récompensés  par  un Best Paper  Award''. Il a été membre du comité de programme de plus de 100 conférences internationales  dans le domaine du calcul réparti et présidé le comité de programme des conférences majeures sur le sujet :  IEEE Int'l Conference on Distributed Computing Systems  (ICDCS), Symposium on Distributed Computing (DISC), Int'l Colloquium on Structural Information and Communication Complexity (SIROCCO), et Int'l  Conference on Principles of Distributed   Systems  (OPODIS). Michel Raynal a été invité par de nombreuses universités de par le monde pour donner des cours sur le calcul réparti. Il est également l'auteur de huit livres sur le sujet, dont le dernier a pour titre "Communication   and   agreement   abstractions for   fault-tolerant asynchronous distributed systems".

 

Abstract

L'incertitude  créée par les "adversaires" que sont l'asynchronisme et les défaillances  rend difficile la compréhension, la conception  et la maitrise du calcul réparti.  Considérant  de tels adversaires dans un contexte ou la  communication entre  entités se fait par passage de messages, l'exposé se concentrera sur les abstractions offertes aux applications, que son le registre partagé,  la diffusion fiable uniforme et l'accord réparti.  Ces abstractions fondamentales  permettent de donner un sens précis aux mots "communiquer", "coopérer" et "être d'accord" lorsqu'on s'intéresse à un ensemble de processus. Elles permettent de concevoir des programmes distribués  dont les propriétés peuvent être non seulement clairement énoncées mais aussi prouvées.  Des résultats d'impossibilité qui doivent être connus sont associés à ces abstractions. L'exposé considèrera en conséquence des systèmes répartis enrichis avec des détecteurs de fautes adéquats.

 

Dependability and Resilience from a Software Engineering Perspective

 

Nicolas Guelfi

Professor of Computer Science

 

Faculty of Sciences, Technology and Communication

Computer Science & Communications Research Unit

LASSY - Laboratory for Advanced Software Systems

University of Luxembourg

 

 

Nicolas Guelfi is professor at the Faculty of Sciences, Technologies and Communications of the University of Luxembourg since March 1999, where he teaches, directs PhD students and makes research in collaboration with national and international partners. Currently, he is the head of the Laboratory for Advanced Software Systems. His main research and development activities concern the engineering and the evolution of reliable and secure distributed and mobile systems based on semi-formal methods and transformations. He is the author of around 50 publications in books, journals, conferences and workshops. He has been for three years the Luxembourgian ERCIM representative at

the executive committee of the ERCIM consortium and he is co-chairman of the ERCIM working groups on Software EngineeRing for rEsilieNt systems (SERENE - http://serene.uni.lu). SERENE considers resilient systems as open and distributed systems that can dynamically adapt in a predictable way to unexpected events. The research group of Nicolas

Guelfi is made of PhD students, engineers and post-doctoral members that are running national or international research projects with important cooperation with universities or industries.

Abstract
The first part of this talk aims at presenting a rigorous conceptual framework for defining the concepts of dependability and resilience. The terms dependability resilience, since the seventies, has been used in nearly all the computer information systems and computer science fields. The introduction and use of these concepts in all these fields makes difficult to have a shared and precise definition of the concept of resilience. Having such definition is nevertheless mandatory for the software and systems engineering research community that create development processes, languages and tools to support the engineering of software and systems that would be required to be dependable or resilient. For this, we introduce an abstract and generic terminology to be used when speaking about resiliency. We also provide some abstract semantic descriptions to these terminological elements. This formal framework is defined from a software engineering perspective, which means that we define its components such that they are useful for the development or improvement of analysis, architectural design, detailed design, implementation, verification and maintenance phases. The second part of the talk aims at presenting an approach for modeling dependable collaborative time-constrained business processes.

The effectiveness of the information system a particular organisation uses for running its business depends largely of the success in modelling such business. This is due to the fact the business model defines the requirements of the information system that will support the running of the business. Nowadays, there exist many business process development methods that are supported by modelling notations and tools. Unfortunately these methods are not capable to model jointly complex collaborations, time constraints and to offer means to support resilient business process engineering. We will present shortly a business process language called DT4BP, which has been designed to drive the modeling of dependable, collaborative and time-constrained business processes. The presentation of DT4BP is made targeting end users, which are business processes modellers.