Cyber Physical System Integration and Configuration Guided by Satisfiability Modulo Theories

Cyber Physical Systems (CPS) are increasingly required to address sophisticated and complex set of stakeholder, security, regulatory policy and physical requirements. CPS employ numerous and interacting software, hardware, control and communication sub-systems that collectively address the system requirements. This paper describes a methodology that applies Satisfiability (SAT) or Satisfiability Modulo Theory (SMT) solvers to guide system architects during the integration, diagnosis, reconfiguration and/or redesign of sub-systems. The system integration problem is posed as search for a feasible configuration in a constraint-based representation. Physical, software and control behaviors of the system and the governing physical laws are translated into a network of interconnected parametric models and as algebraic and symbolic constraints. The methodology entails solving the complete set of constraints for feasible configurations. In the absence of feasible configurations, either the conflicting requirements are renegotiated or a maximally satisfiable subset of constraints is found, that then drives a redesign of sub-systems.