Lecture 19 - UPPAAL Model Checking Tutorial [PoM-CPS] скачать в хорошем качестве

Lecture 19 - UPPAAL Model Checking Tutorial [PoM-CPS]

Principles of Modeling for Cyber-Physical Systems [PoM-CPS] Course Website: https://linklab-uva.github.io/modelin... Instructor: Dr. Madhur Behl, Assistant Professor, Computer Science, University of Virginia “Essentially, all models are wrong, but some are useful” [George Box, 1976] … This course is about building useful models.! Design of complex and reliable cyber-physical systems (CPS) requires the creation of mathematical models, both of the environment and of the system itself. Such models allow us to analyze, control, verify, and optimize a system’s performance. The modeling choice is largely dictated by the intended use of the model plus the intricacies of the underlying physical domain. This course will provide a solid foundation for understanding different modeling paradigms, and explore them through a deep dive and hands on implementation for three CPS domains: Energy, Medical, and Automotive cyber-physical systems. You will come out of this course with advanced and transferrable knowledge of model-based design methods and tools, and will be ready for tackling multi-disciplinary systems projects. In addition, you will become domain experts in energy, medical, and automotive cyber-physical systems. See the attached course handout for a detailed list of topics to be covered. Energy CPS modeling + predicitve control – Buildings consume nearly half of all energy produced in the United States. 75% of all electricity produced in the U.S. is used to just operate buildings. You will learn how first-principles of physics can be used to create a ‘thermal’ RC-network model of the energy-use dynamics of any building. We will train and evaluate these models using real data from buildings. We will then use these models to optimize the operation of the building’s heating, ventilation, and air-conditioning (HVAC), and lighting systems to make them more energy and cost-efficient. We will also explore alternative data-driven methods for building modeling. You will learn to use the following tools: EnergyPlus, MLE+,Matlab (SysID,StateSpace) Medical CPS modeling + model checking - Life-saving medical devices, like pacemakers and defibrillators, require a rigorous approach to verifying their safety. How do we ensure that the software on implantable medical devices will perform safely under all conditions? We will first tackle the question: How do you mathematically model the human heart? We will use timed automata to create a virtual heart electrophysiology model which will allow us to formally verify implantable cardiac devices. You will learn about the principles model checking, and verification. You will learn to use the following tools: Simulink, StateFlow, UPPAAL Automotive CPS modeling + end-to-end learning – End-to-end learning where direct camera inputs can be converted into control actions for an autonomous vehicle is redefining the way we think about modeling automotive systems. In this fast paced module, you will learn about how to model and test automotive control systems. You will learn how to generate code directly from the model implementation. We will then learn about deep convolution networks and use them for designing an end-to-end learning module for a self driving car. You will learn to use the following tools: TORCS, TensorFlow,