{"id":239864,"date":"2016-06-17T16:10:49","date_gmt":"2016-06-17T23:10:49","guid":{"rendered":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/?p=239864"},"modified":"2016-10-04T17:35:36","modified_gmt":"2016-10-05T00:35:36","slug":"cyber-physical-systems-you-can-bet-your-life-on","status":"publish","type":"post","link":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/blog\/cyber-physical-systems-you-can-bet-your-life-on\/","title":{"rendered":"Cyber-physical systems you can bet your life on"},"content":{"rendered":"<p>By <a href=\"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/people\/wing\/\" target=\"_blank\">Jeannette M. Wing<\/a>, Corporate Vice President, Microsoft Research<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" target=\"_blank\" href=\"https:\/\/msdnshared.blob.core.windows.net\/media\/2016\/06\/Jeannette-Wing-Microsoft-13.jpg\"><img loading=\"lazy\" decoding=\"async\" class=\"alignright size-medium wp-image-6515\" src=\"https:\/\/msdnshared.blob.core.windows.net\/media\/2016\/06\/Jeannette-Wing-Microsoft-13-300x217.jpg\" alt=\"Jeannette M. Wing\" width=\"300\" height=\"217\" srcset=\"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-content\/uploads\/2016\/06\/Jeannette-Wing-Microsoft-13-300x217.jpg 300w, https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-content\/uploads\/2016\/06\/Jeannette-Wing-Microsoft-13-768x556.jpg 768w, https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-content\/uploads\/2016\/06\/Jeannette-Wing-Microsoft-13.jpg 900w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/p>\n<p><em>\u201cSelf-driving cars.\u00a0 Robots at work, at home, at play.\u00a0 Drones for package delivery and pathogen surveillance. \u00a0Energy-efficient, earthquake-proof buildings.\u00a0 Jet engines monitored and controlled by networks of sensors and actuators.\u00a0 Embedded medical devices.\u00a0 Unobtrusive assistive technology.\u00a0 What is common to these systems?\u00a0 They have a computational core that interacts with the physical world.\u00a0 These cyber-physical systems require tight conjoining and coordination between the computational (discrete) and the physical (continuous) worlds.\u00a0 Cyber-physical systems are penetrating every aspect of our lives, with profound impact on sectors including aerospace, agriculture, automotive, chemical production, civil infrastructure, energy, entertainment, finance, healthcare, manufacturing, materials, retail, and transportation.<\/em><\/p>\n<p><em>In the future, cyber-physical systems will rely less and less on human control and more and more on the intelligence embodied in the computational core.\u00a0 In some cases, such as an automated brake system in a car, this computational core may be able to detect and respond faster than a human; in some cases, such as robotic surgery, this computational core can be more precise than a human and not prone to fatigue; and in some cases, such as a minefield, an icefield, or a volcano, we would rather risk the expense of a machine over the life of a human.\u00a0 In all cases, it will be the software that provides much of the intelligence of the computational core.<\/em><\/p>\n<p><em>Our daily lives will depend more and more on these systems.\u00a0 Our lives, our money, our welfare.\u00a0 How can we design cyber-physical systems that we can bet our lives on?\u201d<\/em><\/p>\n<p>\u2014From \u201c<a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/lazowska.cs.washington.edu\/initiatives\/WingCRN.pdf\" target=\"_blank\">Cyber-Physical Systems<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>,\u201d by Jeannette M. Wing, <em>Computing\u00a0Research\u00a0News,\u00a0<\/em>Vol. 20, No. 1, January 2008.<\/p>\n<p>To ensure cyber-physical systems are safe, we need to address two fundamental scientific challenges.\u00a0 First, we need to reason about the discrete and continuous at the same time.\u00a0 Fortunately, much progress in formal verification has been made in the past 20 years on this front.\u00a0 One approach is to model a cyber-physical system as a hybrid automaton, which is a finite state machine where each state\u2019s behavior is defined by a set of differential equations over continuous variables.\u00a0 Model checking technology can be applied to hybrid automata, making it feasible to prove properties about and find bugs in models of cyber-physical systems.<\/p>\n<p>Another approach is to write logical formulae describing the behavior of a hybrid system and then use theorem proving technology to prove properties from the formulae.\u00a0 An example of an appropriate logic in which to write such formulae is differential dynamic logic, developed within the last decade along with rich tool support.\u00a0\u00a0 Active research addresses the scalability of these techniques, since currently they support only tens of state variables, whereas an operational cyber-physical system typically has orders of magnitude more.<\/p>\n<p>Second, cyber-physical systems operate under the presence of uncertainty.\u00a0 This uncertainty is due external conditions not under system control: Mother Nature, e.g., earthquakes, hurricanes and snowstorms; and The Human, acting mistakenly, surprisingly or maliciously.<\/p>\n<p>Uncertainty is also due to system failures or approximations, such as faulty sensors and actuators, and noisy or inaccurate data.\u00a0 Again, the research community is exploring many approaches for modeling and reasoning about uncertainty.\u00a0 Common to many of these approaches is the use of probabilities, which can characterize the likelihood of a certain event happening.\u00a0\u00a0 Probabilistic models and probabilistic logics are well-studied and, as applied to cyber-physical systems, active areas of research.\u00a0\u00a0 An emerging area of relevant research is probabilistic programming.\u00a0 Here, values of program variables are randomly drawn from probability distributions and probabilistic inference calculates the implicit distribution specified by a probabilistic program.<\/p>\n<p><em>Intelligent<\/em> cyber-physical systems get much of their intelligence from the use of machine learning, which also introduces approximation and requires probabilistic and statistical reasoning.\u00a0 For example, a camera acting as a sensor on a drone might use a classifier trained to determine whether the drone is too close to a wall.\u00a0 It is in this context that <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/people.eecs.berkeley.edu\/~dsadigh\/\" target=\"_blank\">Dorsa Sadigh<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> and <a href=\"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/people\/akapoor\/\" target=\"_blank\">Ashish Kapoor<\/a> are presenting their recent paper, \u201cSafe Control under Uncertainty with Probabilistic Signal Temporal Logic\u201d at the <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" rel=\"noopener noreferrer\" href=\"http:\/\/www.roboticsconference.org\/\" target=\"_blank\">2016 Robotics: Science and Systems conference<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>.\u00a0 Their work marries formal verification and machine learning through a logic that embeds Bayesian Graphical models.\u00a0 In their Probabilistic Signal Temporal Logic, we can express safety properties of control systems that are aware of whether a predictive system would work or fail.\u00a0 Microsoft researchers and their academic colleagues are now investigating how to expand PrSTL into full-fledged probabilistic programs, including efficient Bayesian inference, which would allow real-time decision making.\u00a0 This work is part of the larger Microsoft Research Safe CPS Expedition.<\/p>\n<p>Now, here is the irony.\u00a0 To prove the safety of cyber-physical systems, we need to deal with uncertainty.\u00a0 To reduce this uncertainty, cyber-physical systems are outfitted with more and more sensors to \u201csee\u201d their environment and to monitor their internal state.\u00a0 To interpret signals from a multitude of these sensors, we rely on statistical machine learning and optimization techniques.\u00a0 But these techniques give us only an approximation of the system\u2019s external world that then determines its next state.\u00a0 And so, inherently these approximations add another dimension of uncertainty.\u00a0 Eek!<\/p>\n<p>The meeting of formal methods, programming languages, control theory, real-time systems, machine learning, optimization and robotics is exactly what we need to ensure that future cyber-physical systems are safe: They should do no harm.\u00a0 Much exciting research remains for the scientific and engineering communities to tackle the fundamental and practical challenges to achieve this goal.<\/p>\n<p>We are moving toward a world where self-driving cars, commercial drones and mobile robots share the same physical space as humans, where embedded medical devices improve through software updates, and where machine learning routinely supports smarter decision-making by these systems.\u00a0 This world requires that we, as scientists and engineers, take responsibility for building cyber-physical systems that you can bet your life on.<\/p>\n<p><em>Photo credit: Scott Eklund\/Red Box pictures<\/em><\/p>\n<p><strong>Related:<\/strong><\/p>\n<ul>\n<li><a href=\"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/expeditions-exploring-the-unknown\/\">Expeditions: Exploring the Unknown<\/a><\/li>\n<li><a href=\"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/microsofts-jeannette-m-wing-to-judge-100-million-macarthur-foundation-competition\/\">Microsoft\u2019s Jeannette M. Wing to judge $100 million MacArthur Foundation competition<\/a><\/li>\n<li><a href=\"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/microsofts-jeannette-m-wing-basic-research-is-the-foundation-of-american-prosperity-and-progress\/\">Wing: Basic research is \u2018the foundation of American prosperity and progress\u2019<\/a><\/li>\n<li><a href=\"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/computational-thinking-10-years-later\/\">Computational thinking, 10 years later<\/a><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>By Jeannette M. Wing, Corporate Vice President, Microsoft Research \u201cSelf-driving cars.\u00a0 Robots at work, at home, at play.\u00a0 Drones for package delivery and pathogen surveillance. \u00a0Energy-efficient, earthquake-proof buildings.\u00a0 Jet engines monitored and controlled by networks of sensors and actuators.\u00a0 Embedded medical devices.\u00a0 Unobtrusive assistive technology.\u00a0 What is common to these systems?\u00a0 They have a computational [&hellip;]<\/p>\n","protected":false},"author":39507,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":[],"msr_hide_image_in_river":0,"footnotes":""},"categories":[194467,194473,194482,194455],"tags":[205652,205655,205658,205661,205664],"research-area":[13556],"msr-region":[],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[],"class_list":["post-239864","post","type-post","status-publish","format-standard","hentry","category-artifical-intelligence","category-cyber-physical-systems","category-hybrid-intelligence","category-machine-learning","tag-2016-robotics-science-and-systems-conference","tag-bayesian-graphical-models","tag-cyber-physical-systems","tag-probabilistic-signal-temporal-logic","tag-safe-cps-expedition","msr-research-area-artificial-intelligence","msr-locale-en_us"],"msr_event_details":{"start":"","end":"","location":""},"podcast_url":"","podcast_episode":"","msr_research_lab":[],"msr_impact_theme":[],"related-publications":[],"related-downloads":[],"related-videos":[],"related-academic-programs":[],"related-groups":[],"related-projects":[],"related-events":[],"related-researchers":[],"msr_type":"Post","byline":"","formattedDate":"June 17, 2016","formattedExcerpt":"By Jeannette M. Wing, Corporate Vice President, Microsoft Research \u201cSelf-driving cars.\u00a0 Robots at work, at home, at play.\u00a0 Drones for package delivery and pathogen surveillance. \u00a0Energy-efficient, earthquake-proof buildings.\u00a0 Jet engines monitored and controlled by networks of sensors and actuators.\u00a0 Embedded medical devices.\u00a0 Unobtrusive assistive technology.\u00a0&hellip;","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/posts\/239864","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/users\/39507"}],"replies":[{"embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/comments?post=239864"}],"version-history":[{"count":2,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/posts\/239864\/revisions"}],"predecessor-version":[{"id":278412,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/posts\/239864\/revisions\/278412"}],"wp:attachment":[{"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/media?parent=239864"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/categories?post=239864"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/tags?post=239864"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=239864"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=239864"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=239864"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=239864"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=239864"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=239864"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=239864"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/cm-edgetun.pages.dev\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=239864"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}