Joseph Sifakis (CNRS / Verimag, France)
“System Design in the Era of IoT — Trends and Challenges”
Abstract: The ICT revolution is dominated by the IoT vision which promises increasingly interconnected smart objects providing autonomous services for the optimal management of resources and enhanced quality of life. These include smart grids, smart transport systems, smart health care services, automated banking services, smart factories, etc. Their coordination will be achieved using a unified network infrastructure, in particular to collect data and send them to the cloud which in return will provide using data analytics, intelligent services to ensure global trustworthiness and performance.
This vision raises a lot of expectations and in my opinion some over-optimism about its short-term impact.
The purpose of this talk is to discuss to what extent the IoT vision is reachable under the current state of the art, identify technical obstacles and point out work directions for overcoming them.
It is well-understood that the current network infrastructure is neither safe nor secure enough. Furthermore, it is hard to guarantee time predictability for critical events. All these make problematic the development and coordination of critical autonomous systems and services. Additional problems come from the need to integrate critical and best-effort systems and deal with heterogeneous technical requirements.
For decades critical systems engineering has relied on two pillars: the first pillar is Verification and Validation (V&V) seeking systematic and accountable exploration of models of the designed system and/or its development process; the second is the V-model of the systems engineering process demonstrating the relationships between each phase of the development life cycle and its associated phase of V&V.
These engineering principles are not any more affordable. They both need rigorous formulation of requirements as well as faithful models of the developed system and process. Writing rigorous requirements for open autonomous systems, e.g. self-driving cars, turns to be an insurmountable problem. It is very hard to understand and logically analyze rules involving not only technical but also ethical, legal and societal issues. Additionally, machine learning techniques — viewed as the key to building autonomous systems — are not developed based on requirements e.g. that specify how a dog looks different from a cat.
Consequently in absence of rigorous requirements, the application of existing V&V techniques becomes also problematic.
The application of rigorous system design techniques is currently challenged by three factors: the extended use of cyber physical components, the deployment of dynamic and reconfigurable systems that exhibit adaptive behavior, and the increasing and unmanageable uncertainty of execution and external environments.
Existing design flows for critical systems are not any more affordable in the IoT context for both technical and economic reasons. Guaranteeing statically at design time correctness of critical autonomous systems becomes impossible. We need effective design flows seeking an appropriate balance between properties guaranteed at design time and properties enforced at run time. This implies in particular that we break with the deterministic concept of correctness adopted by current critical application standards.
We advocate the design of adaptive systems that can change dynamically their behavior to cope timely and effectively with mishaps of any kind caused by design errors, failures or malevolent action. Adaptation is the capability to change system behavior in particular by reconfiguring its services and resources guided by knowledge acquired both at design time and at run time. We identify technical challenges for adaptive control achieved by combining three main functions: objective management, planning and learning.
Bio: Dr Joseph Sifakis is Emeritus Senior CNRS Researcher at Verimag. His current research interests cover fundamental and applied aspects of embedded systems design. The main focus of his work is on the formalization of system design as a process leading from given requirements to trustworthy, optimized and correct-by-construction implementations.
Joseph Sifakis has been a full professor at Ecole Polytechnique Fédérale de Lausanne (EPFL) for the period 2011–2016. He is the founder of the Verimag laboratory in Grenoble, which he directed for 13 years. Verimag is a leading research laboratory in the area of embedded systems, internationally known for the development of the Lustre synchronous language used by the SCADE tool for the design of safety-critical avionics and space applications.
In 2007, Joseph Sifakis has received the Turing Award for his contribution to the theory and application of model checking, the most widely used system verification technique today.
Joseph Sifakis has had numerous administrative and managerial responsibilities both at French and European level. He has actively worked to reinvigorate European research in embedded systems as the scientific coordinator of the « ARTIST » European Networks of Excellence, for ten years. He has participated in many major industrial projects led by companies such as Airbus, EADS, France Telecom, Astrium, and STMicroelectronics.
Joseph Sifakis is a member of the French Academy of Sciences, a member of the French National Academy of Engineering and a member of Academia Europea and a member of the American Academy of Arts and Sciences, and a member of the National Academy of Engineering. He is a Grand Officer of the French National Order of Merit, a Commander of the French Legion of Honor. He has received the Leonardo da Vinci Medal in 2012.
Joseph Sifakis has received in 2009 the Award of the Hellenic Parliament Foundation for Parliamentarism and Democracy. He is a commander of the Greek Order of the Phoenix.
He has been the President of the Greek Council for Research and Technology for the period February 2014 – April 2016.
Thanassis Tsiodras (European Space Agency, The Netherlands)
“TASTE — an ESA-led toolchain that uses model-driven code generation to create correct-by-construction SW for safety-critical targets”
Abstract: Back in 2004, while working as the Senior Software Engineer and Technical Lead of Semantix — a company I co-founded — I found myself facing a significant technical challenge: I had to figure out a way to effectively handle 7 different versions of evolving telecom protocols, while implementing more than three thousand validation rules for each one of them. Through shear luck — reading the right paper at the right time — I realized that instead of writing the code myself, I could instead create a small language to describe the logic of the validations, mergings, etc. — and then create a parser and code generator that would write the code for me.
Six months later, my code generators had created 700’000 lines of C++ code addressing all the needs for all possible versions. We released the resulting product line to the world, and it quickly became world leading — with the rather distinctive characteristic of zero bug reports; with companies all over the world using the tools constantly, processing millions of call records every day.
ESA became aware of this work through a presentation we later did on these code generators. The Agency had always been — and still is — on the lookout for ways to shield mission codebases from errors — since any one of them may lead to mission loss. The right people from ESA saw in that presentation what Semantix did, and involved my company — and me personally — in a series of projects, where TASTE was born and rapidly evolved into an ever-expanding set of closely knit model-to-model and model-to-code transformation engines.
In this talk, I will try to share with the workshop attendees what TASTE is; how it started, how it evolved into what it is today, and what it provides in terms of real-world semantics-preserving model transformations; with specific emphasis on targeting the safety-critical domains.
Bio: Dr Thanassis Tsiodras received his MSc in Computer and Software Engineering from the National Technical University of Athens in 1995, and his PhD in Telecom and Software Engineering from the same institute in 1999. In 2001, he became one of the founders of Semantix Information Technologies, where he spent more than a decade as the company’s Senior Software Engineer and Technical Lead. During that time, he employed model-driven code generation in his company’s product lines, creating world-leading tools in the process. He is currently working for the European Space Agency, as a member of the TEC/SWE engineering team in ESTEC.