A framework for system requirements verification in Industrial Network Systems

Industrial Control Systems (ICS) are undergoing a deep transformation of their communication infrastructures towards increased connectivity of devices and extreme flexibility of industrial plants. This is seen within the Industry 4.0 and Factory of the Future (FoF) frameworks. Innovative industrial applications exploit benefits from Software Defined Network (SDN) and Network Function Virtualization (NFV) approaches; they can bring several advantages, such as a detachment from the traditional Industrial Network design and the power to administer the entire network environment from a centralized point. As the higher flexibility of these systems will require frequent network reconfigurations, an enhanced level of automation in the management of cybersecurity will be necessary. The number of cyberattacks driven through the industrial network infrastructure is increasing; they can exploit both inadequate segregation between different network environments. Additionally, cyberattacks are increasing when the corporate network is not properly segregated from the industrial one, as well as exposed industrial systems that are potentially vulnerable. However, maintaining industrial network systems is very challenging due to their safety-critical mission inside the manufacturing process. The following thesis provides high assurance levels, as required by the safety-critical nature of these systems, by leveraging formal models and verification. Cyberattacks may have different purposes and they can cause industrial process disruption, leakage of secrets or even stealing of money. In order to face these threats, a more complex infrastructure must be deployed. On the other hand, innovative industrial applications have strict requirements on end-to-end latency during critical events. In ICS, systems involved within the network infrastructure should regularly make a decision, report data to a centralized collector, and execute a remote command with a deterministic end-to-end delay. If the operation is not completed in a specific timeslot, all the entire process may be invalidated. The consequence could vary depending on the industrial environment type. In some environments, it can cause production line breaks and only human assistance can restore the proper system functioning. There are also safety-critical systems where issues in industrial systems communication could cause ecological disaster or incidents that result in loss of life. Bringing innovation inside these particular systems is very hard to achieve. It is imperative to meet several requirements before deploying solutions inside real ICS. A solution has been designed and developed to assure formal industrial requirements verification with a particular focus on real-time control systems. This is done by exploiting the innovative approach led by SDN and NFV technologies.