Logical Foundations of Cyber-Physical Systems， And

文件名称: Logical Foundations of Cyber-Physical Systems

所属分类: 其它

开发工具:

文件大小: 10mb

下载次数: 0

上传时间: 2019-07-04

提供者: weixin_********

下载 (10mb)

不能下载？报告错误

详细说明：Logical Foundations of Cyber-Physical Systems， André Platzer， 2018Andre platzer Logical Foundations of Cyber-Physical Systems Springer Andre platzer Computer Science department Carnegie mellon university Pittsburgh, Pennsylvania, USA The content of the book and the image used on the book cover are based upon work performed at Carnegie Mellon University and supported by the National Science Foundation under NSF CAREER Award CNs-1054246 ISBN978-3-319-63587-3 ISBN978-3-319-63588-0( eBook) https://doi.org/10.1007/978-3-319-63588-0 Library of Congress Control Number: 2018946565 o Springer International Publishing ag, part of springer Nature 2018 This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or nformation storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology now known or hereafter developed The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use The publisher, the authors and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication neither the publisher nor the authors or the editors give a warranty, express or implied, with respect to the material contained herein or for any errors or omissions that may have been made. The publisher remains neutral with regard to s and institutional affiliate nted on acid-free pape This Springer imprint is published by the registered company Springer Nature Switzerland AG The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland Endorsements This excellent textbook marries design and analysis of cyber-physical systems with a logical and computational way of thinking. The presentation is exemplary for find ing the right balance between rigorous mathematical formalization and illustrative case studies rooted in practical problems in system design Rajeev alur, University of Pennsylvania This book provides a wonderful introduction to cyber-physical systems, covering fundamental concepts from computer science and control theory from the perspec tive of formal logic. The theory is brought to life through many didactic examples illustrations, and exercises. A wealth of background material is provided in the text and in an appendix for each chapter, which makes the book self-contained and ac cessible to university students of all levels Goran Frehse, Universite Grenoble alpes TThe author] has developed major important tools for the design and control of those cyber-physical systems that increasingly shape our lives. This book is a 'must for computer scientists, engineers, and mathematicians designing cyber-physical systems Anil nerode. Cornell universit As computing interfaces increasingly with our physical world, resulting in So- called cyber-physical systems, our foundations of computing need to be enriched with suitable physical models. This book strikes a wonderful balance between rig orous foundations for this next era of computing with illustrative examples and ap lications that drive the developed methods and tools a must read book for anyone interested in the development of a modern and computational system science for cyber-physical systems George J. Pappas, University of Pennsylvania This definitive textbook on cyber-physical systems lays the formal foundations of their behavior in terms of a single logical framework platzer 's logic stands out among all other approaches because it provides a uniform treatment of both the di crete and continuous nature of cyber-physical systems, and does not shy away from their complex behavior due to stochasticity, uncertainty, and adversarial agents in the environment. His computational thinking approach makes this work accessible to practicing engineers who need to specify and verify that cyber-physical systems are safe Jeannette M. wing, Columbia university oreo I first met Andre when he was just finishing his PhD and gave a job talk at CMU (he got the job). I was a visiting researcher and got to take the young faculty candidate out for lunch. Andre talked about verifying cyber-physical systems( CPS)using differential dynamic logic" and theorem proving i was skeptical, for one because related approaches had only seen modest success, and also because my money was on a different horse. A few years before, I had developed a model checker(PhAVer) and was working on a second one, called spaceX. at the time these were the onl verification tools that, on the push of a button, could verify certain benchmarks from CPS and other domains involving continuous variables that change with time. I was quite proud of them and, for me, algorithmic verification was the way to go. But Andre was determined to make theorem proving work in practice, and indeed he advanced the field to an extent that i did not think possible. andre and his team first developed the logical framework, then built a very capable theorem prover for CPs (KeY maera), successfully applied it to industrial case studies like airplane collision avoidance, and, finally, addressed important application issues such as validating the model at runtime The book in front of you provides a comprehensive introduction on how to rea son about cyber-physical systems using the language of logic and deduction. Along the way you will become familiar with many fundamental concepts from computer science, applied mathematics and control theory all of which are essential for CPS The book can be read without much prior knowledge, since all necessary back- ground material is provided in the text and in appendices for many chapters. The book is structured in the following four parts. In the first part, you will learn how to model CPs with continuous variables and programming constructs, how to specify requirements and how to check whether the model satisfies the requirements using proof rules. The second part adds differential equations for modeling the physical world. The third part introduces the concept of an adversary, who can take actions that the system can not influence directly. In a control system, the adversary can be the environment, which influences the system behavior through noise and other disturbances. Making decisions in the presence of an adversary means trying to be prepared for the worst case. The fourth part adds further elements for reasoning soundly and efficiently about systems in applications, such as using real arithmetic and- my favorite- monitor conditions. monitor conditions are checked while the system is in operation. As long as they hold, one can be sure that not only the model but also the actual CPS implementation satisfy the safety requirements By now Andre and his group have handled an impressive number of case studies that are beyond the capabilities of any model checker i know. fortunately for me and my horse, the converse is also still true, since some problems can in practice only be solved numerically using algorithmic approaches. If your goal is to obtain a rock-solid foundation for CPS from the beautiful and elegant perspective of logics then this is the book for you Goran Frehse, Associate Professor, Universite Grenoble Alpes, Grenoble, 2017 Acknowledgements This textbook is based on the lecture notes for the Foundations of Cyber-Physical Systems undergraduate course i taught in the Computer Science Department at Carnegie Mellon University. The textbook would have been impossible without the feedback from the students and helpful discussions with the teaching assis ants Joao Martins. Annika Peterson. Nathan Fulton. Anastassia Kornilova. Bran don Bohrer, and especially Sarah Loos who TAed for the first instance in Fall 2013 and co-instructed for the intensive courses at ENS Lyon, France, in Spring 2014 and at MAP-1, Braga, Portugal in Summer 2014. Based on the experience with earlier Ph. D.level courses, this course was originally designed as an undergraduate course but then extended to masters students and eventually ph. D. students I appreciate the feedback of all my students on this textbook, but also by my post docs stefan Mitsch, Jean-Baptiste Jeannin, Khalil Ghorbal, and Jan-David Quesel I am especially thankful to Sarah Loos's formative comments on the earliest draft and Yong Kiam Tan's careful extensive feedback for the final version. I am also grate ful to Jessica Packer's exhaustive consistency checking on the textbook structuring and to julia platzer for crucial advice on illustrations. i am most indebted to the de velopers Stefan Mitsch and Nathan Fulton of the KeY maera X prover for verifying cyber-physical systems, and very much appreciate also the Key maera X contribu tions by Brandon Bohrer, Yong Kiam Tan, Jan-David Quesel, and Marcus volp For help with the book process, I am grateful to the copyeditor and ronan Nugent rom Springer. Especially, however, I thank my family, without whose patience and support this book would not exist This textbook captures findings from the NsF CAREEr award on Logical Foun dations of Cyber-Physical Systems, which I am very grateful to have received. I also benefitted from Helen Gills advice as a program manager when this project started Funding This material is based upon work supported by the National Science Foundation under nsf career award cNs-1054246 any opinions, findings and conclusions or recommendations expressed in this publication are those of the author(s)and do not necessarily reflect the views of the National science foundation Pittsburgh, December 2017 Andre Platzer Disclaimer This book is presented solely for educational purposes. While best efforts have been ed in preparing this book, the author and publisher make no representations or warranties of any kind and assume no liabilities of any kind with respect to the accuracy or completeness of the contents and specifically disclaim any implied war- ranties of merchantability or fitness of use for a particular purpose. Neither the au thor nor the publisher shall be held liable or responsible to any person or entity with respect to any loss or incidental or consequential damages caused, or alleged to have been caused, directly or indirectly, by the information contained herein. No warranty may be created or extended by sales representatives or written sales materials Contents 1 Cyber-Physical Systems: Overview 1.1 Introduction 1.1.1 Cyber-Physical Systems Analysis by Example 1. 1. 2 Application Domains 1.1.3 Significance 1.1.4 The Importance of Safet 1.2 Hybrid Systems Versus Cyber-Physical Systems 234467 1. 3 Multi-dynamical Systems 1. 4 How to Learn about Cyber-Physical Systems 10 1.5 Computational Thinking for Cyber-Physical Systems 12 1.6 Learning Objectives 1. 7 Structure of This Textbook 15 1. 8 Summary 18 References ...19 Part I Elementary Cyber-Physical Systems 25 2 Differential Equations domains 2.1 Introduction 7 2.2 Differential Equations as Models of Continuous Physical Processes 28 2.3 The Meaning of Differential Equations 2. 4 A Tiny Compendium of Differential Equation Examples ..... 33 2.5 Domains of Differential equations 39 2.6 Syntax of Continuous Programs 41 2.6.1 Continuous Programs 41 2. 6.2 Terms 42 2.6.3 First-Order formulas 2.7 Semantics of Continuous programs .45 2.7.1 Terms 45 ontents 2.7.2 First-Order formulas 2.7.3 Continuous programs 51 2.8 Summar 52 2.9 Appendix · 53 2.9.1 Existence Theorems 2.9.2 Uniqueness Theorems 54 2.9.3 Linear Differential Equations with Constant Coefficients . 55 2.9.4 Continuation and Continuous Dependency Ex xercises 58 References 61 3 Choice Control 3.1 Introduction ..63 3.2 A Gradual Introduction to hybrid Programs 3.2.1 Discrete Change in Hybrid programs 66 3.2.2 Compositions of hybrid programs 66 3.2.3 Decisions in Hybrid Programs 68 3.2.4 Choices in Hybrid Programs 3.2.5 Tests in Hybrid Programs 71 3.2.6 Repetitions in Hybrid Programs 3.3 Hybrid Programs 75 3.3.1 Syntax.... ....75 3.3.2 Semantics 3.4 Hybrid Program Design 82 3.4.1 To Brake, or Not to Brake, That Is the Question 8 3.4.2 A Matter of Choice 83 3. 5 Summary 3.6 Appendix: Modeling the motion of a robot around a bend 85 Exercises References 92 4 Safety Contracts 95 4.1 Introduction 95 4.2 A Gradual Introduction to CPS Contracts 97 4.2.1 The Adventures of Quantum the Bouncing Ball 98 4.2.2 How Quantum Discovered a Crack in the Fabric of Time.. 101 4.2.3 How Quantum Learned to Deflate 4.24 Postcondition Contracts for CPS···. 103 .105 4.2.5 Precondition Contracts for CPs 106 4.3 Logical Formulas for Hybrid Programs 107 4.4 Differential Dynamic Logic .110 4.4.1 Syntax 110 4.4.2 Semantics l12 4.5 CPS Contracts in Logic 115 4.6 Identifying requirements of a CPs .118

(系统自动生成,下载前可以参看下载内容)