Verifying Response Times in Networked Automation Systems Using Jitter Bounds

TL;DR

This paper presents a formal verification method for response times in Networked Automation Systems using jitter bounds and model templates, demonstrated on an industrial steam boiler.

Contribution

It introduces a novel approach combining jitter bounds with model templates for verifying NAS response times during design.

Findings

Effective verification of response times using jitter bounds

Model templates simplify timing fluctuation analysis

Validated method on industrial steam boiler

Abstract

Networked Automation Systems (NAS) have to meet stringent response time during operation. Verifying response time of automation is an important step during design phase before deployment. Timing discrepancies due to hardware, software and communication components of NAS affect the response time. This investigation uses model templates for verifying the response time in NAS. First, jitter bounds model the timing fluctuations of NAS components. These jitter bounds are the inputs to model templates that are formal models of timing fluctuations. The model templates are atomic action patterns composed of three composition operators- sequential, alternative, and parallel and embedded in time wrapper that specifies clock driven activation conditions. Model templates in conjunction with formal model of technical process offer an easier way to verify the response time. The investigation demonstrates the proposed verification method using an industrial steam boiler with typical NAS components in plant floor.