Information Technology Reference
In-Depth Information
While such a layered approach is highly beneficial for a separation of concerns
in design processes, the inherent differences between models situated at different
layers make it a challenge to provide semantic bridges between these, as would
be required for a complete verification methodology spanning all three levels.
Indeed, models at the control layer would hardly be able to exactly realize
the trajectories prescribed by strategies at the cooperation layer. While highly
elaborated plant models are available, e.g., capturing car dynamics, control de-
signers typically work with simplified models which have been proven to be
practically sucient for validating stability and safety. Such simplified models
ignore higher-order effects and use linear approximations whenever reasonably
possible, trading exactness for simulation speed. Similarly, the induced limita-
tions of digital control (cf. [3]) make it impossible for digital controllers to enforce
the plant dynamics of control models; rather, robustness is designed into digital
controllers to “suciently” approximate such dynamics.
Industrial design processes cater for these gaps, e.g., by enforcing design for
robustness, re-validating stability and safety at each layer, in particular ensur-
ing complete traceability of safety requirements throughout all design steps,
and by rapid prototyping. Extensions to Matlab-Simulink such as the Jitterbug
[10] allow for an early assessment of the impact of design level impurities on
control-strategies.
However, as argued in Section 8, theoretical approaches to cover multi-layered
designs, such as refinement and compositional reasoning, fail to provide semantic
bridges across this design space, due to their inability to support the degree of de-
viations between models tolerated by industrial design processes. We thus leave
the development of a theoretical approach building on compositional extensions
of robust refinement to future research, and focus in this paper on a verifica-
tion methodology which adds mathematical rigor to industrial approaches to
bridge the gap between design layers. Specifically, we enhance established prac-
tices of providing full traceability for safety requirements in offering techniques
of assigning responsibility of derived safety requirements jointly guaranteeing
collision freedom to subsystems, and provide formal verification techniques tai-
lored to the particularities of model classes at each level, to formally verify such
delegated safety requirements. Regarding stability of local control, as well as
stability of design models, we provide automated formal techniques establishing
various notions of stability. The remainder of this section outlines the overall
approach, which is then refined in individual sections.
Our verification methodology addresses the cooperation layer by formalizing
design patterns for collision avoidance as a proof rule reducing collision free-
dom to locally dischargeable safety requirements on individual subsystems of
the involved trac agents. The design patterns builds on the following central
concepts (see Section 4):
- Each agents is seen enclosed in a safety envelope, which must not be entered
by other agents;
Search WWH ::
Custom Search