Keynotes Speakers

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

 

- Michel Raynal (Biography, Abstract, Home page)
                 Communication and Agreement Abstractions for
              Fault-tolerant Distributed Systems

 

- 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. 

 

Communication   and   agreement   abstractions for   fault-tolerant distributed systems

Michel Raynal

Professor of Computer Science

 

IRISA, Campus de Beaulieu
Université de Rennes1

France

 

 

 

Michel Raynal is a professor of computer science at the University of Rennes, France.  His main research interests are the basic principles of distributed computing systems. Michel Raynal is the author of numerous papers on distributed algorithms and a world leading researcher in the domain of distributed computing. He has chaired the program committee of the major conferences on the topic, such as the IEEE Int'l Conference on Distributed Computing Systems (ICDCS), the Symposium on Distributed Computing (DISC), the Int’l Colloquium on Structural Information and Communication Complexity (SIROCCO), and   the Int’l Conference on Principles of Distributed   Systems (OPODIS). He has  also  served  on  the  program  committees  of  many international   conferences,  and is    the  recipient  of  several  "Best Paper''   awards.  Michel Raynal has been invited by many universities all over the world to give lectures on distributed computing.

 

Abstract

Understanding distributed computing is not an easy task. This is due to the many facets of uncertainty one has to cope with and master in order to produce correct distributed software. Considering the uncertainty created by asynchrony and process crash failures in the context of message-passing systems, the talk will focus on the main abstractions that one has to understand and master in order to be able to produce software   with guaranteed properties. These fundamental abstractions are communication abstractions that allow the processes to communicate consistently (namely the register abstraction and the reliable broadcast abstraction), and the consensus agreement abstractions that allows them to cooperate despite failures.  As they give a precise meaning to the words "communicate" and "agree" despite asynchrony and failures, these abstractions allow distributed programs to be designed with properties that can be stated and proved.

Impossibility results are associated with these abstractions. Hence, in order to circumvent these impossibilities, the talk relies on the failure detector approach.

 

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.