TY - GEN
T1 - Cyber Physical System Integration and Configuration Guided by Satisfiability Modulo Theories
AU - Pochiraju, Kishore
AU - Narain, Sanjai
N1 - Publisher Copyright:
© 2015 IEEE.
PY - 2015/10/19
Y1 - 2015/10/19
N2 - 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.
AB - 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.
KW - Configuration
KW - Constraint-based Representation
KW - Redesign
KW - Satifiability Solvers
KW - System Requirements
UR - http://www.scopus.com/inward/record.url?scp=84959159215&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84959159215&partnerID=8YFLogxK
U2 - 10.1109/IRI.2015.93
DO - 10.1109/IRI.2015.93
M3 - Conference contribution
AN - SCOPUS:84959159215
T3 - Proceedings - 2015 IEEE 16th International Conference on Information Reuse and Integration, IRI 2015
SP - 589
EP - 592
BT - Proceedings - 2015 IEEE 16th International Conference on Information Reuse and Integration, IRI 2015
T2 - 16th IEEE International Conference on Information Reuse and Integration, IRI 2015
Y2 - 13 August 2015 through 15 August 2015
ER -