8.3 Verification
123
Preventing Droplet Coalescence
Finally, it is only left to enforce that droplets never coalesce. Therefore, at most one
droplet is allowed to enter an entity in each time step t, which ensures a minimum
droplet distance T = 1 (cf. for droplet distances longer than 1, this constraint needs
to be adapted), i.e.
e∈C∪M
T up +T maxP ath
t=1
⎛
⎝
f ∈pred(e)
pd f,t [pSteps(f )] ∨ hd f,t [hSteps(f )]
⎞
⎠ ≤ 1
(8.7)
Passing the resulting formulation to an SMT-solver now only yields assignments
representing valid droplet sequences and valid droplet flows, which correctly
execute the experiment φ in the discrete model. If the SMT-solver determines that
no assignment is possible satisfying all constraints, it is proven that the given
microfluidic network and the discrete model abstracting its flow does not allow
to execute the experiment φ. If instead a satisfying assignment is determined,
the assignments of the vectors inj P and inj H represent a droplet sequence in
the discrete model executing the experiment φ. This process is repeated for all
experiments φ ∈ and if there is a satisfying assignment for all experiments,
the proposed method has proven that the given microfluidic network is capable of
executing all experiments at least on the discrete model.
8.3.3 Evaluation
In order to evaluate the proposed verification method, the architectures as obtained
in the evaluation of Sect. 7.5.2 have been used. Their respective specification has
been determined by the automatic dimensioning method proposed in Chap. 4 using
the settings as specified in Table 6.1 (i.e., the same microfluidic networks have
been considered in Sect. 8.2). For these resulting microfluidic networks, first, the
discrete model has been determined using a “real time” of 1/150s for one time step.
Afterwards, the proposed method has been applied to verify whether the resulting
microfluidic networks allow to execute the given set of experiments on the discrete
model.
Recall, the maximal length of the droplet sequence T up (cf. Definition 8.2)
provides an upper bound which guarantees that, if the microfluidic network allows
to execute an experiment φ, a valid droplet sequence is within this bound. However,
this maximal length determines the number of possible droplet sequences which
have to be considered (i.e., the search space). In this evaluation, first only droplet
sequences with a maximal length of T maxP ath /2 have been used, which heavily
reduces the search space. Only if no droplet sequence can be determined with a
maximal length of T maxP ath /2, the initial upper bound T up is used.
123
Preventing Droplet Coalescence
Finally, it is only left to enforce that droplets never coalesce. Therefore, at most one
droplet is allowed to enter an entity in each time step t, which ensures a minimum
droplet distance T = 1 (cf. for droplet distances longer than 1, this constraint needs
to be adapted), i.e.
e∈C∪M
T up +T maxP ath
t=1
⎛
⎝
f ∈pred(e)
pd f,t [pSteps(f )] ∨ hd f,t [hSteps(f )]
⎞
⎠ ≤ 1
(8.7)
Passing the resulting formulation to an SMT-solver now only yields assignments
representing valid droplet sequences and valid droplet flows, which correctly
execute the experiment φ in the discrete model. If the SMT-solver determines that
no assignment is possible satisfying all constraints, it is proven that the given
microfluidic network and the discrete model abstracting its flow does not allow
to execute the experiment φ. If instead a satisfying assignment is determined,
the assignments of the vectors inj P and inj H represent a droplet sequence in
the discrete model executing the experiment φ. This process is repeated for all
experiments φ ∈ and if there is a satisfying assignment for all experiments,
the proposed method has proven that the given microfluidic network is capable of
executing all experiments at least on the discrete model.
8.3.3 Evaluation
In order to evaluate the proposed verification method, the architectures as obtained
in the evaluation of Sect. 7.5.2 have been used. Their respective specification has
been determined by the automatic dimensioning method proposed in Chap. 4 using
the settings as specified in Table 6.1 (i.e., the same microfluidic networks have
been considered in Sect. 8.2). For these resulting microfluidic networks, first, the
discrete model has been determined using a “real time” of 1/150s for one time step.
Afterwards, the proposed method has been applied to verify whether the resulting
microfluidic networks allow to execute the given set of experiments on the discrete
model.
Recall, the maximal length of the droplet sequence T up (cf. Definition 8.2)
provides an upper bound which guarantees that, if the microfluidic network allows
to execute an experiment φ, a valid droplet sequence is within this bound. However,
this maximal length determines the number of possible droplet sequences which
have to be considered (i.e., the search space). In this evaluation, first only droplet
sequences with a maximal length of T maxP ath /2 have been used, which heavily
reduces the search space. Only if no droplet sequence can be determined with a
maximal length of T maxP ath /2, the initial upper bound T up is used.