Abstract
Cyber Physical Systems (CPS) exist in a physical environment and
comprise both physical components and a control program.
Physical components are inherently
liable to failure and yet an overall CPS is required to operate safely, reliably and cost
effectively. This paper proposes a framework for deriving the specification
of the software control component of a CPS from an understanding of the behaviour required
of the overall system in its physical environment.
The two key elements of this
framework are (i) an extension to the use of rely/guarantee conditions to
allow specifications to be obtained systematically
from requirements (as expressed in terms of the required behaviour in the environment)
and nested assumptions (about the physical components of the CPS); and (ii) the use of
time bands to record the temporal properties required of the CPS at a number of different
granularities.
The key contribution is in combining these ideas;
using time bands overcomes a significant drawback in earlier work.
The paper also addresses the means by which the reliability of
a CPS can be addressed by challenging each rely condition in the derived specification
and, where appropriate, improve robustness and/or define weaker guarantees that
can be delivered with respect to the corresponding weaker rely conditions.
comprise both physical components and a control program.
Physical components are inherently
liable to failure and yet an overall CPS is required to operate safely, reliably and cost
effectively. This paper proposes a framework for deriving the specification
of the software control component of a CPS from an understanding of the behaviour required
of the overall system in its physical environment.
The two key elements of this
framework are (i) an extension to the use of rely/guarantee conditions to
allow specifications to be obtained systematically
from requirements (as expressed in terms of the required behaviour in the environment)
and nested assumptions (about the physical components of the CPS); and (ii) the use of
time bands to record the temporal properties required of the CPS at a number of different
granularities.
The key contribution is in combining these ideas;
using time bands overcomes a significant drawback in earlier work.
The paper also addresses the means by which the reliability of
a CPS can be addressed by challenging each rely condition in the derived specification
and, where appropriate, improve robustness and/or define weaker guarantees that
can be delivered with respect to the corresponding weaker rely conditions.
| Original language | English |
|---|---|
| Number of pages | 17 |
| Journal | Computer journal |
| DOIs | |
| Publication status | Published - 30 Apr 2019 |