Formal Methods and Toolsuites for CPS Security, Safety and Verification

Speaker: John Baras

Abstract

In these five lectures we present a general rigorous methodology for model-based systems engineering for cyber-physical systems (CPS), which uses in several key steps traditional and novel formal methods, and more specialized applications and deeper results in several areas.

In lectures 1 and 2, we present a rigorous MBSE methodology, framework and tool-suites for CPS. Advances in Information Technology have enabled the design of complex engineered systems, with large number of heterogeneous components and capable of multiple complex functions, leading to the ubiquitous CPS. These advances have, at the same time, increased the capabilities of such systems and have increased their complexity to such an extent that systematic design towards predictable performance is extremely challenging, if not infeasible with current methodologies and tools. These rapidly expanding advances create tremendous opportunities for novel software systems use as both system components as well as design-manufacturing-operation tools, and consequently the need for developing novel formal methods for testing-validation-verification. The need to address both the cyber and the physical components leads to a critical need for new formal models beyond the current ones. The methodology and framework we present is aimed at catalyzing the development and use of interoperable methods and tools. We describe the fundamental components in this MBSE methodology and framework and the associated challenges: Architectures, Integrated Modeling Hubs, Development of System Structure and Behavior Formal Models, Allocation of Behavior to Structure, Tradeoff Analysis and Design Space Exploration, Requirements Management, Testing-Validation-Verification. We emphasize the importance of linking multiple physics and cyber models through metamodeling, the run-time interaction between design space exploration and system models, and the current lack of integrated modeling and testing of requirements via formal models of various kinds. The methodology proposes such an integration via the use of various formal models for requirements ranging from timed automata to timed Petri-Nets and several others, and the integration of model checking, contract based design and automatic theorem proving. We next describe applications to several important technological problems: power grids, autonomous cars, aerospace, energy efficient buildings, sensor and communication networks, smart manufacturing, robotics, unmanned air vehicles, health care, cyber-security, drug discovery and manufacturing, disease modeling and analysis. We describe the new fundamental challenges faced when we consider networked CPS and when incorporating humans as elements of such complex systems, a subject of rapidly increasing importance in view of the “networked society”, the IoT, and the “interconnected coevolving sociotechnical networks” paradigms. We describe a novel formal method to control the complexity of design space exploration by grouping questions about related design variables that leads to provably faster response to design queries by several orders of time scale. We close with a description of what is lacking, research challenges and future promising research directions.

In lectures 3 and 4, we present several methods addressing the key problem of motion planning and controls with safety and temporal constraints. The lectures are organized in the four parts described below.

Part I: Reachable set based safety verification and control synthesis

– I.1 Reachable set based verification

– I.2 Control synthesis using optimization

Part II: Motion planning for temporal logics with finite time constraints

– II.1 Mixed integer optimization based method

– II.2 Timed automata based method

Part III: Event –Triggered Controller Synthesis for Dynamical Systems with Temporal Logic Constraints

Part V: Event –Triggered Feedback Control for Signal Temporal Logic Tasks

We describe the strengths and weaknesses of each method and provide explicit application examples. We emphasize the key challenge of developing an integrated framework for handling finite temporal and finite space tolerances (requirements, constraints).

In lecture 5 we present several detailed vignettes in: Security and Trust in Networked Systems, Automotive CPS, Stable Path Routing in MANET, Composable and Assured Autonomy. The lecture is organized in the four parts described below.

Part I: Security and Trust in Networks and Networked Systems

Part II: Hardware Software Co-design for Automotive CPS using Architecture Analysis and Design Language

Part III: Distributed Topology Control for Stable Path Routing in Multi-Hop Wireless Networks

Part IV: Composable and Assured Autonomy

We introduce novel formal methods employing various partial ordered semirings, which we use for modeling and evaluating trust and for analyzing multi-metric problems on networks and graphs (multigraphs). We showed an example linking the MBSE methodology to hardware design for automotive controllers. We discussed the challenge and need for composable security and described some initial steps towards achieving this goal.