Prof. Maryline Chetto, Nantes Université, France.

(Title: Real-time scheduling issues in sensors with energy neutral constraints)

Abstract

A growing number of IoT applications involve wireless sensor nodes that may be deployed in wide areas and possibly unattainable places. These devices have to function perpetually without any human intervention because either costly or impractical. Thus, Energy Harvesting (EH) has arisen as a suitable means to satisfy design objectives. Nevertheless, the environmental energy is uncontrollable, not necessarily predictable and fluctuent along time.  The sensor node should be equipped with an intelligent power management strategy that guarantees energy neutral operation (i.e. that the system never consumes more energy than harvested). In addition to energy limitations and variability, a common characteristic of the IoT devices is their cyclic data computations within specified and bounded time intervals. A lot of research work has been done to analyze and predict the schedulability of real-time systems under different scheduling policies and several task models.  However, few analyses were performed under both energy neutrality and real-time requirements.

This talk will provide state of the art as well as our findings regarding the power management and real-time scheduling techniques that permit to sparingly use the harvested energy for the execution of deadline constrained tasks.  Special emphasis will be placed on dynamic priority scheduling since the classical real-time scheduler Earliest Deadline First cannot ensure energy aware scheduling and behaves poorly under EH settings.

Biography

Maryline Chetto is currently a full professor in computer engineering with Nantes Université, France. She received the degree of Docteur de 3^ème cycle in control engineering and the degree of Habilitée à Diriger des Recherches in Computer Science from the University of Nantes, France, in 1984 and 1993, respectively.  From 1984 to 1985, she held the position of Assistant professor of Computer Science at the University of Rennes, while her research was with the Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Rennes. In 1986, she returned to Nantes and has been from 2002 a full professor with the University of Nantes. She is conducting her research at Laboratoire des Sciences du Numérique de Nantes (LS2N, UMR CNRS n° 6004) in the Real Time System group.

Her research has been focused on development and formal validation of solutions regarding Scheduling, Fault-tolerance and Dynamic Power Management in real time embedded applications. Her current research is specifically targeting real-time scheduling issues in energy neutral devices. She has more than 150 papers published in international journals and conferences. She was the editor of the books Real-time Systems Scheduling (Elsevier, 2014) with volume 1 Fundamentals and Volume 2 Focusses. She was the co-author of the book Energy Autonomy of real-time systems (Elsevier, 2016). She was general chair of the 2020 IEEE International Conference on Green Computing and Communications (GreenCom-2020). Since 2011, she was elected member of the French National Council for Universities.

*********

Prof. Mohammad Reza Mousavi, King’s College London, England.

(Title: Formal Analysis of Dynamic Updates in Software Defined Networks)

Abstract

We introduce a language for specifying dynamic updates for Software-Defined Networks. Our language captures the interaction between the control- and data-plane in dynamic updates. We provide an efficient reasoning method about safety properties for dynamic networks. We implement our reasoning method in a tool prototype and apply it to a case study. We show that we can analyze the case study for networks with hundreds of switches using our tool prototype.

Biography

Mohammad Reza Mousavi is a professor of Software Engineering at King’s College London. Prior to that, he held the chair in Data-Oriented Software Engineering at the University of Leicester, UK. Before moving to the UK, he held positions in Sweden (Halmstad and Chalmers), The Netherlands (TU Eindhoven and TU Delft) and Iceland (Reykjavik). Mohammad obtained his Ph.D. in Computer Science from Eindhoven University of Technology, The Netherlands in 2005. He got his bachelors and master’s degrees, respectively, in 1999 and 2001, from Sharif University of Technology, Iran. He has led various research grants from the British, Swedish, and Icelandic funding agencies on formal semantics, verification, and software and systems testing at the foundational and applied level, involving industrial sectors such as transport and healthcare. Currently, he is the principal investigator of the UKRI Trustworthy Autonomous Systems Node on Verifiability. His main research interest is in testing, particularly of variability-intensive and cyber-physical systems

*********

Prof. Marjan Sirjani, Mälardalen University, Sweden

(Title: Analysis of Timing Properties in Networked Systems)

Abstract

Our world has become a network of connected software systems, communicating with each other, and controlling physical systems. Soon we will see autonomous cars whooshing around, interoperable medical devices monitoring and controlling the health of patients, and collaborating robots interacting with humans without separating fences. These systems are generally concurrent, distributed, and dynamic, with critical timing properties. In this talk, I will present our approach for analysis of timing properties of interoperable systems, using actor models and formal verification. Rebeca was designed more than 20 years ago as an imperative actor-based language with the goal of providing an easy-to-use language for modelling concurrent and distributed systems, with formal verification support. It was extended a few years later to support modelling real-time network and computational delays, periodic events, and required deadlines. I will reflect on how we used this language and its toolset for timing analysis and safety assurance of different systems, such as Network on Chip architectures, sensor network applications, network protocols, and medical interoperable systems.

Biography

Marjan Sirjani is a Professor at Mälardalen University, and the leader of Cyber-Physical Systems Analysis research group. Her main research interest is applying formal methods in Software Engineering. She works on modeling and verification of concurrent, distributed, timed, and self-adaptive systems. Marjan and her research group are pioneers in building model checking tools, compositional verification theories, and state-space reduction techniques for actor-based models. She has been working on analyzing actors since 2001 using the modeling language Rebeca (http://www.rebeca-lang.org). Her research is now focused on safety and security assurance and performance evaluation of cyber-physical and autonomous systems. Marjan has been the PC member and PC chair of several international conferences including SEFM, iFM, Coordination, FM, FMICS, SAC, FSEN, and DATE. She is an editor of the journal of Science of Computer Programming.