Method for validating or verifying a technical system
A computer-implemented method for verifying and/or validating whether a technical system fulfills a desired criterion with a predefined probability. The technical system emits output signals based on input signals supplied to the technical system. The method includes: obtaining models for components of the technical system and connections between the models; obtaining test outputs for the models based on test inputs of the models and the connections between the models; determining an upper or lower bound of an output of the technical system; verifying and/or validating whether the technical system fulfills the criterion with the predefined probability based on the determined upper or lower bound of the output.
1 . A computer-implemented method for verifying and/or validating whether a technical system fulfills a desired criterion with a predefined probability, wherein the technical system emits output signals based on input signals supplied to the technical system, the method comprising the following steps:
obtaining models for components (S 1 , S 2 , S C ) included in the technical system, and obtaining connections between the models for the components (S 1 , S 2 , S C ), wherein each connection characterizes which model passes which output as input to another model;
obtaining a plurality of validation measurements, wherein each validation measurement includes a measurement input and a measurement output, the measurement output being obtained from a component (S 1 , S 2 , S C ) of the technical system for the measurement input when the measurement input is provided to the component (S 1 , S 2 , S C );
obtaining test outputs for the models based on test inputs of the models and the connections between the models;
determining an upper bound of an output of the technical system or a lower bound of the output by propagating upper or lower bounds (B 1 , B 2 , B C−1 , B C ) of discrepancies (D) of the models through the models, wherein each discrepancy (D) of each model characterizes a discrepancy (D) between a distribution of measurement outputs (p 1 , p 2 , p C−1 , p C ) for the component (S 1 , S 2 , S C ) corresponding to the model and a distribution of test outputs (q 1 , q 2 , q C−1 , q C ) obtained for the model of the component (S 1 , S 2 , S C ); and
verifying and/or validating whether the technical system fulfills the criterion with the predefined probability based on the determined upper bound of the output or verifying and/or validating whether the technical system fulfills the criterion with the predefined probability based on the determined lower bound of the output.
2 . The method according to claim 1 , wherein the upper bounds (B 1 , B 2 , B C−1 , B C ) of discrepancies (D) of the models are propagated through the models by iteratively determining an upper bound (B 1 , B 2 , B C−1 , B C ) of discrepancy (D) for a second model, wherein the discrepancy (D) is determined based on a discrepancy (D) for a first model and wherein the first model provides an input to the second model.
3 . The method according to claim 2 , wherein the discrepancy (D) for the second model is determined by maximizing the discrepancy (D) between a distribution of measurement outputs obtained for that component which corresponds to the second model and a distribution of test outputs obtained for the second model, wherein the discrepancy is maximized over possible distributions of measurement outputs obtained for that component.
4 . The method according to claim 3 , wherein the maximization of the discrepancy is a convex optimization problem under convex constraints.
5 . The method according to claim 4 , wherein the distribution of measurement outputs obtained for the component is a weighted empirical distribution.
6 . The method according to claim 5 , wherein the discrepancy for the second model is determined according to a first formula:
B
c
+
1
:=
max
α
D
(
S
c
+
1
[
p
α
]
,
q
c
+
1
)
subject
to
D
(
p
α
,
q
c
)
≤
B
c
α
v
≥
0
∀
v
=
1
,
…
,
V
∑
v
α
v
=
1.
7 . The method according to claim 6 , wherein each discrepancy between each respective distribution of measurements outputs and a respective distribution of test outputs are determined by a weighted sum of kernel evaluations for elements of the respective distributions.
8 . The method according to claim 7 , wherein the discrepancy for the second model is determined according to a relaxation of the first formula, wherein the relaxation characterizes a convex optimization problem.
9 . The method according to claim 1 , wherein the test inputs and test outputs are determined by synthesizing inputs of the technical system and forwarding the synthesized inputs through the models.
10 . The method according to claim 1 , wherein a model of the models is improved when the criterion cannot be verified and/or validated.
11 . The method according to claim 1 , wherein components of the technical system are improved when the criterion cannot be verified and/or validated with the predefined probability.
12 . The method according to claim 1 , wherein the technical system is configured to provide a control signal to a manufacturing machine, and/or a robot.
13 . A non-transitory machine-readable storage medium on which is stored a computer program for verifying and/or validating whether a technical system fulfills a desired criterion with a predefined probability, wherein the technical system emits output signals based on input signals supplied to the technical system, the computer program, when executed by a computer, causing the computer to perform the following steps:
obtaining models for components (S 1 , S 2 , S C ) included in the technical system, and obtaining connections between the models for the components (S 1 , S 2 , S C ), wherein each connection characterizes which model passes which output as input to another model;
obtaining a plurality of validation measurements, wherein each validation measurement includes a measurement input and a measurement output, the measurement output being obtained from a component (S 1 , S 2 , S C ) of the technical system for the measurement input when the measurement input is provided to the component (S 1 , S 2 ,S C );
obtaining test outputs for the models based on test inputs of the models and the connections between the models;
determining an upper bound of an output of the technical system or a lower bound of the output by propagating upper or lower bounds (B 1 , B 2 , B C−1 , B C ) of discrepancies (D) of the models through the models, wherein each discrepancy (D) of each model (M 1 , M 2 , M C ) characterizes a discrepancy (D) between a distribution of measurement outputs (p 1 , p 2 , p C−1 , p C ) for the component (S 1 , S 2 , S C ) corresponding to the model and a distribution of test outputs (q 1 , q 2 , q C−1 , q C ) obtained for the model (M 1 , M 2 , M C ) of the component (S 1 , S 2 , S C ); and
verifying and/or validating whether the technical system fulfills the criterion with the predefined probability based on the determined upper bound of the output or verifying and/or validating whether the technical system fulfills the criterion with the predefined probability based on the determined lower bound of the output.