Statistical Model Checking as an Effective Technology to Formally Analyze Industry-Relevant Cyber-Physical Systems Angela Pappagallo Computer Science Dept., Sapienza University of Rome, via Salaria 113, 00198, Italy Abstract Many autonomous Cyber-Physical Systems (e.g., devices for Internet of Things, Unmanned Autonomous Vehicles, medical devices, etc) are mission-critical (i.e., errors result in loss of money) or safety-critical (i.e., errors result in damage or even death for humans). This motivates research on efficient formal verification methods for such Cyber-Physical Systems. Unfortunately, this is not an easy task, as verifying a Cyber-Physical System entails evalu- ating a huge number of scenarios (scenario explosion). Furthermore, a unified mathematical model for the (discrete) cyber part and the (continuous) physical part is currently not available. Such obstructions may be mitigated by using Statistical Model Checking, which uses statistical methods to sample the set of scenarios while basing on possibly black-box models of the System Under Verification. In this paper, we review 5 recent real-world and industry-relevant case studies from the literature that involved usage of Statistical Model Checking. Such case studies range on very different application areas, namely: i) intelligent services for peak shaving in smart grids, ii) In-Silico Clinical Trial for medical services, iii) applications for wireless sensor networks; iv) aircraft data networks; v) plug-in electric vehicles. This shows the maturity, feasibility and flexibility of Statistical Model Checking when applied to real-world case studies. 1. Introduction A Cyber-Physical System (CPS) is a system where a (continuous) physical system (plant) is controlled and/or monitored by a (discrete) software. The deployment of autonomous CPSs [3], such as, e.g., devices for Internet of Things (IoT) [11, 88], Unmanned Au- tonomous Vehicles [35] and medical devices [20], has been speeding up for the last decades, with a projected 1.1 trillion USD global speding on IoT only [81]. For many of such CPSs, it is important to rule out errors [21, 22], especially bugs in the software part, since such bugs may lead to: • loss of money in mission-critical systems [8]. This is the case, e.g., in aerospace: as an example, in 1996 the Ariane 5 [4] rocket was destroyed after launch due to a type conversion error in the software, resulting in a 500 M$ loss; IPS-RCRA 2021: 9th Italian Workshop on Planning and Scheduling and 28th International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion © 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) • death of serious injury for people in safety-critical systems [66]. This is the case, e.g., for medical devices. As standard testing could not provide the required degree of correctness assurance, this motivates research on efficient formal verification methods [16]. There are multiple challenges to overcome when formally verifying a CPS [17], e.g., the huge number of scenarios to be evaluated (scenario explosion, e.g., [49, 53, 52, 54]), which is hard to tackle also using High-Performance Computing (HPC) [55, 56, 51, 60]. Furthermore, much research must still be done in order to find a unified mathematical model for the discrete cyber part and the continuous physical part [38, 45]. Such issues make it hard to apply analytical approaches based on logics (e.g., [14, 26, 47, 13, 48]) or automata (e.g., [19, 46, 62]). Statistical Model Checking (SMC) [41] holds the promise to overcome this obstacle by using statistical methods to sample the set of scenarios up to desired accuracy and precision [27, 28, 18], while possibly relying on black-box models of the System Under Verification (SUV) (i.e., the full system encompassing both the software and the plant) [2, 5]. In this paper, we review 5 recent real-world and industry-relevant case studies from the literature that involved usage of SMC. Such case studies range on very different application areas, namely: • verification of an intelligent service for peak shaving in smart grids; • generation of Virtual Patients (VPs) to enable In-Silico Clinical Trial (ISCT) for medical services (Virtual Physiological Human [31, 36]); • parameter estimation for an application to stream audio in wireless sensor networks; • computation of network latency under different system parameters for an aircraft network; • computation of confidence intervals for the probability of failures in the recharging process of a Plug-in Electric Vehicle (PEV). This shows the feasibility and flexibility of SMC when applied to real-world case studies. A preliminary version of this paper has been presented in [68]. Here we discuss more case studies, by also providing more details about methodologies and results. For a complete survey of SMC methodologies themselves, see, e.g., [69, 1, 74, 7]. 2. Real-World Case Studies for Statistical Model Checking This section discusses some recent real-world and industry-relevant problems that have been solved by using SMC or SMC-based methodologies. Namely, Section 2.1 shows an application in the field of intelligent services for smart grids, Section 2.2 presents an SMC-based methodology used for enabling ISCT in Virtual Physiological Human (VPH), Section 2.3 illustrates how SMC may be used in the field of wireless sensors networks, Section 2.4 discusses results on verifying network latency of an aircraft data network and finally Section 2.5 computes the probability of failures in PEV recharging. 2.1. Peak Shaving in Smart Grids An Electric Distribution Network (EDN) [71] is composed of several substations, where each substation serves a set of residential houses. By using the measurements taken from the home electricity mains (Advanced Metering Infrastructure, AMI), we know each house power demand, with periodicity at least one hour. Our objective is to reduce costs for the Distribution System Operator (DSO), by limiting the demand drawn at some or all substations of the EDN at times of peak demand (peak shaving [73]). In fact, this reduces costs of buying energy from the market at times of peak electricity price (which involves usage of peak power plants [65]), and reduces overloading of network components during times of peak demand (thus reducing substations aging), or during periods when the system is weakened due to line/transformer maintenance or other outages [83]. Many work in the literature address the problem above, see, e.g., [34, 23, 86, 32, 77]. In this paper, we focus on the methodology in [29, 58, 59, 64], for which a verification based on SMC techniques is available. Namely, in that line of research the problem of achieving peak shaving is counteracted by proposing the two following intelligent services (for an high-level schema, see Figure 1). 1. The first service (EDN Virtual Tomography, EVT) computes time-varying upper bounds for the aggregated electricity demand resulting from the residential houses 𝑈 connected to a given EDN substation 𝑠. As a result, if the aggregated demand of 𝑠 is kept below such upper bounds, the DSO will save in the maintenance costs for 𝑠, as well as in energy production costs. 2. The second service (Demand-Aware Price Policy, DAPP) computes individualised time-varying upper bounds for each residential house in 𝑈 . If a residential user keeps its demand below the bounds computed by DAPP, then a low energy tariff is applied, otherwise an high tariff is applied. Note that, in order to do this, residential users must perform load shifting, by consuming more electricity when the bound is high and less electricity when the bound is low. As a result, if all residential users succeeds in keeping their demand below the given bounds, the aggregated demand on 𝑠 will be below the bound computed by EVT. However, there is no guarantee that residential users will be able to perform load shifting so as to stay below the bounds computed by DAPP. In [57], a domain-specific statistical model checker named Aggregated Power Demand-Analyzer (APD-A) is designed, in order to compute the probability of violations of the bounds on the aggregated demand on 𝑠, given probabilistic deviations from the expected power demand (again, computed by DAPP) of each single house. More in detail, APD-A takes in input: 1. the time 𝑇 on which to perform the evaluation (usually, one month divide in time-slots of one hour); Jan EDN Feb Mar Electrical Distr. + energy price policies Apr Substation Network measurements May EDN configuration Network readings User flexibility Jun DSO Retailer Distribution ! Jul Operational price policies Constraints User flexibility Aug Network Sep state estimation Distribution price policies Oct EVT DAPP Nov Services Dec 0 100 200 300 400 500 Figure 1: Intelligent systems for smart grids [29] Figure 2: Results for Aggregated Power Demand-Analyzer from [57 2. for each user 𝑢 ∈ 𝑈 , the Expected Power Profile (EPP) 𝑝𝑢 : 𝑇 → R, i.e., a function taking as input a time-slot in 𝑡 ∈ 𝑇 and returning the power demand 𝑝𝑢 (𝑡) (in kW) of user 𝑢 in 𝑡; such demand is a further output of DAPP and is always below the power bound for 𝑢 in 𝑡 (i.e., 𝑝𝑢 (𝑡) ≤ 𝑃𝑢 (𝑡), being 𝑃𝑢 (𝑡) the upper bound output by DAPP, for all 𝑢 ∈ 𝑈, 𝑡 ∈ 𝑇 ; 3. a ∫︀ 𝑏 probabilistic model dev𝑢 for users deviations from deviations from EPPs, i.e., 𝑎 𝑑𝑒𝑣𝑢 (𝑥)𝑑𝑥 = is the probability that actual ∫︀power demand of 𝑢 in any time-slot 0.02 𝑡 ∈ 𝑇 is in [(1 + 𝑎)𝑝𝑢 (𝑡), (1 + 𝑏)𝑝𝑢 (𝑡)] (e.g., −0.02 𝑑𝑒𝑣𝑢 (𝑥)𝑑𝑥 = probability that actual power demand of 𝑢 in any time-slot 𝑡 ∈ 𝑇 deviates at most by 2% from EPP of 𝑢); 4. the substation safety requirements, i.e., 𝑝𝑠 : 𝑇 → R s.t., for each 𝑡 ∈ 𝑇 , the DSO wants the aggregated demand on 𝑠 to be below 𝑝𝑠 (𝑡); 5. parameters for the output probability distribution 0 < 𝛿, 𝜀 < 1 and 𝛾 ∈ R, i.e., the output values must be correct up to tolerance 𝜀 with statistical confidence 1 − 𝛿, and the output probability distribution is discretized with step 𝛾. As an output, APD-A returns the probability distribution for the aggregated demand on 𝑠 resulting from EPPs disturbed with the given probabilistic disturbance model dev𝑢 . To this aim, APD-A relies on a parallel version (for cluster of computers with distributed memory) of the Optimal Approximation Algorithm (OAA) from [28]. Figure 2 shows the resulting output of APD-A for a group of 186 real-world houses in Denmark. 2.2. Virtual Patients for In-Silico Clinical Trials One of the most complex problems in Medicine is assessing safety and efficacy of pharma- cological drugs, medical devices and, more in general, treatment strategies [76]. In the last years, a wide research area called ISCT has been developed [70, 6], with the aim to approach such a problem via Computer Science techniques. By prioritizing the successive in vivo experimentations, this would decrease time and cost of the overall process, reduce animal and human testing, and enable precision medicine [37, 24, 84, 85]. A key enabler to carry out an ISCT is the availability of a population of VPs, i.e., a set computational models of the physiology of interest and of the Pharmacokinet- ics/Pharmacodynamics (PK/PD) of the relevant pharmacological compounds on which to perform computer simulations. However, to guarantee compelling evidence of safety and efficacy of the therapy under assessment, such a population of VP must be representative of the entire spectrum of human phenotypes. This includes the possible individual differences in physiology and the different possible reactions to the external stimuli (e.g., drug administrations). Such computational, quantitative, personalized models of the human physiology and drugs PK/PD are typically derived in two steps. First, quantitative inter-individual VPH models are derived from qualitative knowledge from, e.g., available repositories [33, 25], and are often formalized in terms of systems of parametric differential equations (for continuous-time models) or different equations (for discrete-time models). Different assignments to such (real valued) parameters yield different time courses (aka trajectories) of the modeled biological quantities, and different reactions to the same stimuli. Thus, a quantitative VPH model combined with a parameter assignment is regarded as a Virtual Patient (VP), representing a human phenotype. Such VPs can then be simulated (typically as black-box systems via numerical simulators, given the complexity of the differential equations) to assess the values of proper metrics of the therapy of interest, e.g., expected safety and efficacy (In-Silico Clinical Trials, ISCT). Unfortunately, computing VPs is all but easy. Indeed, most of the legal assignments to a VPH model do yield model trajectories which clearly violate human physiology. This is because such models are often over-parameterised, and unknown inter-dependency constraints among the various parameters do exist. Also, parameters are often introduced to model not-well-understood biological mechanisms (see, e.g., [82, 61]), or to abstract away details that are not needed to be modeled accurately to perform the planned verification activity. Also in this case, a random assignment to such parameters would yield, with very high probability, an overall model behavior which is clearly non-admissible from a biological standpoint. The major obstacle is thus to automatically recognize whether a model parameter assignment is a (physiologically admissible) VP, and to search for such VPs in the (typically huge real-valued) space of model parameter assignments. However this is not enough. Indeed, since, in order to carry out an ISCT we need a population of VPs representative of the entire spectrum of the phenotypes entailed by the VPH model, we need to search for all VPs satisfying the physiological admissibility criterion. Furthermore, since complex VPH models are often non-identifiable, it is often the case that several parameter assignments yield VPs which have indistinguishable (with respect to some given tolerance) trajectories under all time series of external stimuli (e.g., drug administrations). The presence, in the computed population, of such indistinguishable VPs would be a major source of redundancy, hence inefficiency of the Figure 3: Results for Virtual Patients coverage from [79] verification process, and should be avoided. In [79], SMC-based techniques are used to drive global search (intelligently guided by an heuristic) in the VPs parameters space. Namely, starting from a (non-identifiable) VPH model and suitable biological and medical knowledge elicited from experts to formally define what a physiologically admissible trajectory is, such techniques compute a population of VPs which is representative of the entire spectrum of phenotypes entailed by the model and does not contain indistinguishable VPs, up to the user-requested statistical guarantees. Namely, given user-defined constants 𝜀, 𝛿 ∈ (0, 1), when the algorithm terminates, the probability that further sampling will yield a VP showing an unknown phenotype (i.e., a phenotype not already included in the population computed so far) is ≤ 𝜀 with statistical confidence ≥ 1 − 𝛿. The effectiveness of such approach has been proven on GynCycle [75], a non-identifiable model of the female Hypothalamic Pituitary Gonadal (HPG) axis, consisting of 33 highly non-linear stiff ordinary differential equations. Namely, a population of 4,830,264 VPs (each one being an assignment to 75 real-valued parameters) was generated and stratified into 7 levels (at different granularity of behaviours). The representativeness of such VPs was assessed against 86 retrospective health records from Pfizer, Hannover Medical School and University Hospital of Lausanne. Figure 3 shows that the datasets are respectively covered by such VPs within Average Normalised Mean Absolute Error (ANMAE) of 15%, 20%, and 35%. The computed population of VPs was then used in [50, 80] to compute, again in silico, optimal robust personalised treatments for assisted reproduction, an area currently showing many factors that can be hardly kept under full control [40, 30, 39]. Namely, digital twins of human patients were computed by selecting those VPs best matching clinical measurements on them, and a black-box simulator of the VPH model in [75] was driven [78] via intelligent backtracking on such digital twins. Figure 4: SBIP model of the wireless sensor network from [67] Figure 5: Results for properties 𝜑1 and 𝜑2 from [67] 2.3. Wireless Sensors Network In this section we discuss a low-level engineering application, namely an audio streaming application over a Wi-Fi network. Such an application is representative of a wide area of applications on networked systems [43, 44]. In such a network, several nodes are equipped with microphones which produce different audio streams and are transmitted to a base station equipped with a speaker to play the received audio. The goal is to ensure the synchronization between the different nodes of the network, in order to guarantee a consistent audio output. To this extent, in [42, 67] a Phase Locked Loop (PLL) synchronization master-slave protocol [15] is designed so that all nodes in the network agree on a synchronized clock, within a 1𝜇𝑠 tolerance. In order to show that the PLL synchronization protocol fulfills the main design requirement, as well as to perform a parameter tuning of the main protocl parameters, the SBIP statistical model checker [63] is used, which is based on the Behaviour, Interaction, Priority (BIP) framework [10]. A schema of the SBIP model for the PLL is shown in Figure 4. Namely, the following three properties were verified: 𝜑1 the size of the slave buffer must be below its maximum capacity (no overflow); 𝜑2 the master buffer must be not empty (no underflow); 𝜑3 it must hold that the difference between the Master clock 𝜃𝑚 and the software clock, computed in every Slave 𝜃𝑠 , must be within a given bound Δ with high probability Figure 6: An AFDX architecture from [9]. E.S. stands for “end-system”, which is a source of information and accuracy. For 𝜑1 , many verifications were run, by varying the size of the slave buffer. Analogously, for 𝜑2 the initial playout (i.e., the delay after which the master starts consuming from its buffer), was varied. The results are shown in Figure 5, as a function of the size of the buffer and of the initial delay, respectively. Of course, in both cases we are interested in the probability of 𝜑1 and 𝜑2 to be as close to 100% as possible. From the verification results it is possible to conclude that the optimal value for the slave buffer is 400 slots, while the optimal value for the inital playout is 1430 ms. Finally, as for 𝜑3 , again many verifications were run, by varying Δ as the specific time bound between the master clock and the software clock. The obtained result was that, for the considered setting, the smallest bound that ensures the synchronisation is Δ = 76𝜇𝑠. 2.4. Avionics Full-Duplex Switched Ethernet Avionics Full-Duplex Switched Ethernet (AFDX) is a network architecture used in many aircrafts, such as Airbus, Boeing, AgustaWeistland, Comac and many others. It has been patented by Airbus in order to provide data network connection inside aircrafts while maintaining deterministic quality of service. In [9], SMC is used in order to estimate AFDX performances under various assumptions (scenarios), by focusing on a given AFDX architecture (see Figure 6, though the method may be easily generalized). The main idea is to model the network by replacing the network switches with a probability distribution for the delay experienced by a packet which traverses a given switch. Then, the network latency is estimated, when varying the following network parameters: Figure 7: Results for AFDX verification (scenario 2 from [9]): left is for 10 VLs, center is for 20 VLs and right is for 30 VLs • number of Virtual Links (VLs), i.e., of logical unidirectional connections from one transmitter end-system to one or many receiver end-systems; • number of frames (i.e., packets); • size of the Bandwidth Allocation Gap (BAG), i.e., the time interval allocated for the transmission of one packet. We review one of the main results of SMC usage on such case study from [9]. Three experiments are performed with increasing number of VLs (let 𝑋 be such number), namely 10, 20, and 30 links. For all VLs we have that BAG is 4 ms while the frame size varies from 100 (for end-system number 1) to 500 bytes (for end-system number 5). Note that end-system number 6 is not considered in this scenario. For each 𝑋 ∈ {10, 20, 30}, the task is to compute the probability that the total delivery time for packets (network latency) is smaller than a given bound, until we reach probability one. The results are given in Figure 7. We note that, for end-system 1 (which only traverses one switch), the results are better, i.e., the network latency is always below 500 𝜇s (𝑋 = 10), 1000 𝜇s (𝑋 = 20) and 1500 𝜇s (𝑋 = 30). All other end-systems have the same (worse) results, as they traverse two switches. Namely, the network latency is always below 1100 𝜇s (𝑋 = 10), 2000 𝜇s (𝑋 = 20) and 3000 𝜇s (𝑋 = 30). 2.5. Recharging of a Plug-in Electric Vehicle PEVs are being increasingly used in the last decade all over the world [87]. Being able to efficiently recharge PEVs is of great importance, and has impacts on the smart grids field again. In this case study, we consider a Tesla Model S with a battery capacity of 90kWh which must be charged at a charging station. The model consider we consider here (see [12, 72]) provides several features, such as: 1. charging may be probabilistically delayed, modeling that the grid is currently congested; 0.09 lower bound 0.08 upper bound 0.07 0.06 Confidence interval 0.05 0.04 0.03 0.02 0.01 0 -0.01 2 3 4 5 Number of failures Figure 8: Results for the confidence intervals (lower and upper bounds) of the PEV case study from [12] 2. the amount of time after which the PEV is disconnected is unknown, so it is modeled as a normal probability distribution; 3. the charging processes starts from an empty battery, goes through a “good” charging state after a given time interval and end up in a “full” charging state after another time interval; 4. it is possible to charge the PEV multiple times; 5. one entire week of operation is considered, where recharging is also started in the night and the PEV has to be found fully recharged on the next morning (at an unknown time, as discussed above); 6. we want to compute the probability that the recharging process fails at least 𝑛𝑓 𝑎𝑖𝑙 ∈ {2, 3, 4, 5} times. Results for the confidence intervals of the resulting probability is shown in Figure 8, as a function of the number of failures 𝑛𝑓 𝑎𝑖𝑙 . Note that probabilities decrease very fast when increasing 𝑛𝑓 𝑎𝑖𝑙 . 3. Conclusions In this work, we have reviewed some recent real-world problems that were solved using SMC-based techniques. Such problems were taken from very different application areas: • smart grid intelligent services, in order to compute the probability of EDN sub- stations to be overloaded, when residential users may deviate from their expected power profiles; • Virtual Physiological Human, to generate a population of VPs for ISCT of drugs, medical devices and treatment strategies, s.t. such population is complete and not over-representative; • wireless sensor networks, in order to find the smallest bound for clock synchroniza- tion accuracy of an audio streaming application; • aircraft data network (AFDX, Avionics Full-Duplex Switched Ethernet), in order to estimate network latency under different system parameters such as frame size, BAG and number of VLs; • Plug-in Electric Vehicles, in order to estimate the probability of failures during the recharging process. This results show that SMC is a mature methodology which can be successfully applied to real-world meaningful problems. References [1] G. Agha and K. Palmskog. A survey of statistical model checking. ACM Trans. Model. Comput. Simul., 28(1), 2018. [2] B. K. Aichernig and M. Tappler. Probabilistic black-box reachability checking (extended version). Formal Methods Syst. Des., 54(3):416–448, 2019. [3] R. Alur. Principles of Cyber-Physical Systems. MIT, 2015. [4] ARIANE 5 Flight 501 Failure, hiips://www- users.cse.umn.edu/ arnold/disasters/ariane5rep.html, 1996. [5] P. Ashok, P. Daca, J. Křetínský, and M. Weininger. Statistical model checking: Black or white? In T. Margaria and B. Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, pages 331–349, Cham, 2020. Springer International Publishing. [6] Avicenna Project. In silico clinical trials: How computer simulation will transform the biomedical industry. hiip://avicenna-isct.org/wp-content/uploads/2016/01/ AvicennaRoadmapPDF-27-01-16.pdf, 2016. [7] M. Bakir, M. Gheorghe, S. Konur, and M. Stannett. Comparative analysis of statistical model checking tools. In CMC 2016, 2016. [8] A. Banerjee, K. K. Venkatasubramanian, T. Mukherjee, and S. K. S. Gupta. En- suring safety, security, and sustainability of mission-critical cyber–physical systems. Proceedings of the IEEE, 100(1):283–299, 2012. [9] A. Basu, S. Bensalem, M. Bozga, B. Delahaye, A. Legay, and E. Sifakis. Verification of an afdx infrastructure using simulations and probabilities. volume 6418, pages 330–344, 11 2010. [10] A. Basu, M. Bozga, and J. Sifakis. Modeling heterogeneous real-time components in bip. In Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM’06), pages 3–12, 2006. [11] B. Bordel, R. Alcarria, T. Robles, and D. Martín. Cyber–physical systems: Extending pervasive sensing from control theory to the internet of things. Pervasive and Mobile Computing, 40:156–184, 2017. [12] C. E. Budde, P. R. D’Argenio, A. Hartmanns, and S. Sedwards. A statistical model checker for nondeterminism and rare events. In D. Beyer and M. Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 340–358, Cham, 2018. Springer International Publishing. [13] M. Cadoli and T. Mancini. Combining relational algebra, SQL, constraint modelling, and local search. TPLP, 7(1-2), 2007. [14] M. Cadoli, T. Mancini, and F. Patrizi. SAT as an effective solving technology for constraint problems. In ISMIS 2006, volume 4203 of LNCS. Springer, 2006. [15] K. Choi and H. Liu. Phase-Locked Loop and Synchronization, pages 135–150. Wiley- IEEE Press, 2016. [16] E. Clarke and J. M. Wing. Formal methods: state of the art and future directions. Comp. Surv., 28(4), 1996. [17] E. Clarke and P. Zuliani. Statistical model checking for cyber-physical systems. In ATVA 2011, volume 11. Springer, 2011. [18] P. Dagum, R. Karp, M. Luby, and S. M. Ross. An optimal algorithm for Monte Carlo estimation. SICOMP, 29(5), 2000. [19] G. Della Penna, B. Intrigila, I. Melatti, E. Tronci, and M. Venturini Zilli. Bounded probabilistic model checking with the Mur𝜙 verifier. In FMCAD 2004. IEEE, 2004. [20] N. Dey, A. S. Ashour, F. Shi, S. J. Fong, and J. M. R. S. Tavares. Medical cyber-physical systems: A survey. Journal of Medical Systems, 42(74), 2018. [21] K. Ding, S. Ding, A. Morozov, T. Fabarisov, and K. Janschek. On-line error detection and mitigation for time-series data of cyber-physical systems using deep learning based methods. In 2019 15th European Dependable Computing Conference (EDCC), pages 7–14, 2019. [22] B. Dowdeswell, R. Sinha, and S. G. MacDonell. Finding faults: A scoping study of fault diagnostics for industrial cyber–physical systems. Journal of Systems and Software, 168:110638, 2020. [23] O. Erdinc, A. Tascikaraoglu, N. G. Paterakis, and J. P. S. Catalao. Novel incentive mechanism for end-users enrolled in dlc-based demand response programs within stochastic planning context. IEEE Transactions on Industrial Electronics, 66(2):1476– 1487, 2019. [24] European Medicines Agency. Reporting of physiologically based pharmacokinetic (PBPK) modelling and simulation, 2019. EMA/CHMP/458101/2016. [25] A. Fabregat, S. Jupe, L. Matthews, K. Sidiropoulos, M. Gillespie, P. Garapati, R. Haw, B. Jassal, F. Korninger, B. May, M. Milacic, C. Roca, K. Rothfels, C. Sevilla, V. Shamovsky, S. Shorser, T. Varusai, G. Viteri, J. Weiser, G. Wu, L. Stein, H. Hermjakob, and P. D′ Eustachio. The Reactome pathway knowledgebase. Nucl. Ac. Res., 46(D1), 2018. [26] G. Gottlob, G. Greco, and T. Mancini. Conditional constraint satisfaction: Logical foundations and complexity. In IJCAI 2007, 2007. [27] R. Grosu and S. Smolka. Quantitative model checking. In ISoLA 2004, 2004. [28] R. Grosu and S. Smolka. Monte Carlo model checking. In TACAS 2005, volume 3440 of LNCS. Springer, 2005. [29] B. Hayes, I. Melatti, T. Mancini, M. Prodanovic, and E. Tronci. Residential demand management using individualised demand aware price policies. IEEE Trans. Smart Grid, 8(3), 2017. [30] M. Hengartner, T. Kruger, K. Geraedts, E. Tronci, T. Mancini, F. Ille, M. Egli, S. Roeblitz, R. Ehrig, L. Saleh, K. Spanaus, C. Schippert, Y. Zhang, and B. Leeners. Negative affect is unrelated to fluctuations in hormone levels across the menstrual cycle: Evidence from a multisite observational study across two successive cycles. J. Psycho. Res., 99, 2017. [31] P. Hunter, P. Coveney, B. de Bono, V. Díaz-Zuccarini, J. Fenner, A. Frangi, P. Harris, R. Hose, P. Kohl, P. Lawford, K. Mccormack, M. Mendes, S. Omholt, A. Quarteroni, J. Skår, J. Tegner, S. R. Thomas, I. Tollis, I. Tsamardinos, and M. Viceconti. A vision and strategy for the virtual physiological human in 2010 and beyond. Philosophical transactions. Series A, Mathematical, physical, and engineering sciences, 368:2595– 614, 06 2010. [32] A. Jindal, B. S. Bhambhu, M. Singh, N. Kumar, and K. Naik. A heuristic-based appliance scheduling scheme for smart homes. IEEE Transactions on Industrial Informatics, 16(5):3242–3255, 2020. [33] M. Kanehisa, M. Furumichi, M. Tanabe, Y. Sato, and K. Morishima. Kegg: New perspectives on genomes, pathways, diseases and drugs. Nucl. Ac. Res., 45(D1), 2017. [34] C. E. Kement, H. Gultekin, and B. Tavli. A holistic analysis of privacy-aware smart grid demand response. IEEE Transactions on Industrial Electronics, 68(8):7631–7641, 2021. [35] W. Koch, R. Mancuso, R. West, and A. Bestavros. Reinforcement learning for uav attitude control. ACM Trans. Cyber-Phys. Syst., 3(2), Feb. 2019. [36] P. Kohl and D. Noble. Systems biology and the virtual physiological human. Molecular Systems Biology, 5(1):292, 2009. [37] M. R. Kosorok and E. B. Laber. Precision medicine. Annual Review of Statistics and Its Application, 6(1):263–286, 2019. [38] E. A. Lee. Fundamental limits of cyber-physical systems modeling. ACM Trans. Cyber-Phys. Syst., 1(1), Nov. 2016. [39] B. Leeners, T. Krüger, K. Geraedts, E. Tronci, T. Mancini, M. Egli, S. Röblitz, L. Saleh, K. Spanaus, C. Schippert, Y. Zhang, and F. Ille. Associations between natural physiological and supraphysiological estradiol levels and stress perception. Front. Psycol., 10, 2019. [40] B. Leeners, T. Kruger, K. Geraedts, E. Tronci, T. Mancini, F. Ille, M. Egli, S. Roe- blitz, L. Saleh, K. Spanaus, C. Schippert, Y. Zhang, and M. Hengartner. Lack of associations between female hormone levels and visuospatial working memory, divided attention and cognitive bias across two consecutive menstrual cycles. Front. Behav. Neuro., 11, 2017. [41] A. Legay, B. Delahaye, and S. Bensalem. Statistical model checking: An overview. In RV 2010, volume 6418 of LNCS. Springer, 2010. [42] A. Lekidis, P. Bourgos, S. Djoko-Djoko, M. Bozga, and S. Bensalem. Building distributed sensor network applications using bip. In Proceedings of 2015 IEEE Sensors Applications Symposium, Zadar, Croatia, 2015. [43] A. Lekidis, M. Bozga, D. Mauuary, and S. Bensalem. A model-based design flow for can-based systems. In 13th International CAN Conference, iCC13, 11 2013. [44] A. Lekidis, E. Stachtiari, P. Katsaros, M. Bozga, and C. K. Georgiadis. Using BIP to reinforce correctness of resource-constrained iot applications. In 10th IEEE International Symposium on Industrial Embedded Systems, SIES 2015, Siegen, Germany, June 8-10, 2015, pages 245–253. IEEE, 2015. [45] F. Maggioli, T. Mancini, and E. Tronci. SBML2Modelica: Integrating biochemical models within open-standard simulation ecosystems. Bioinformatics, 36(7), 2020. [46] T. Mancini and M. Cadoli. Detecting and breaking symmetries by reasoning on problem specifications. In SARA 2005, volume 3607 of LNCS. Springer, 2005. [47] T. Mancini, M. Cadoli, D. Micaletto, and F. Patrizi. Evaluating ASP and commercial solvers on the CSPLib. Constraints, 13(4), 2008. [48] T. Mancini, P. Flener, and J. Pearson. Combinatorial problem solving over relational databases: View synthesis through constraint-based local search. In SAC 2012. ACM, 2012. [49] T. Mancini, F. Mari, A. Massini, I. Melatti, F. Merli, and E. Tronci. System level formal verification via model checking driven simulation. In CAV 2013, volume 8044 of LNCS. Springer, 2013. [50] T. Mancini, F. Mari, A. Massini, I. Melatti, I. Salvo, S. Sinisi, E. Tronci, R. Ehrig, S. Röblitz, and B. Leeners. Computing personalised treatments through in silico clin- ical trials. A case study on downregulation in assisted reproduction. In RCRA 2018, volume 2271 of CEUR W.P. CEUR, 2018. [51] T. Mancini, F. Mari, A. Massini, I. Melatti, I. Salvo, and E. Tronci. On minimising the maximum expected verification time. Inf. Proc. Lett., 122, 2017. [52] T. Mancini, F. Mari, A. Massini, I. Melatti, and E. Tronci. Anytime system level verification via random exhaustive hardware in the loop simulation. In DSD 2014. IEEE, 2014. [53] T. Mancini, F. Mari, A. Massini, I. Melatti, and E. Tronci. System level formal verification via distributed multi-core hardware in the loop simulation. In PDP 2014. IEEE, 2014. [54] T. Mancini, F. Mari, A. Massini, I. Melatti, and E. Tronci. SyLVaaS: System level formal verification as a service. In PDP 2015. IEEE, 2015. [55] T. Mancini, F. Mari, A. Massini, I. Melatti, and E. Tronci. Anytime system level verification via parallel random exhaustive hardware in the loop simulation. Microprocessors and Microsystems, 41, 2016. [56] T. Mancini, F. Mari, A. Massini, I. Melatti, and E. Tronci. SyLVaaS: System level formal verification as a service. Fundam. Inform., 149(1–2), 2016. [57] T. Mancini, F. Mari, I. Melatti, I. Salvo, E. Tronci, J. Gruber, B. Hayes, and L. Elmegaard. Parallel statistical model checking for safety verification in smart grids. In SmartGridComm 2018. IEEE, 2018. [58] T. Mancini, F. Mari, I. Melatti, I. Salvo, E. Tronci, J. Gruber, B. Hayes, M. Pro- danovic, and L. Elmegaard. Demand-aware price policy synthesis and verification services for smart grids. In SmartGridComm 2014. IEEE, 2014. [59] T. Mancini, F. Mari, I. Melatti, I. Salvo, E. Tronci, J. Gruber, B. Hayes, M. Pro- danovic, and L. Elmegaard. User flexibility aware price policy synthesis for smart grids. In DSD 2015. IEEE, 2015. [60] T. Mancini, I. Melatti, and E. Tronci. Any-horizon uniform random sampling and enumeration of constrained scenarios for simulation-based formal verification. IEEE TSE, 2021. [61] T. Mancini, E. Tronci, I. Salvo, F. Mari, A. Massini, and I. Melatti. Computing biological model parameters by parallel statistical model checking. In IWBBIO 2015, volume 9044 of LNCS. Springer, 2015. [62] F. Mari, I. Melatti, I. Salvo, and E. Tronci. Model based synthesis of control software from system level formal specifications. ACM TOSEM, 23(1), 2014. [63] B. L. Mediouni, A. Nouri, M. Bozga, M. Dellabani, A. Legay, and S. Bensalem. SBIP 2.0: Statistical Model Checking Stochastic Real-time Systems. In ATVA 2018 - 16th International Symposium Automated Technology for Verification and Analysis, pages 536–542, Los Angeles, CA, United States, Oct. 2018. Springer. [64] I. Melatti, F. Mari, T. Mancini, M. Prodanovic, and E. Tronci. A two-layer near- optimal strategy for substation constraint management via home batteries. IEEE Trans. Ind. Elect., 2021. [65] J. Milewski, A. Szczęśniak, and J. Lewandowski. Dynamic characteristics of auxiliary equipment of sofc/soec hydrogen peak power plant. IERI Procedia, 9:82–87, 2014. International Conference on Environment Systems Science and Engineering (ESSE 2014). [66] R. Mitchell and I.-R. Chen. Behavior rule specification-based intrusion detection for safety critical medical cyber physical systems. IEEE Transactions on Dependable and Secure Computing, 12(1):16–30, 2015. [67] A. Nouri, B. L. Mediouni, M. Bozga, J. Combaz, S. Bensalem, and A. Legay. Performance Evaluation of Stochastic Real-Time Systems with the SBIP Framework. International Journal of Critical Computer-Based Systems, pages 1–33, 2018. [68] A. Pappagallo. Statistical model checking for the analysis of mission- and safety- critical cyber-physical systems. In 3rd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis (OVERLAY 2021), volume to appear of CEUR Workshop Proceedings. CEUR-WS.org, 2021. [69] A. Pappagallo, A. Massini, and E. Tronci. Monte carlo based statistical model checking of cyber-physical systems: A review. Information, 11(12), 2020. [70] F. Pappalardo, G. Russo, F. Tshinanu, and M. Viceconti. In silico clinical trials: concepts and early adoptions. Brief. Bioinform., 20(5), 2019. [71] D. R. Patrick and S. W. Fardo. Electrical Distribution Systems, Second Edition. Pearson Professional Education, 2009. [72] C. Pilch and A. Remke. Statistical model checking for hybrid petri nets with multiple general transitions. In 2017 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pages 475–486, 2017. [73] A. J. Pimm, T. T. Cockerill, and P. G. Taylor. The potential for peak shaving on low voltage distribution networks using electricity storage. Journal of Energy Storage, 16:231–242, 2018. [74] D. Reijsbergen, W. de Boer, P.T.and Scheinhardt, and B. Haverkort. On hypothesis testing for statistical model checking. Int. Soft. Tech. Trans., 17(4), 2015. [75] S. Röblitz, C. Stötzel, P. Deuflhard, H. Jones, D.-O. Azulay, P. van der Graaf, and S. Martin. A mathematical model of the human menstrual cycle for the administration of GnRH analogues. J. Theor. Biol., 321, 2013. [76] W. Rogers and K. Hutchison. Evidence-Based Medicine in Theory and Practice: Epis- temological and Normative Issues, pages 851–872. Springer Netherlands, Dordrecht, 2017. [77] A. Saad, T. Youssef, A. T. Elsayed, A. Amin, O. H. Abdalla, and O. Mohammed. Data-centric hierarchical distributed model predictive control for smart grid energy management. IEEE Transactions on Industrial Informatics, 15(7):4086–4098, 2019. [78] S. Sinisi, V. Alimguzhin, T. Mancini, and E. Tronci. Reconciling interoperability with efficient verification and validation within open source simulation environments. Simul. Model. Pract. Theory, 109, 2021. [79] S. Sinisi, V. Alimguzhin, T. Mancini, E. Tronci, and B. Leeners. Complete pop- ulations of virtual patients for in silico clinical trials. Bioinformatics, 36(22–23), 2020. [80] S. Sinisi, V. Alimguzhin, T. Mancini, E. Tronci, F. Mari, and B. Leeners. Optimal personalised treatment computation through in silico clinical trials on patient digital twins. Fundam. Inform., 174(3–4), 2020. [81] Statistics on IoT Spending, hiips://www.statista.com/topics/2637/internet-of- things/, 2021. [82] E. Tronci, T. Mancini, I. Salvo, S. Sinisi, F. Mari, I. Melatti, A. Massini, F. Davi’, T. Dierkes, R. Ehrig, S. Röblitz, B. Leeners, T. Krüger, M. Egli, and F. Ille. Patient- specific models from inter-patient biological models and clinical records. In FMCAD 2014. IEEE, 2014. [83] M. Uddin, M. F. Romlie, M. F. Abdullah, S. A. Halim], A. H. A. Bakar], and T. C. Kwang]. A review on peak load shaving strategies. Renewable and Sustainable Energy Reviews, 82:3323 – 3332, 2018. [84] U.S.A. Food and Drug Administration. Reporting of computational modeling studies in medical device submissions, 2016. FDA-2013-D-1530. [85] U.S.A. Food and Drug Administration. Physiologically based pharmacokinetic analyses – format and content guidance for industry, 2018. FDA-2016-D-3969. [86] N. Zhang, B. D. Leibowicz, and G. A. Hanasusanto. Optimal residential battery stor- age operations using robust data-driven dynamic programming. IEEE Transactions on Smart Grid, 11(2):1771–1780, 2020. [87] Y. Zhou, M. Wang, H. Hao, L. Johnson, and H. Wang. Plug-in electric vehicle market penetration and incentives: a global review. Mitigation and Adaptation Strategies for Global Change, 20:777–795, 06 2015. [88] M. Zimmerling, L. Mottola, P. Kumar, F. Ferrari, and L. Thiele. Adaptive real-time communication for wireless cyber-physical systems. ACM Trans. Cyber-Phys. Syst., 1(2), Feb. 2017.