tycho-bro-hey / physical-spud

RFD: Cyber-Physical System Model

Cyber-physical systems (CPSs) are the integration of computation with physical processes whose behavior is defined by both cyber and physical parts. At the physical interface, we have a computer that is providing inputs to physics. This computational component is programmed to manipulate the external, physical world to perform an intended function.

If we wish to fully understand the behavior of cyber-physical systems in a comprehensive model and ensure security, safety, and resilience at the physical interface, then we must include the continuous dynamics of the physical world and how the discrete computers interact with it. With a comprehensive model, then we may be able to fully comprehend the behavior of the physical world when a computer is attempting to manipulate it. To this end, we will be able to identify the security, safety, and resilience properties that must exist in order to ensure the physical asset is protected.

Modeling of Cyber-Physical Systems

Modelica is an object-oriented, declarative, multi-domain modeling language that enables component-oriented modeling and simulation of complex cyber-physical systems. The FCS-IT consist of several integrated modules that simulate a factory and manufacturing process. Within each module are cyber-physical components that sense and control the physical processes. PSaR is modeling and simulating these components using Modelica in order to have a concise understanding of the cyber-physical behavior of the FCS-IT and provide formal specification of requirements.

Using a model that represents the cyber-physical interactions of the FCS-IT, properties of its behavior are formalized using a candidate formal specification language. PSaR is capturing the specifications in linear temporal logic (LTL) and in a second candidate language for a 'check twice and compare' approach to ensure correctness. These specifications include type checking, initialization of system states, and state transitions. PSaR is using a model checking-based approach to verify that the behavior of the FCS-IT satisfies the formalized specifications. As a result, the verified model is used during runtime to verify properties and to detect any abnormal behavior that may violate them

Fischertechnik Training Factory Industry 4.0

The Fischertechnik Training Factory Industry 4.0 is an environment used for learning and understanding Industry 4.0 applications. This application simulates ordering, production, and delivery processes for a manufacturing system. We aim to use application as an embedded research platform for securing industrial control systems.