Open CPS: A Symbolic Model

Modeling of the environment presents a challenge in all open systems, particularly in open cyber-physical systems where the environment is nature. In some cases the environment can be considered and modeled as yet another actor or component in the system. However, in cases of complex systems with intricate interactions with nature as their environment, the unpredictability of this environment and the complexity of the physics involved in its modeling make “environment as a component” an untenable approach. Concurrent Rules Machines (CRMs) constitute a model for formal specification and analysis of open, distributed cyber-physical systems [3]. The CRM model makes interaction with the environment explicit and offers an algebra of composition and decomposition for construction and analysis of systems through their constituent components. Systematic and automatic verification of properties of systems modeled as CRMs remains a significant challenge. Symbolic representations have been used to model the inherently continuous properties of physics. In this paper we introduce symbolic execution as a means of reasoning about behaviors of CRM models. A symbolic execution represents possibly infinitely many executions and can focus on environments meeting requirements such as physically reasonable actions. We show that symbolic execution is sound, and is complete for a natural class of CRMs. We illustrate our ideas with a simple cyber-physical system example.

• View at Publisher