CPS Master Track - List of Courses

 " Computational logic has been used in a wide range of application in computer science, ranging from the deductive approach to Artificial Intelligence advocated by AI's founder John McCarthy, to proving the absence of bugs in large industrial software such as the 14th metro line in Paris, or checking difficult theorems the as the one of Feit-Thompson in the classification of finite simple groups. The goal of this course is to explain how logic can be used in order for modeling problems of computational or mathematical nature, and how computers can be used to achieve this. In particular, we will present proof assistants, which allow to formalize human reasoning by interactively constructing proofs, and explain their use to certify the absence of bugs in programs. This is based on the so-called Curry-Howard correspondence: a program is the same as a proof (or, more precisely, a typed functional program corresponds to a derivation of its type). We will gradually introduce the required notions: - propositional logic and the constructive variants, - functional programming, formalized by lambda-calculus, - typing systems and the Curry-Howard correspondence. Then in order to reach realistic applications, we will present the proof assistant Agda and dependent logic which underlies it. Time permitting, we will also present various important related notions and techniques such as set theory and proof search. This course is also about logic in practice: all the TDs will be on computer, using OCaml and then Agda. Pre-requisites: some basic knowledge of logic, the course INF412 being of course perfect for this, otherwise reading some introductory book on logic over the summer is recommended (see the references on the website). The website for the course is http://inf551.mimram.fr/"

Syllabus from 2021-2022 We have entered the Artificial Intelligence Era. The explosion of available data in a wide range of application domains give rise to new challenges and opportunities in a plethora of disciplines – ranging from science and engineering to business and society in general. A major challenge is how to take advantage of the unprecedented scale of data, in order to acquire further insights and knowledge for improving the quality of the offered services, and this is where Machine and Deep Learning comes in capitalizing on techniques and methodologies from data exploration (statistical profiling, visualization) aiming at identifying patterns, correlations, groupings, modeling and doing predictions. In the last years Deep learning is becoming a very important element for solving large scale prediction problems. Course Logistics: 1. The course will take place on Monday afternoons beginning on 20/09/2021 and will be divided into nine 4-hour sessions as follows: (14:00 - 16:00) magistral teaching in: Amphi Gay-Lussac. (16:15 - 18:15) lab sessions in the small classes: Amphi Painlevé, Amphi Poisson, Amphi Sauvy. 2. Interaction/Q&As: We have set up a dedicated slack workspace for this course, which we will use to communicate with you. Please register to the following workspace with your full name and use it as much as possible. https://join.slack.com/t/inf554--202122/shared_invite/zt-v0v3gbl1-tsGESUgYbHgC7_Xcx3GsEg 3. The course will be assessed via: (20% of the course mark) an individual take-home assessment handed out on Monday 11th October with deadline on Monday 25th October 5pm. (80% of the course mark) a group data challenge handed out on Monday 8th November with a written report deadline on Friday 3rd December 5pm and oral assessments in the week of the 13th December. We will communicate further details about the formation of groups for the challenge at the start of November on the course slack channel. 4. You will have to complete the course work on your own laptops (preferably with a Unix environment like Linux or Mac OS X for compatibility reasons). As for software, we will be using Python among others (to be installed locally on the laptops). Students are invited to install the current Anaconda distribution BEFORE the 1st lab session (https://www.anaconda.com/products/individual). Please also make sure that you have installed the PyTorch, numpy and scikit-learn python packages. Detailed syllabus of the course: (minor changes may apply during course evolution.) General Introduction to Machine Learning - Machine Learning paradigms - The Machine Learning Pipeline Supervised Learning - Generative and non generative methods - Naive Bayes, KNN and regressions - Tree based methods Unsupervised Learning - Dimensionality reduction - Clustering Advanced Machine Learning Concepts - Regularization - Model selection - Feature selection - Ensemble Methods Kernels - Introduction to kernels - Support Vector Machines Neural Networks - Introduction to Neural Networks - Perceptrons and back-propagation Deep Learning I - Convolutional Neural Networks - Recurrent Neural Networks - Applications Deep Learning II - Modern Natural Language Processing - Unsupervised Deep Learning - Embeddings, Auto-Encoders, Generative Adversarial Networks Machine & Deep Learning for Graphs - Graph Similarity - Graph Kernels - Node Embeddings

 " The 21th century is, if anything, becoming a data-driven century. Interaction with everyday objects may yield a wealth of information, especially when correlated: if in an apartment the fridge door is being opened and closed regularly, then presumably apartment is inhabited ; if a drinking glass is subsequently emptied, presumably the inhabitant is alive and well, and, is staying both fresh and hydrated ; if the BBQ or the oven is used frequently, perhaps the inhabitant is either overeating (and so, a potential customer for diet plans) or is entertaining frequently (and so, a a potential customer for party supplies) — something which analysing the usage patterns of the door bell would reveal… A premise for being able to analyse usage patterns and interactions is, of course, that these physical actions are captured and transformed into data — and, that these data are communicated from everyday objects with and through the Internet, and to the cloud. And so, the 21th century is necessarily also the connected century: smartphones, watches, fridges, toothbrushes, drinking glasses, coffee machines, medical implants, BBQs, office plants, and forks are all becoming connected objects, generating data — and thus, becoming part of the Internet. Outside of the consumer market, knowing the state of a machine, of an airplane engine, or of a power substation, permits scheduling predictive maintenance and avoid accidents — embedded sensors able to capture, and communicate, this state is a necessary premise. As a matter of fact, a company launching a product today that doesn't ""run an app"" and ""connects to the Internet"" is a company, which just hasn't grasped the needs (or, at least, the desires) of its market - much as the guy installing the bike rack on the left, clearly misunderstood his ""target market"". In order to ensure that YOU do not end up being that gal/guy, building a product miserably missing the market, this course provides you with the core competencies, necessary for developing connected systems. This course: Offers a pragmatic and practical approach to communicating systems and to computer networking Studies, for each of the four major functional layers in a protocol stack (data-link, internetwork, transport, and application) the fundamental ideas, algorithms, and architectural principles, that apply “from the Internet, and to the IoT” Provides an in-depth tutorial in the principles behind TCP/IP Networking Introduces and decrypts modern Internet and IoT protocols: from IPv6 to 6LoWPAN, from ALOHA through Ethernet and WiFi to LoRa and Bluetooth — and from the WEB and REST to CORE And CoAP Provides practical experience in developing networked applications, and in developing and implementing protocols. In short, this course provides an in-depth understanding of “how the net works” (pun intended), and gives the necessary baggage for an engineer (regardless of area of exercise) to be able to design communicating systems. This course is self-contained: it assumes some programming skills, and a lot of curiosity — and will introduce the rest as it goes along. Each lesson will consist of a lecture, followed by 2h of lab (TD). This course is calibrated so that a student should expect to spend 1-2h/week outside of class, reviewing material and/or finishing exercises."

 " Cryptology is concerned with realising the impossible, namely securing information in open networks. This includes ensuring confidentiality of messages, integrity of messages, authenticity of principals. credit card The course gives an introduction to cryptology, its history and its use in modern computer systems. While the lectures are self-contained, some familiarity with basic algebra (Z/NZ, finite fields, cf. MAT552), networking (cf. INF557) is highly recommended. This course is part of the Cybersecurity track and a prerequisite for INF568. To each lecture corresponds a TD, in which you apply the learnt concepts by implementing them in C. The course is validated by a written examination. Moreover, many topics can be at the heart of a 3rd year project."

 " We will explain the enduring concepts underlying all computer systems, and show the concrete ways that these ideas affect the correctness, performance, and utility of any application program. This course serves as an introduction to the students who go on to implement systems hardware and software. But this course also pushes students towards becoming the rare programmers who know how things work and how to fix them when they break. It is not a course reserved to geeks, it is a course for all programmers! This course will cover most of the key interfaces between user programs and the bare hardware, including: - The representation and manipulation of information - Machine-level representation of programs - Processor architecture - The memory hierarchy - Exceptional Control Flow - Virtual memory The TDs are the heart of the course and will illustrate how to put the above at work in everyday programming practice. Among other things we will reverse-engineer a binary program, implement a buffer overflow attack, optimise a processor design, and implement our own memory allocator. We assume that the student has familiarity with programming. Experience with C or C++ languages is a plus, but If your only prior experience is with Java we will help. We do not assume any prior experience with hardware, machine language, or assembly-language programming."

  With the advent of multicore processors (and now many-core processors with several dozens of execution units), expressing parallelism is mandatory to enable high performance on different kinds of applications (scientific computing, big-data...). In this context, this course details multiple parallel programming paradigms to help exploiting such a large number of cores on different target architectures (regular CPUs and GPUs).It includes distributed-memory model (MPI), shared-memory model (OpenMP) and heterogeneous model (CUDA). All these approaches would allow leveraging the performance of differents computers (from small servers to large supercomputers listed in Top500).

Introduction to compilers. We describe tools and techniques used in the various phases of a compiler, up to optimizing assembly code production. An optimizing compiler for a fragment of the C language to x86-64 assembly is implemented during the labs.

 " The goal of this course is to provide an in-depth understanding of select advanced problems in wireless networking. Specifically, the course will study these topics: Overview of Wireless Networks Wireless Communications Random Access Deterministic Access Schemes Radio Link Control Cellular Access Constrained Networking Cellular Architecture and Protocols Cellular Mobility Transport and Wireless "

 This is a course on the design, implementation, and analysis of contemporary cryptographic algorithms. Among other things, we will give a detailed introduction to elliptic curve cryptography lattice-based cryptosystems real-world protocols public-key cryptography modern key exchange and signature schemes side-channel safety homomorphic encryption post-quantum cryptography modern symmetric cryptography We assume a familiarity with the basic cryptographic concepts and tools introduced in the course INF558a.

 " Distributed systems are composed of several computational units, classically called processes, that run concurrently and independently, without any central control. Additional difficulties are introduced by asynchrony (processes and channels operate at different speeds) and by limited local knowledge (each process has only a local view of the system and has a limited amount of information). Distributed algorithms are algorithms designed to run in this quite challenging setting. They arise in a wide range of applications, including telecommunications, internet, peer-to-peer computing, blockchain technology... This course aims at giving a comprehensive introduction to the field of distributed algorithms. A collection of significant algorithms will be presented for asynchronous networked systems, with a particular emphasis on their correctness proofs. Algorithms will be analyzed according to various measures of interest (eg., time and space complexities, communication costs). We will also present some ""negative"" results, i.e., impossibility theorems and lower bounds as they play a useful role for a system designer to determine what problems are solvable and at what cost. Content: Modelling of distributed networked systems Wave and traversal algorithms Leader election Logical time and global snapshots Detection of stable properties Synchronizers Link reversal algorithms "

 "L'interaction de composantes informatiques, qui calculent et communiquent, avec leur environnement régi par des lois physiques, comme pour un avion ou un système médical implanté, est au centre du domaine émergent des systèmes cyber-physiques. Parmi les défis posés par ces systèmes auxquels nous nous intéresserons, l'utilisation croissante d'algorithmes d'intelligence artificielle (réseaux de neurones typiquement), que ce soit pour la perception ou le contrôle. Maitriser la modélisation, le contrôle et la vérification du comportement de tels systèmes est crucial pour garantir l'efficacité, les fonctionnalités et la fiabilité de ces systèmes, toujours plus complexes et le plus souvent critiques en terme de sécurité ou de coût. Le cours s'attachera à trouver un équilibre entre modélisation et vérification, et entre fondations théoriques et les aspects pratiques. Il introduira notamment aux principes et à l'utilisation de quelques outils représentatifs de l'état de l'art, et s'intéressera à des cas d'étude réalistes (notamment un modèle temporel de pacemaker modélisé et vérifié avec l'outil Uppaal). Le cours est central aux thématiques de la filière Design of Intelligent Autonomous Systems, mais il est également naturel dans le parcours Electrical Engineering ou dans les filières The Internet of Everything for a Digitized Society (IOE4DS) ou Algorithms and Foundations of Programming Languages. Des sujets de projets 3A en lien avec des thématiques peuvent être proposés. Contenu: Introduction, modèles et langages synchrones Langages synchrones: spécification et vérification Automates temporisés Logique temporelle et verification par model-checking Modélisation et simulation de systèmes hybrides Analyse d'atteignabilité de systèmes hybrides Stabilité et contrôle de systèmes hybrides Sureté des systèmes autonomes intelligents Le cours est illustré par des exercices applicatifs (en cours), et par les séances de travaux pratiques utilisant différents outils de modélisation et vérification. Les quatre dernières séances sont dédiées à un projet, dans lequel l'accent pourra être mis, au choix des étudiants, sur la modélisation et vérification d'un système cyber-physique, ou sur l'étude plus poussée d'un aspect d'une méthode de vérification. Le cours sera validé pour une petite moitié sur les TPs, et la grosse moitié restante sur le projet et l'oral associé."

 " La programmation mathématique (PM) est un langage formel pour définir et resoudre un problème d'optimisation. Un programme mathématique est constitué de paramètres (l'input du problème), variables de décision (l'output), une ou plusieurs fonctions objectifs, et zéro ou plusieurs contraintes qui peuvent être données sous forme explicite ou implicite (par exemple, contraintes d'intégralité sur les variables). Les objectifs et les contraintes explicites sont éxprimés comme des fonctions des paramètres et des variables de décision. Il existe une grande variété de ""solveurs génériques"" pour les programmes mathématiques, de telle sorte qu'obtenir la solution du problème se réduit à soumettre le programme à un solveur. Ainsi, la PM réduit les difficultés algorithmiques de l'optimisation à des difficultés de modélisation. La PM est fortement utilisée dans des milieux industriels: production, logistique, gestion des ressources (humaines, financières, énergétiques et autres), télécommunications, etc., ainsi que dans les milieux de l'Information Technology de pointe: Google, Microsoft, Yahoo, Huawei embauchent plusieurs chercheurs en PM, et IBM en hébèrge une équipe entière! Ce paradigme de programmation donne lieu à une famille d'algorithmes complexes et puissants, qui incluent le calcul des solutions de problèmes d'optimisation (grâce à la PM) parmi leurs ""instructions élémentaires"". Celui-ci donne lieu à pratiquement toutes les approches en Machine Learning (ML) les plus modernes, du clustering jusqu'au traitement automatique du langage naturel. "

Driven by recent breakthroughs, rapidly growing collections of data, and a plethora of exciting applications, artificial intelligence is experiencing massive interest and investment from both the academic and industrial scene. This course selects a number of advanced topics to explore in machine learning and autonomous agents, in particular: Probabilistic graphical models (Bayesian networks, ...) Multi-output and structured-output prediction problems Deep-learning architectures Methods of search and optimization (Beam search, epsilon-approximate search, stochastic optimization, Monte Carlo methods, ...) Sequential prediction and decision making (HMMs, Sequential Monte Carlo, Bayesian Filtering, MDPs, ...) Reinforcement learning (Q-Learning, Deep Q-Learning, ...) Although these topics are diverse and extensive, this course is developed around a common thread connecting them all, such that each topic builds off the others. Lectures will cover the relevant theory, and labs will familiarize the students with these topics from a practical point of view. Several of the lab assignments will be graded, and a team project on reinforcement learning will form a major component of the grade - where the goal is to developing and deploy an agent in an environment and write a report analyzing the results.

Threats and attacks are like living organisms: some survive unaltered, mostly hidden from view, but remain deadly when conditions are “just right” ; others emerge quickly, wreck havoc, then become extinct — and yet others keep evolving, both in terms of their propagation methods and their impact. A network professional can therefore not be limited to just static application of risk assessment methodology, nor to mechanical application intrusion detection and forensics tools — and must, by nature, not simply be “following a cookbook”, but must also have a complete understanding of the whole processes, technologies, and theories involved in attacks. This program in network security is therefore not just limited to a theoretical understanding the state of the art of security standards, threats, and techniques— but tries to bring a broad systems-understanding, to be able to be proactive and identify potential attack surfaces of a system, before an attack exists, and the necessary background to be able to rapidly analyse and understand the root nature of a new attackon a system. To this end, the program alternates theoretical lectures and hands-on exercises, with seminars and “war-stories”,with 4h practice sessions during which we will be building a first-hand experience with how vulnerable real-world Internet-connected systems are — as well as with how “white-hat”IT professional constructs (more) secured computer networks. Objectives The objectives of this program is to allow students to: Not just to understand “This is an attack, and here is how to detect it”, but also to understand “What architectural choices have made this attack even possible?”. This, so as to ensure that graduates can: Go beyond just mechanically replicating recipes from a catalogue for “evaluation-detection-countermeasures” When developing a system, make appropriate, security-informed, architectural choices Distinguish between “science-facts”and “science-fiction”, when listening to security solution vendors, reading popular press, etc. Understand, analyse, and exercise critical appreciation of, the panorama of current known techniques for: Risk Evaluation Systems and Network Protection Intrusion Detection Forensics and Recovery Practice setting up secure networks, including the usage of techniques such as VLANs, VPNs, DMZs, IDSes (Snort, Suricata), Firewalls, etc. Structure To this end, the program alternates theoretical lectures, seminars, and “war-stories”,with 4h practice sessions during which we will be building a first-hand experience with how vulnerable real-world Internet-connected systems are — as well as with how “white-hat” IT professional constructs (more) secured computer networks. Requirements: A good dose of curiosity is required. As we will be studying some advanced topics in computer networking, INF557 "From the Internet to the IoT: The Fundamentals Of Modern Computer Networking" is recommended. Evaluation mechanism: Active participation during weekly TD sessions, worth 50% of the final grade, and a final exam QCM worth the other 50% of the grade. Language: English (with, at least, bilingual teaching staff)

Neural networks are now widely used in numerous applications including speech recognition, natural language processing, image segmentation, control and planning for autonomous systems. A central question is how to verify that they are correct with respect to some specification. Beyond correctness, we are also interested in questions such as explainability and fairness, that can in turn be specified as formal verification problems. The interest in explainability and validation for neural networks based systems has fostered an enormous amount of research in recent years, revisiting some older themes in formal methods. Recently, the problem of verifying properties of neural networks has been investigated extensively under a variety of contexts. A natural neural network analysis problem is that of range estimation, i.e. bounding the values of neurons on the output layer, or some function of the output neurons, given the range of neurons on the input layer. A prototypical application of range estimation is the verification of the ACAS Xu - the next generation collision avoidance system for autonomous aircrafts, which is implemented by a set of neural networks. Such a verification problem is translated into a range estimation problem over these neural network wherein the input ranges concern a set of possible scenarios and the outputs indicate the possible set of advisories provided by the network. Another prototypical application concerns the robustness of image classification wherein we wish to analyze whether a classification label remains constant for images in a neighborhood of a given image that is often specified using ranges over a set of pixels. Robustness is akin to numerical stability analysis, and for neural nets used as decision procedures (e.g. control of a physical apparatus), this is a form of decision consistency. It is also linked to the existence or non-existence of adversarial inputs, i.e. those inputs close to a well classified input data, that dramatically change the classification, and may have dire consequences. Many formal methods approaches that have been successfully used in the context of program verification seem to be successfully leveraged to the case of neural net verification: proof-theoretic approaches, SMT techniques, constraint based analyzers and abstract interpretation. In this course, we will begin by setting up the scene, and introduce formal methods as developed for program analysis and verification, and more specifically abstract interpretation based methods. Then we will show how to translate some of the successes of program verification to neural net verification. The course will include lab sessions. Evaluation will be made for 60% on a project (e.g. implementation of analysis methods for the analysis of neural nets or of programs), and 40% on a presentation of a research article.

 " L’enseignement porte sur la sécurité des systèmes d’Information avec une forte orientation sur la modélisation des risques pour les systèmes complexes. L’objectif est dans un premier temps de présenter les méthodes classiques (informelles) d’analyse de risques de sécurité pour ces systèmes. Les limitations de ces méthodes sont une justification à l’introduction d’approches plus formelles. Des exemples d’application sont pris dans le contexte de la sécurité des systèmes industriels. Les aspects d’interdépendances entre sécurité et sûreté de fonctionnement sont aussi une problématique émergente qui sera abordée. Méthodes informelles d’analyse de risques de sécurité (ISO27005, EBIOS, Mehari, Cramm, Octave, ….) Méthodes et outils pour la modélisation des attaques et défense – Arbres d’attaques – Arbres d’attaques défense – Réseaux bayésiens pour la sécurité – Graphes d’attaques Méthodes quantitatives pour l’analyse de risques – Adversary-driven state-based system security evaluation (ADVISE) – Approches basées sur la théorie des jeux,… Approches jointes Sécurité/Sûreté de fonctionnement Applications à la sécurité des systèmes complexes/industriels – Stratégies de défense optimales dans les smartgrids – Gestion des patchs dans les systèmes critiques – Détection d’intrusion dans les systèmes SCADA" SCHEDULE: Tuesday morning between September 19th and December 16th, excluding November 1st (there will be 7 classes and the exam, scheduled in that period).

This course presents the main numerical tools for the study and the analysis of continuous-time dynamical systems. Different classes of dynamical systems will be considered among ordinary differential equations, differential-algebraic equations, and differential equations with delay in the first part of the course. Numerical algorithms to solve initial value problems and two point boundary value problems will be presented as well as their stability properties emphasizing their pros and cons. The last part of the course will be an introduction to the reachability analysis of dynamical systems based on interval analysis methods. Practical exercices on computers using Matlab and C++ will help understanding the presented algorithms.

Reasoning automatically about logical formulas is crucial in solving problems in Artificial Intelligence (e.g., path and task planning) and Formal Methods (e.g., software verification). This course will present the modern, efficient algorithms (decision procedures) used to check the satisfiability (SAT) of formulas in propositional logics (e.g., Conflict Driven Clause Learning, CDCL) and the extensions of these algorithms to check more expressive first-order-logic formulas (Satisfiability Modulo Theory, SMT). The course will also present how logical modeling and satisfiability can solve problems in AI (Logical Knowledge-based agent) and formal methods (software verification). In detail, the tutorial will cover problems such as path planning, task planning, and bounded model checking to illustrate theoretical notions and practical implementation of algorithms.

Description ----------- In this cours you will learn how to build **system-level applications** that avoid by construction **memory safety issues** and **data race issues**, by relying on modern type systems. You will be introduced to **Rust** as an example of a programming language that realizes this approach and has significant industry adoption. Syllabus -------- - Memory safety - How to detect memory-safety issues in C/C++ - The Rust memory model - NULL references and how to avoid "billion dollar mistakes" - Rust language basics - Race conditions - Avoiding multiprocessing (security) pitfalls - Data races - Avoiding multithreading (security) pitfalls Meta ---- - Field: System programming and Software security - Keywords: programming, security, statictyping, memorysafety, multiprocessing, multithreading, rust - Evaluation: exam + project - Prerequisites: - operating systems foundamentals - C programming (C++ would be a plus) - POSIX programming - some experience with multithreading/multiprocessing programming

Le cours abordera la conception d'applications concurrente : modèles de concurrence, politiques d'ordonnancement, mécanismes de synchronisation. Ces concepts seront illustrés par la mise en œoeuvre de l'interface de programmation C/POSIX et par celle du modèle objet Java. Le cours portera également sur des patrons de conception pour la programmation concurrente ainsi que la vérification d'applications concurrentes.

 Cette unité d'enseignement vise à donner aux étudiants les connaissances indispensables pour la conception de systèmes temps réel embarqués critiques. Notamment, l'enseignement se concentre sur les problèmes liés à la satisfaction de contraintes non-fonctionnelles (contraintes matérielles, temporelles, etc.) dans le cadre de la conception de systèmes temps réel et souvent critiques. Plus particulièrement, le cours porte sur des aspects algorithmiques comme la théorie de l’ordonnancement, sur la conception bas niveau avec mise en œuvre sur noyaux temps réel, sur la modélisation, l’analyse et la production de code embarqué, sur les approches pour la sûreté de fonctionnement ou encore sur les standards industriels propres à l’avionique, l’automobile ou le ferroviaire. Objectifs d'apprentissage : Algorithmes et Architectures de référence Algorithmes d'ordonnancement de tâches et serveurs périodiques Systèmes et architectures dans l’avionique et l’automobile Motifs de conception pour la tolérance aux fautes Synthèse de logiciel embarqué à partir de modèle (AADL -> C) Programmation Programmation temps réel via différentes API Programmation de la tolérance aux fautes Implémentation d'un ordonnanceur Analyse et Modélisation Tests d'ordonnancement analytiques Calcul de pire temps d'exécution Définition et interprétation de modèles pour calculs de fiabilité / disponibilité pour systèmes critiques

 " Cette unité d'enseignement vise à donner aux étudiants les connaissances indispensables pour la conception de systèmes temps réel embarqués critiques. Notamment, l'enseignement se concentre sur les problèmes liés à la satisfaction de contraintes non-fonctionnelles (contraintes matérielles, temporelles, etc.) dans le cadre de la conception de systèmes temps réel et souvent critiques. Plus particulièrement, le cours porte sur des aspects algorithmiques comme la théorie de l’ordonnancement, sur la conception bas niveau avec mise en œuvre sur noyaux temps réel, sur la modélisation, l’analyse et la production de code embarqué, sur les approches pour la sûreté de fonctionnement ou encore sur les standards industriels propres à l’avionique, l’automobile ou le ferroviaire. Objectifs d'apprentissage : Algorithmes et Architectures de référence Algorithmes d'ordonnancement de tâches et serveurs périodiques Systèmes et architectures dans l’avionique et l’automobile Motifs de conception pour la tolérance aux fautes Synthèse de logiciel embarqué à partir de modèle (AADL -> C) Programmation Programmation temps réel via différentes API Programmation de la tolérance aux fautes Implémentation d'un ordonnanceur Analyse et Modélisation Tests d'ordonnancement analytiques Calcul de pire temps d'exécution Définition et interprétation de modèles pour calculs de fiabilité / disponibilité pour systèmes critiques"

The main objective of this course is the study of existing testing techniques for different types of software, mostly used in telecommunications. The students should learn how to estimate the software quality from a tester point of view and which formal models can be used to derive high quality tests or to verify the correctness of certain properties of software components of discrete event systems. - Introduction to software quality and software testing problem; classification of various testing techniques (lecture); - Motivation to Model Based Testing; introducing formal models for discrete event systems (lecture); - Finite State Machines – definitions and examples (lecture and exercises); - FSM based test generation strategies; guaranteed fault coverage (lectures and exercises); - Non-intrusive testing techniques and Passive testing (lecture and exercises); - Optimization of passive testing/monitoring techniques (lecture); - (Collaborative) project management class (laboratory and seminar).