Efficient Decision Procedures for Design Exploration and Reasoning About Heterogeneous Systems

We are investigating methodologies, algorithms, and decision procedures to enable automated analysis, synthesis, and design space exploration of cyber-physical systems. Our research in this area is supported by the National Science Foundation (NSF), the Defense Advanced Research Projects Agency (DARPA), and the Office of Naval Research (ONR).

Scalable Decision Procedures for Cyber-Physical System Verification and Synthesis

The design of cyber–physical systems (CPSs) requires methods and tools that can efficiently reason about the interaction between discrete models, e.g., representing the behaviors of “cyber” components, and continuous models of physical processes. Boolean methods such as satisfiability (SAT) solving are successful in tackling large combinatorial search problems for the design and verification of hardware and software components. On the other hand, problems in control, communications, signal processing, and machine learning often rely on convex programming as a powerful solution engine. However, despite their strengths, neither approach would work in isolation for CPSs. We are interested in frameworks, algorithms, and tools that integrate SAT solving and convex optimization to efficiently reason about Boolean and convex constraints at the same time and tackle combinatorial problems over discrete and continuous variables. Applications include a variety of design and verification problems: spacecraft docking mission control, robotic motion planning, secure state estimation, bounded model checking of hybrid automata, static analysis of software, verification and synthesis for artificial intelligence (AI)-enabled system in unstructured and uncertain environments.

Relevant Papers:

• P. Nuzzo, A. Puggelli, S. A. Seshia, A. Sangiovanni-Vincentelli, “CalCS: SMT Solving for Non-linear Convex Constraints,” Proc. IEEE Formal Methods in Computer-Aided Design (FMCAD), pp. 71-79, Oct. 2010.
• Y. Shoukry, P. Nuzzo, A. L. Sangiovanni-Vincentelli, S. A. Seshia, G. J. Pappas, P. Tabuada, “SMC: Satisfiability Modulo Convex Programming,” Proc. IEEE, vol. 106, no. 9, pp. 1655-1679, Sep. 2018.
• Y. Shoukry, M. Chong, M. Wakaiki, P. Nuzzo, A. Sangiovanni-Vincentelli, S. A. Seshia, J. P. Hespanha, P. Tabuada, “SMT-Based Observer Design for Cyber-Physical Systems Under Sensor Attacks,” ACM Trans. Cyber-Phys. Syst. (TCPS), vol. 2, no. 1, pp. 5, 2018.
• Y. Shoukry, P. Nuzzo, A. Puggelli, A. Sangiovanni-Vincentelli, S. A. Seshia, P. Tabuada, “Secure State Estimation for Cyber-Physical Systems Under Sensor Attacks: A Satisfiability Modulo Theory Approach,” IEEE Transactions on Automatic Control, vol. 62, no. 10, pp. 4917-4932, Oct. 2017.
• X. Sun, R. Nambiar, M. Melhorn, Y. Shoukry, P. Nuzzo, “DoS-Attack-Resilient Multi-Robot Temporal Logic Motion Planning ,” Proc. International Conference on Robotics and Automation (ICRA), pp. 6051-6057, May 2019.

ArchEx: Cyber-Physical System Architecture Exploration

We investigate efficient optimization-based algorithms for the exploration of large, hybrid (discrete/continuous) design spaces and the selection of cyber–physical system (CPS) architectures. A special focus has been on algorithms that combine concepts from satisfiability modulo theory (SMT) solving and mathematical programming with an approximate calculus for efficiently quantifying reliability properties of complex systems. The reliability calculus provides compact analytic expressions for the failure probability of complex CPS architectures with a guaranteed bound on the approximation errors. ArchEx, a toolbox for the design exploration and optimized selection of CPS architectures, implements these algorithms and introduces a pattern-based domain-specific language to enable formal, yet flexible, specification of the design requirements. Applications range from aircraft power distribution networks to reconfigurable automated production lines and wireless networks.

Relevant Papers:

• P. Nuzzo, N. Bajaj, M. Masin, D. Kirov, R. Passerone, A. Sangiovanni-Vincentelli, “Optimized Selection of Reliable and Cost-Effective Safety-Critical System Architectures,” IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, to appear, 2020.
• D. Kirov, P. Nuzzo, R. Passerone, A. L. Sangiovanni-Vincentelli, “Optimized Selection of Wireless Network Topologies and Components via Efficient Pruning of Feasible Paths,” Proc. Design Automation Conference (DAC), p. 179, Jun. 2018.
• D. Kirov, P. Nuzzo, R. Passerone, A. L. Sangiovanni-Vincentelli, “ArchEx: An Extensible Framework for the Exploration of Cyber-Physical System Architectures,” Proc. Design Automation Conference (DAC), pp. 1-6, June 2017.
• A. Moin, P. Nuzzo, A. L. Sangiovanni-Vincentelli, J. Rabaey, “Optimized Design of a Human Intranet Network,” Proc. Design Automation Conference (DAC), p. 30, June 2017.