A Digital Twin Setup for Safety-aware Optimization of a Cyber-physical
System
Jalil Boudjadar
1
and Martin Tomko
2
1
ECE Department, Aarhus University, Aarhus, Denmark
2
Systematic, Aarhus, Denmark
Keywords:
Digital Twins, Model-based Engineering, Safety, Optimization, Formal Verification, Uppaal.
Abstract:
Digital twin technology offers a sophisticated and flexible methodology to design high fidelity models of
cyber-physical systems for simulation, optimization, formal verification and validation purposes. This has
made such a technology a nascent process being currently adopted in many industries. This paper introduces
a digital twin setup for safety-aware performance optimization of a cyber-physical system (Energy Buck con-
verter EBC). This is achieved by designing a high fidelity digital twin model of the Buck converter through
synchronization of the model with the physical system, namely calibration. The behavior model is originally
built in MATLAB to identify potential runtime optimization patterns using a genetic algorithm. Such a model
is translated to a Uppaal model to perform formal verification of the safety properties. The behavior patterns
from optimization are provided as inputs to the verification engine for approval, where only valid and feasible
patterns are pushed into the actual control loop of EBC. The proposed setup has led to maintain the system
safety while optimizing the performance and reducing the output errors.
1 INTRODUCTION
Due to the increasing energy demand and the underly-
ing need to reduce CO2 emissions, different interna-
tional authorities have dictated many regulations and
policies about high energy efficiency for different ap-
plication domains (Asdrubali and Desideri, 2019; Yu
et al., 2011; Labandeira et al., 2020; Eyring et al.,
2005). To comply with such requirements, the man-
ufacturers of electrical equipments seek sophisticated
and optimal control strategies to operate such equip-
ment with high performance following the deploy-
ment environments (Teng et al., 2021; Wei et al.,
2019; Rodrigues et al., 2018; Frangopoulos, 2018;
Letafat et al., 2020).
To investigate the operation performance and op-
timize the equipment control, flexible methodologies
that enable low cost design of high fidelity models
and high confidence analysis of the functional and
non-functional properties have been studied in the lit-
erature (Teng et al., 2021; Suslov, K. et al., 2019;
Wu et al., 2020; Garc
´
ıa-Gusano et al., 2017; Domke,
2012; Boudjadar et al., 2014a). However, two chal-
lenges have emerged: 1) it is not trivial to design high
fidelity digital models of complex systems (Austin
et al., 2020); 2) designing a model to analyze dif-
ferent nature properties (safety, performance, respon-
siveness) can be misleading due to merging different
modeling profiles is overly conservative (Rodrigues
et al., 2018; Boudjadar et al., 2015).
A digital twin (DT) is a model replica of a physical
system, known also as physical twin (PT), (Fitzgerald
et al., 2019). To ensure high fidelity of a digital twin
model to its physical twin, a calibration process can
be conducted (Wang et al., 2020a). In fact calibration
amounts at synchronizing inputs, outputs and actions
triggering of DT to that of PT and converge the DT
output values to that of PT. Thus, potential behavior
exploration, optimization, testing and verification can
be conducted on DT rather than PT.
To perform sophisticated verification with high
guarantee, one needs to either describe the DT mod-
els in a formal specification language or use a domain
specific modeling language that can be translated to
a formal specification for verification purposes. The
former option is not well suitable for industry as it
is expensive and not engineer-friendly. The later op-
tion is much feasible given the cheap modeling cost
however the challenging aspect is that performance
related features are usually abstracted through trans-
lation to prevent state space explosion of the formal
verification process (Clarke et al., 2012).
Boudjadar, J. and Tomko, M.
A Digital Twin Setup for Safety-aware Optimization of a Cyber-physical System.
DOI: 10.5220/0011272100003271
In Proceedings of the 19th International Conference on Informatics in Control, Automation and Robotics (ICINCO 2022), pages 161-168
ISBN: 978-989-758-585-2; ISSN: 2184-2809
Copyright
c
2022 by SCITEPRESS – Science and Technology Publications, Lda. All rights reserved
161
Figure 1: Proposed methodology.
The safety and energy efficiency of CPS for elec-
tric applications have been thoroughly explored in the
state of the art (Bizon, 2018; Odeim et al., 2015; Ba-
naei et al., 2021; Banaei et al., 2020; Rafiei et al.,
2021) such as road vehicles (Andari et al., 2018),
buses (Peng et al., 2017) and trams (Zhang et al.,
2017), however only few attempts consider both met-
rics together when designing controllers for safety-
critical applications (Banerjee et al., 2012). Mak-
ing safety as the driving property in the design of
safety-critical systems may lead to expensive opera-
tion cost and inefficient utilization of the energy re-
sources (Wang et al., 2020b).
This paper introduces a methodology for safe
and energy-efficient control optimization of the EBC
cyber-physical system. The methodology combines
model-based design and data-driven engineering. Our
controller focuses on finding a compromise between
safety, performance and response time (frequency) to
operate the switch of EBC so that the energy effi-
ciency is improved as high as the safety and response
time permit. Runtime control decisions are calculated
with respect to the actual system state such as compo-
nents temperature (safety), output voltage deviation
(error) and EBC frequency (constraint). Matlab mod-
els are used for calibration and optimization purposes,
whereas a translation to Uppaal is carried out to per-
form formal validation of the optimization sequences
using model checking.
The overall proposed methodology is depicted in
Figure 1. The rest of the paper is organized as fol-
lows: Section 2 presents the EBC system architecture
and early model of the EBC operation and tempera-
ture dynamics. Section 3 describes the calibration of
early model to a high fidelity model and the optimiza-
tion process. Section 4 presents our formal specifi-
cation and verification using Uppaal. Section 5 cites
relevant related work. Finally, Section 6 concludes
the paper.
2 EBC SYSTEM MODELING
This section presents the Matlab models of EBC, de-
fault controller to operate EBC and the calibration
process. The energy Buck converter we consider is
a high voltage DC-DC converter operating with a ca-
pacity of 200W and a maximum frequency of 50KHz.
EBC is a step-down converter that decreases the volt-
age of its input, from a supply for example, to its out-
put. EBC can experience output error where the ac-
tual output voltage deviates from the expected output
voltage. A constraint about EBC fault tolerance is that
the output voltage value deviates at most with 2 volts
from the requested output voltage.
The higher the positive deviation is the larger en-
ergy waste will be. Meanwhile, the larger negative
deviation is, the higher the risk will be to damage ex-
ternal load connected to EBC.
2.1 Modeling of Buck Converter
The model of EBC is made in Matlab/Simulink due
to the availability of the instantiable PowerLib library
1
to model the different hardware and electronic com-
ponents, however the behavior logic is mathemati-
cally modeled and integrated into Matlab. EBC model
1
https://se.mathworks.com/products/
simscape-electrical.html
ICINCO 2022 - 19th International Conference on Informatics in Control, Automation and Robotics
162
Figure 2: Buck converter hardware.
consists of different components where the Mosfet
switch is the master piece (Beck, 2020a). EBC out-
put interface has two ports: expected reference volt-
age V
re f
(24v in our case) and actual output voltage
V
out
(it is 22.14 in Figure 2).
In fact, the switch is the gate to pass on the current
(On state) or not (Off state). The switch operation is
controlled by a pulse signal decided by a PID con-
troller (Haq and G, 2016), i.e. when to pass on cur-
rent from the source to the output through the other
components of EBC. In simple words, the default PID
controller measures the actual error, as the difference
between expected and actual output voltages, and de-
cides to open/close the switch to rectify such an error.
In order to operate safe, the temperature of the
integrated circuits of EBC must not exceed 150
◦
C
(Beck, 2020a). The temperature depends mainly on
the switch operation (frequency to transit between
states On and Off) and the internal resistance leading
to power loss. The power loss ∆
P
(t) of EBC can be
calculated at any time point t as follows:
∆
P
(t) = (1 − η) ∗ P
in
(1)
Where η is a heat efficiency factor related to the EBC
size and material, and P
in
is the input power. One
can see that P
in
is not time dependent as it is al-
ways constant. Since P
in
is effective only when the
switch state alternates to On, reducing the switching
frequency will reduce the power loss in the converter
(Beck, 2020a). However, this may lead to lower the
output voltage. Thus, a tuning of the switch frequency
needs to be made with respect to both power loss and
output voltage deviation. The thermal performance R
of EBC at a given time point t is calculated according
to equation (2).
R(t) =
T (t) − T
A
(t)
(1 − η) ∗ P
in
(2)
Where T (t) is the EBC temperature at time point t
and T
A
(t) is the ambient temperature at time point t.
Accordingly, the internal temperature of EBC can be
calculated as follows:
T (t) = T
A
(t) + R(t) ∗ ∆
P
(t) (3)
In fact one can reduce actual temperature by reducing
the power loss which is dependent on the the switch
frequency through manipulation of P
in
. In a similar
way, the output voltage V
out
of EBC can be calculated
as follows:
V
out
(t) = V
in
∗ D(t) (4)
Where V
in
is the constant input voltage (110v) and
D(t) is the converter duty cycle factor related to ∆
P
(t).
Thus, output error is calculated by:
Error(t) = V
re f
−V
out
(t) (5)
According to the output voltage of our early stage
model, for an expected output value V
re f
= 24v the ac-
tual output voltage varies from 19.5 to 37 if we ignore
the model initialization phase.
It is clear that the maximum error (Error(t)=24-
37) of our model is too high and not acceptable.
Moreover, the temperature calculated by our DT
model is far from the actual EBC temperature. Thus,
in Section 2.2 we calibrate the behavior of our DT
model to that of the PT device.
2.2 EBC Model Calibration
The calibration goal is to establish an accurate syn-
chronization between the physical system (PT) and
the early DT model. This leads to creating a high fi-
delity DT model of EDC through updating some of
the state calculation functions of the early DT model
so that the internal states of PT and the final DT model
match. Through synchronization analysis of PT and
DT, achieved using Matlab simulations displayed as
signals on an oscilloscope, we noticed the following:
A Digital Twin Setup for Safety-aware Optimization of a Cyber-physical System
163
• DT actions are not synchronized with the actions
of PT. Thus, we calibrated the actions durations
in DT following how long the executions of such
actions take in PT. This enables us to time our DT
model and maintain synchronization between DT
and PT behaviors.
• The temperature calculated by DT converges to
that in PT only if the EBC is idling or just started
the operation. After being in operation for longer
than 37s, DT temperature is considerably lower
than that in PT. This is in fact due to the temper-
ature calculation (Eq. (3)) does not consider the
most recent temperature of EBC and only refers
to the ambient temperature. Thus, we have up-
dated the calculation of temperature dynamics of
the digital twin model as follows, by which DT
and PT temperatures align in most of the cases:
T (t) = T (t − δ) + T
A
(t) + R(t) ∗ ∆
P
(t) (6)
and δ=36s.
Thanks to synchronization of DT actions through cal-
ibration, the error calculation (Eq. (5)) has drastically
decreased and converged to the actual error in PT.
However, although the error is immensely reduced, it
is still higher than the tolerance threshold which is 2v.
Given that the calibrated DT model exposes a high fi-
delity to PT, in the next section we will conduct an
optimization of the controller using the calibrated DT
model in order to improve the EBC performance and
reduce error. The control patterns resulting from DT
optimization will first be approved against safety, fre-
quency and error tolerance requirements using Uppaal
verification engine.
3 OPTIMIZATION OF EBC
OPERATION
Given that power loss of EBC during operation is pro-
portional to its temperature (Beck, 2020b), the op-
timization goal then is to make EBC working with
the lowest possible temperature while satisfying the
requirements for maximum error tolerance and fre-
quency (response time).
Optimizing the performance of a cyber-physical
system can lead to degrading other safety and re-
liability metrics (Teng et al., 2021; Boudjadar and
Khooban, 2021) given that the system parameters can
be conflicting. As an example, the optimization pro-
cess can speed up the switch operation to minimize
the output voltage error which can result in heating up
the device beyond safety threshold. Thus, a tradeoff
between the different performance and safety parame-
ters must be carefully established and maintained dur-
ing runtime.
The optimization task has been achieved using a
genetic algorithm where the objective function is the
minimization of the output voltage error. The overall
requirements for the EDC operation are: a) Maximum
error of output voltage cannot go above 2; b) EBC
control switch has to be operable at maximum 50kHz;
c) EBC temperature must not exceed 150
◦
C.
The optimization process workflow is depicted in
Figure 3. Following the optimization process outputs
(parameters P, I and D), for the configurations satis-
fying PID feasibility requirements, the PID controller
calculates the system actuations through which error,
temperature and response time are assessed accord-
ingly. The error result is then compared to the current
best (minimal) where a new iteration of the optimiza-
tion algorithm can be triggered if the newly obtained
error does not outperform the actual minimum. To
prevent running the optimization algorithm endlessly
in case the the iterations do not converge to a better
output value, we bound the number of iterations to
20. In fact, we have empirically identified that 20 it-
erations will always lead to the system optimum no
matter of the input configuration.
Algorithm 1: Optimization algorithm.
1: function DEF RUNSIMULATION(X, DRAW-
PLOT=FALSE)(:)
2: P = X[0]
3: I = X[1]
4: D = X[2]
5: eng.set param simlP’, ’value’,Str(P), nar-
gout=0)
6: eng.set param simiI’, Value’,Str(I), nar-
gout=0)
7: eng.set param( simlD’, value’,str(D), nar-
gout=0);
8: eng.sim ’Simulationssim1.slx’)
9: result = eng.workspace[’errors’]
10: vOut = eng.workspace[’vout’]
11: avg = 0.0
12: for res in result do:
13: avg = avg + abs(np. float32(res))
14: avgError = avgresult.size[0]
15: end for
16: if drawPlot then:
17: print(”Smulation:”) Plot(out)
print(”Parameters: ”,P,I,D)
18: print(”AvgError:”,avgError)
19: return avgError
20: end if
21: end function
ICINCO 2022 - 19th International Conference on Informatics in Control, Automation and Robotics
164
Figure 3: Optimization diagram.
A sketch of the optimization algorithm is depicted
in Algorithm 1 where the parameters of the genetic
algorithm are as follows:
population size = 20
iterations = 20
mutation probability = 0.1
elite ratio = 0.01
crossover probability = 0.5
Figure 4 illustrates the outputs of the optimization
algorithm for 20 iterations. One can see that the first
iteration reduces the error to be below 2v which is
the maximum tolerance value. This is very practical
for the solution to be implemented in real-time so that
one iteration of the optimization process is sufficient
to tune the control parameters of EDC.
Figure 4: Output error following the optimization iterations.
Our mission now is to secure that the system con-
figurations obtained through optimization will not vi-
olate, immediately or potentially leading to a future
state, EBC safety and operation requirements. To
such an end, in the next section, we will translate the
high fidelity model of EDC from Matlab to Uppaal
in order to perform formal verification of the safety
and operation requirements following the input pa-
rameters calculated by the optimization function so
that only the optimization configurations satisfying
the requirements will be candidates to integration in
the controller of the physical twin.
4 FORMAL VERIFICATION AND
VALIDATION
This section describes the verification model and pro-
cess.
Verification Model. We have built a verification
model, using Uppaal timed automata (Boudjadar
et al., 2014b), to implement the theory introduced in
Section 2. Globally, the verification model of the EBC
system is formed by a set of processes, each of which
specifies the behavior of one EBC component, syn-
chronizing through different events and shared vari-
ables. Besides, a process simulating the optimization
function is integrated into the set of behavior pro-
cesses to map the optimization outputs to the input
parameters of Uppaal model.
Namely, a process P
i
is a timed automaton given
by hV
i
, L
i
, l
0
i
, I
i
, →
i
i, over a set of global variables V
and channels C shared with other processes, where:
• V,V
i
are set of global and local variables, includ-
ing discrete and continuous variables (clocks).
• L
i
is the set of locations whereas l
0
i
is the initial
location.
• I
i
: L
i
7→ pred(V ∪V
i
) is the invariant relation.
• →
i
⊆ L
i
× pred(V ∪V
i
)×(C!∪C? ∪ {τ})×U ×L
i
is the transition relation.
A Digital Twin Setup for Safety-aware Optimization of a Cyber-physical System
165
pred() is a predicate defining the syntax of guards
and comparison constructs over clocks and variables
in Uppaal (Bodeveix et al., 2011). τ is an internal
(silent) event and U : V ∪V
i
7→ R is the update to lo-
cal and global variables.
Transitions between the different locations of each
process can be driven by either events such as Req,
On, Off or time durations. Semantically, a process
state is given by the actual location of the correspond-
ing Uppaal template and a valuation of the different
variables.
Given that Uppaal transitions are instantaneous
and the stays happen only at locations, we calculate
the state update upon leaving a location by calling a
function with the duration spent at that location as a
parameter. Since Uppaal clocks are continuous, to be
able to pass the time on as a parameter we designed
a time discretizer automaton. This is in fact imple-
mented via a clock variable which is reset almost at
each transition. In iterative way, the clock value clk
is compared to an integer to find the interval [t, t + 1]
such that clk > t and clk < t +1.
At the corresponding transitions, the EBC control
process calculates the different safety attributes (error,
temperature, duration between two switch events) ac-
cording to the equations presented in Section 2 and
following the stay durations at the relevant locations.
The switch control process schedules the ON op-
erations following the actual energy convert status and
the output error. We define an energy supply request
R = he, di to be the energy supply rate e and the time
duration d for which the supply holds (Boudjadar and
Khooban, 2021).
Requirements Specification. In order to perform
formal verification and validation of EBC safety fol-
lowing the optimization process, we formalized the
aforementioned requirements (temperature, max er-
ror, frequency) as safety properties using CTL logic
as follows:
S
1
.
= ∀[] Temp ≤ Max Temp;
S
2
.
= ∀[] Freq ≤ Max Freq
S
3
.
= ∀[] Error ≤ Max Error;
Each safety property S
i
is examined individually as
a query to the Uppaal symbolic model checker. So
that for each input configuration from the optimiza-
tion, we run 3 verification processes in an automated
way as described below.
Verification and Validation. The verification of S
1
,
S
2
and S
3
for each optimization output is done us-
ing a script to trigger Uppaal verification on the same
models with optimization configurations as parame-
ters. The verification outcomes of the EBC case study
show an alignment between the number of optimiza-
tion iterations and the number of configurations satis-
fying the safety requirements. In fact, the higher the
iterations number is the higher number the optimiza-
tion configurations satisfying safety requirements will
be. The reason could be that the optimization con-
verges towards values that prevent the frequency mo-
mentum to escalate rapidly to which the temperature
increase is proportional.
Cost and Scalability Challenges. Running the ver-
ification process for each of the parameter configura-
tions obtained by the optimization process is a tedious
operation that is expensive and time consuming. This
leads the verification process to be behind the opti-
mization operation most of the time, thus optimiza-
tion results cannot be adopted upon arrival which is
not profitable from a performance engineering point
of view. A future work would be to optimize the ver-
ification process by identifying the boundaries of fea-
sible parameter values so that only candidates having
a high likelihood to be safe will be subject to verifica-
tion. This can be achieved using a machine learning
(ML) process to calculate the boundaries dynamically
together with a feedback loop from the verification
process to ML.
5 RELATED WORK
Ensuring high performance and safety properties of
cyber-physical systems (CPS) is a challenging task
given the spatio-temporal dynamics of the under-
lying physical environment (Banerjee et al., 2012).
Safety validation and energy performance optimiza-
tion of cyber-physical systems, using digital twins,
have been studied in the literature for different appli-
cations (Wang et al., 2021; Bizon, 2018; Bizon, 2017;
Herr et al., 2017; Herr et al., 2014; Boudjadar and
Khooban, 2021). However, only few attempts focused
on coupling the optimization with formal verification
to secure high performance while maintaining the un-
derlying safety requirements (van Biert et al., 2016).
The authors of (Wang et al., 2021) proposed a dig-
ital twin setup for network energy optimization and
safety analysis of Unmanned Aerial vehicles (UAV).
They used a energy-based weighted clustering algo-
rithm (EWCA) to optimize the life of the overall
communication network and enhance its availability
by minimizing the energy consumption. However,
the safety analysis is conducted in a statistical way
(probability-based) making room for misleading de-
cisions given that no absolute guarantee can be deliv-
ered about when an optimization is safe.
ICINCO 2022 - 19th International Conference on Informatics in Control, Automation and Robotics
166
The authors of (Bizon, 2017; Bizon, 2018) intro-
duced a controller for electric hybrid vehicle power
systems. The control algorithm is coupled with an
optimization process to find the efficient injection rate
so that minimizing the gap and energy waste between
the supply and the load demand. However, making
the performance as the only driving optimization fac-
tor may jeopardize the system safety.
The authors of (Herr et al., 2017; Herr et al., 2014)
propose an optimization process for multi-stack en-
ergy supply system to improve the reliability and life-
time of individual electric units. A unit is chosen
to supply the energy load if the cost related to its
activity is the cheapest possible, this will contribute
most likely to escalate the temperature of the cheap
resource units and thus violates safety.
The authors of (He et al., 2019) present a digital
twin setup to integrate process monitoring, diagnosis
and enable automated calibration of system models.
An optimization approach has been proposed to en-
hance the control stability and safety under apparatus
faults.
Our paper differs from the aforementioned refer-
ences by using Matlab as a domain-specific setup to
model EBC, calculate and optimize the performance
metrics while using Uppaal as a powerful verifica-
tion engine to deliver absolute guarantee about the
safety properties following the optimization. How-
ever, our approach might be much expensive and less
automated compared to the work in (He et al., 2019).
6 CONCLUSION
This paper presented a digital twin setup for model-
based optimization, verification and validation of a
cyber-physical system (EBC).
An early stage digital twin model has been de-
signed in Matlab. Besides, a data-driven engineering
approach has been used to calibrate the early stage
model where the outputs of the physical system (ac-
tions, values, time points) are used to synchronize and
tune the digital twin model. Optimization and safety
verification have been conducted on the resulting high
fidelity model. The optimization consists in identify-
ing candidate control configurations that lead to a bet-
ter performance and smaller output errors. To main-
tain safety requirements, we have translated the Mat-
lab model to Uppaal timed automata for formal veri-
fication. We coupled the optimization with the verifi-
cation so that only safe optimal configurations will be
integrated into the physical system control loop.
ACKNOWLEDGMENT
We acknowledge the Poul Due Jensen Foundation that
funded our basic research for engineering of digital
twins.
REFERENCES
Andari, W., Ghozzi, S., Allagui, H., and Mami, A. (2018).
Optimization of hydrogen consumption for fuel cell
hybrid vehicle. Indian Journal of Science and Tech-
nology, 11(2).
Asdrubali, F. and Desideri, U. (2019). Policies, recommen-
dations and standards. In Handbook of Energy Effi-
ciency in Buildings, pages 5–73.
Austin, M., Delgoshaei, P., Coelho, M., and Heidarine-
jad, M. (2020). Architecting smart city digital twins:
Combined semantic model and machine learning ap-
proach. Journal of Management in Engineering,
36(4).
Banaei, M., Boudjadar, J., and Khooban, M.-H. (2021).
Stochastic model predictive energy management in
hybrid emission-free modern maritime vessels. IEEE
Transactions on Industrial Informatics, 17(8):5430–
5440.
Banaei, M., Ghanami, F., Rafiei, M., Boudjadar, J., and
Khooban, M.-H. (2020). Energy management of hy-
brid diesel/battery ships in multidisciplinary emission
policy areas. Energies, 13(16).
Banerjee, A., Venkatasubramanian, K. K., Mukherjee, T.,
and Gupta, S. K. S. (2012). Ensuring safety, security,
and sustainability of mission-critical cyber–physical
systems. Proceedings of the IEEE, 100(1):283–299.
Beck, M. (2020a). Thermal design concerns for buck con-
verters in high-power automotive applications. Analog
Design Journal, 2:1–6.
Beck, M. (2020b). Thermal design concerns for buck con-
verters in high-power automotive applications. Analog
Design Journal, 2:1–6.
Bizon, N. (2017). Energy optimization of fuel cell system
by using global extremum seeking algorithm. Applied
Energy, 206:458 – 474.
Bizon, N. (2018). Real-time optimization strategy for fuel
cell hybrid power sources with load-following control
of the fuel or air flow. Energy Conversion and Man-
agement, 157:13 – 27.
Bodeveix, J.-P., Boudjadar, A., and Filali, M. (2011). An
alternative definition for timed automata composition.
In Proceedings of ATVA, pages 105–119.
Boudjadar, A., David, A., Kim, J. H., Larsen, K.,
Miku
ˇ
cionis, M., Nyman, U., and Skou, A. (2015).
Widening the schedulability of hierarchical schedul-
ing systems. In Formal Aspects of Component Soft-
ware, pages 209–227.
Boudjadar, J., David, A., Kim, J., Larsen, K., Nyman, U.,
and Skou, A. (2014a). Schedulability and energy effi-
ciency for multi-core hierarchical scheduling systems.
In ERTS2 Conf.
A Digital Twin Setup for Safety-aware Optimization of a Cyber-physical System
167
Boudjadar, J., Jin, H. K., Larsen, K., and Nyman, U.
(2014b). Compositional schedulability analysis of an
avionics system using uppaal. In International Con-
ference on Advanced Aspects of Software Engineer-
ing, pages 111–132.
Boudjadar, J. and Khooban, M. H. (2021). A safety-driven
cost optimization for the real-time operation of a hy-
brid energy system. In Proceedings of the 27th Intl.
Conf. ICSEng 2020.
Clarke, E. M., Klieber, W., Nov
´
a
ˇ
cek, M., and Zuliani,
P. (2012). Model Checking and the State Explosion
Problem. Springer Berlin Heidelberg.
Domke, J. (2012). Generic methods for optimization-based
modeling. In Proceedings of the Intl. Conf. on Ar-
tificial Intelligence and Statistics, volume 22, pages
318–326.
Eyring, V., K
¨
ohler, H. W., Lauer, A., and Lemper,
B. (2005). Emissions from international shipping:
2. impact of future technologies on scenarios un-
til 2050. Journal of Geophysical Research: Atmo-
spheres, 110(D17).
Fitzgerald, J. S., Larsen, P. G., and Pierce, K. G. (2019).
Multi-modelling and co-simulation in the engineering
of cyber-physical systems: Towards the digital twin.
In From Software Engineering to Formal Methods and
Tools, and Back, LNCS Springer, pages 40–55.
Frangopoulos, C. A. (2018). Recent developments and
trends in optimization of energy systems. Energy,
164:1011–1020.
Garc
´
ıa-Gusano, D., Garra
´
ın, D., and Dufour, J. (2017).
Prospective life cycle assessment of the spanish elec-
tricity production. Renewable and Sustainable Energy
Reviews, 75:21–34.
Haq, A. U. and G, S. R. (2016). Low power vlsi archi-
tectures for digital pid controller applications. In-
ternational Journal of Advanced Research in Electri-
cal, Electronics and Instrumentation Engineering, 5-
3:903–910.
He, R., Chen, G., Dong, C., Sun, S., and Shen, X. (2019).
Data-driven digital twin technology for optimized
control in process systems. ISA Transactions, 95:221–
234.
Herr, N., Nicod, J., and Varnier, C. (2014). Prognostics-
based scheduling in a distributed platform: Model,
complexity and resolution. In CASE’14, pages 1054–
1059.
Herr, N., Nicod, J.-M., Varnier, C., Jardin, L., Sorrentino,
A., Hissel, D., and P
´
era, M.-C. (2017). Decision pro-
cess to manage useful life of multi-stacks fuel cell
systems under service constraint. Renewable Energy,
105:590 – 600.
Labandeira, X., Labeaga, J. M., Linares, P., and L
´
opez-
Otero, X. (2020). The impacts of energy efficiency
policies: Meta-analysis. Energy Policy, 147:111790.
Letafat, A., Rafiei, M., Ardeshiri, M., Sheikh, M., Banaei,
M., Boudjadar, J., and Khooban, M. H. (2020). An
efficient and cost-effective power scheduling in zero-
emission ferry ships. Complex., 2020:6487873:1–
6487873:12.
Odeim, F., Roes, J., and Heinzel, A. (2015). Power
management optimization of an experimental fuel
cell/battery/supercapacitor hybrid system. Energies,
8(7):6302–6327.
Peng, J., He, H., and Xiong, R. (2017). Rule based energy
management strategy for a series–parallel plug-in hy-
brid electric bus optimized by dynamic programming.
Applied Energy, 185:1633 – 1643. Clean, Efficient
and Affordable Energy for a Sustainable Future.
Rafiei, M., Boudjadar, J., and Khooban, M.-H. (2021). En-
ergy management of a zero-emission ferry boat with a
fuel-cell-based hybrid energy system: Feasibility as-
sessment. IEEE Transactions on Industrial Electron-
ics, 68(2):1739–1748.
Rodrigues, G. S., Esp
´
ındola Ferreira, J. C., and Rocha, C. R.
(2018). A novel method for analysis and optimization
of electric energy consumption in manufacturing pro-
cesses. Procedia Manufacturing, 17:1073–1081.
Suslov, K., Piskunova, V., Gerasimov, D., Ukolova, E.,
Akhmetshin, A., Lombardi, P., and Komarnicki, P.
(2019). Development of the methodological basis of
the simulation modelling of the multi-energy systems.
In Proceedings of E3S Web Conf., volume 124.
Teng, S. Y., Tou
ˇ
s, M., Leong, W. D., How, B. S., Lam,
H. L., and M
´
a
ˇ
sa, V. (2021). Recent advances on in-
dustrial data-driven energy savings: Digital twins and
infrastructures. Renewable and Sustainable Energy
Reviews, 135:110208.
van Biert, L., Godjevac, M., Visser, K., and Aravind, P.
(2016). A review of fuel cell systems for maritime
applications. Journal of Power Sources, 327:345 –
364.
Wang, R., Zhou, X., Dong, L., Wen, Y., Tan, R., Chen, L.,
Wang, G., and Zeng, F. (2020a). Kalibre: Knowledge-
based neural surrogate model calibration for data cen-
ter digital twins. In Proceedings of BuildSys 20.
Wang, W., Li, X., Xie, L., Lv, H., and Lv, Z. (2021). Un-
manned aircraft system airspace structure and safety
measures based on spatial digital twins. IEEE Trans-
actions on Intelligent Transportation Systems, pages
1–10.
Wang, Y., Huang, C., and Zhu, Q. (2020b). Energy-efficient
control adaptation with safety guarantees for learning-
enabled cyber-physical systems. In Intl. Conf. on
Computer-Aided Design.
Wei, C., Xu, X., Zhang, Y., Li, X., and Bai, X. (2019). A
survey on optimal control and operation of integrated
energy systems. Complex., 2019.
Wu, B., Widanage, W. D., Yang, S., and Liu, X. (2020).
Battery digital twins: Perspectives on the fusion of
models, data and artificial intelligence for smart bat-
tery management systems. Energy and AI, 1:100016.
Yu, J., Zhang, T., and Qian, J. (2011). Energy-efficiency
standards of electrical motor products. In Electrical
Motor Products, pages 51–172.
Zhang, W., Li, J., Xu, L., and Ouyang, M. (2017). Op-
timization for a fuel cell/battery/capacity tram with
equivalent consumption minimization strategy. En-
ergy Conversion and Management, 134:59 – 69.
ICINCO 2022 - 19th International Conference on Informatics in Control, Automation and Robotics
168
