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 eficient formal verification methods for such Cyber-Physical Systems. Unfortunately, this is not an easy task, as verifying a Cyber-Physical System entails evaluating 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 diferent 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 lfexibility of Statistical Model Checking when applied to real-world case studies.
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 [
As standard testing could not provide the required degree of correctness assurance,
this motivates research on eficient 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., [
Statistical Model Checking (SMC) [
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 diferent
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 [
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., [
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 ifnally Section 2.5 computes the probability of failures in PEV recharging.
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., [
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 tarif is applied, otherwise an high tarif 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 [
Operational
Constraints
User flexibility state Network estimation
EVT Services
Electrical Substation
Distr. + energy price policies Network measurements DSO
User flexibility Distribution ! price policies
Distribution price policies
Feb Mar Apr May Jun Jul Aug Sep Oct Nov Dec 0 100 200 300 400
500
DAPP, for all ∈ ,
∈ ; 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 ︀∫
of ); 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 ∈ is in [(1 + ) ( ), (1 + ) ( )] (e.g., ∫︀ 0.02 actual power demand of in any time-slot ∈ deviates at most by 2% from EPP ( ) = probability that wants the aggregated demand on to be below ( ); 4. the substation safety requirements, i.e., : → R s.t., for each ∈ , the DSO 5. parameters for the output probability distribution 0 < , < 1 and ∈ R, i.e., the and the output probability distribution is discretized with step .
output values must be correct up to tolerance with statistical confidence 1 − , 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.
One of the most complex problems in Medicine is assessing safety and eficacy of
pharmacological drugs, medical devices and, more in general, treatment strategies [76]. In the
last years, a wide research area called ISCT has been developed [
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 Pharmacokinetics/Pharmacodynamics (PK/PD) of the relevant pharmacological compounds on which to perform computer simulations.
However, to guarantee compelling evidence of safety and eficacy 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 diferences in physiology and the diferent 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 [
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 ineficiency of the 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 efectiveness 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 stif ordinary diferential 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 diferent 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 [
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 [
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 [
and accuracy.
For 1, many verifications were run, by varying the size of the slave bufer. Analogously, for 2 the initial playout (i.e., the delay after which the master starts consuming from its bufer), was varied. The results are shown in Figure 5, as a function of the size of the bufer 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 bufer 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 .
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 [
We review one of the main results of SMC usage on such case study from [
PEVs are being increasingly used in the last decade all over the world [87]. Being able to eficiently recharge PEVs is of great importance, and has impacts on the smart grids ifeld 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; 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 .
In this work, we have reviewed some recent real-world problems that were solved using SMC-based techniques. Such problems were taken from very diferent application areas: • smart grid intelligent services, in order to compute the probability of EDN substations 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 synchronization accuracy of an audio streaming application; • aircraft data network (AFDX, Avionics Full-Duplex Switched Ethernet), in order to estimate network latency under diferent 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. [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 efective 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 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 nearoptimal 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 safetycritical 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: Epistemological 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 eficient 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 populations 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-ofthings/, 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. Patientspecific 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 storage 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.