Abstract
A digital twin for a Cyber-Physical System includes a simulation model that predicts how a physical system should behave. We show how to quantify and characterise violation events for a given safety property for the physical system. The analysis uses the digital twin to inform a runtime monitor that checks whether the noise and violations observed fall within expected statistical distributions. The results allow engineers to determine the best system configuration through what-if analysis. We illustrate our approach with a case study of an agricultural vehicle.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
In practice, there may be many sub-components of each of the controller, plant, and environment, elements, and they may have complex interactions.
- 2.
Some terminology. Kinematics is the space of all possible configurations of a system at one time without considering the forces acting on the system. For example, invariants between state variables that follow from conservation laws. Dynamics is how configurations change as a function of time, due to the forces acting on the system.
- 3.
The term “bicycle model” is used because the equations assume that the angle of each front wheel is the same, as happens with vehicles that have only one front wheel. In practice, the angle between the two front wheels differs and the difference is proportional to the distance between them (as in Ackermann steering geometry).
- 4.
We assume that the vehicle moving at a constant speed describes a circle about its forward travelling frame of reference. In reality, steering is more complicated than this. It depends on whether the vehicle is front or rear-wheel driven; whether the front or rear-wheels steer the vehicle; what particular steering geometry is present; what the tyre characteristics are; and whether there are differential axles. A standard configuration is for the vehicle to have front-wheel steered driving wheels with Ackermann steering geometry (Zhao et al. show how to derive this geometry in a mechanical engineering setting [33]). This approximates idealised steering along a circular arc.
- 5.
More formally, it is the limit of the secant lines through \( (x_0,f(x_0))\) and nearby points (x, f(x)) as x approaches \( x_0\). For the tangent line to be well-defined, the graph of f at \( x_0\) must be continuous. The tangent line must not be vertical: a vertical line is not a function and so does not have a slope.
References
Alur, R.: Principles of Cyber-Physical Systems. The MIT Press, Cambridge (2015)
Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1–33. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_1
Box, G.E.P.: Robustness in the strategy of scientific model building. In: Launer, R.L., Wilkinson, G.N. (eds.) Robustness in Statistics, pp. 201–236. Academic Press (1979)
Box, G.E.P., Draper, N.R.: Empirical Model-Building and Response Surfaces. Wiley, Hoboken (1987)
Cassar, I., Francalanza, A., Aceto, L., Ingólfsdóttir, A.: A survey of runtime monitoring instrumentation techniques. Electron. Proc. Theor. Comput. Sci. 254, 15–28 (2017)
Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. Formal Methods Syst. Des. 51(1), 5–30 (2017). https://doi.org/10.1007/s10703-017-0286-7
Donzé, A.: On signal temporal logic. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 382–383. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40787-1_27
Falcone, Y., Krstić, S., Reger, G., Traytel, D.: A taxonomy for classifying runtime verification tools. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 241–262. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03769-7_14
Fitzgerald, J., Gamble, C., Larsen, P.G., Pierce, K., Woodcock, J.: Cyber-physical systems design: formal foundations, methods and integrated tool chains. In: 2015 IEEE/ACM 3rd FME Workshop on Formal Methods in Software Engineering (FormaliSE), pp. 40–46 (2015)
Fitzgerald, J., Larsen, P.G., Pierce, K.: Multi-modelling and co-simulation in the engineering of cyber-physical systems: towards the digital twin. In: ter Beek, M.H., Fantechi, A., Semini, L. (eds.) From Software Engineering to Formal Methods and Tools, and Back. LNCS, vol. 11865, pp. 40–55. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30985-5_4
Foldager, F.F., Larsen, P.G., Green, O.: Development of a driverless lawn mower using co-simulation. In: Cerone, A., Roveri, M. (eds.) SEFM 2017. LNCS, vol. 10729, pp. 330–344. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-74781-1_23
Forrester, A., Sobester, A., Keane, A.: Engineering Design via Surrogate Modelling: A Practical Guide. Wiley, Hoboken (2008)
Gibson, J.P., Larsen, P.G., Pantel, M., Fitzgerald, J., Woodcock, J.: Cyber-physical systems engineering: an introduction. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018, Part III. LNCS, vol. 11246, pp. 407–410. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03424-5_27
Gomes, C., Thule, C., Broman, D., Larsen, P.G., Vangheluwe, H.: Co-simulation: a survey. ACM Comput. Surv. 51(3), 49:1–49:33 (2018)
INTOCPS Association: Uncertainty quantification repository (2020). https://gitlab.au.dk/clagms/2020.isola.uncertaintyquantification. Accessed 21 Dec 2020
Jantsch, A., Sander, I.: Models of computation and languages for embedded system design. IEE Proc. Comput. Digit. Tech. 152(2), 114–129 (2005)
Keesman, K.J.: System Identification: An Introduction. Springer, London (2011). https://doi.org/10.1007/978-0-85729-522-4
Kritzinger, W., Karner, M., Traar, G., Henjes, J., Sihn, W.: Digital twin in manufacturing: a categorical literature review and classification. IFAC-PapersOnLine 51, 1016–1022 (2018)
Larsen, P.G., Fitzgerald, J., Woodcock, J., Gamble, C., Payne, R., Pierce, K.: Features of integrated model-based co-modelling and co-simulation technology. In: Cerone, A., Roveri, M. (eds.) SEFM 2017. LNCS, vol. 10729, pp. 377–390. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-74781-1_26
Legaard, C.M., Gomes, C., Larsen, P.G., Foldager, F.F.: Rapid prototyping of self-adaptive-systems using python functional mockup units. In: SummerSim 2020. ACM, New York (2020)
Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebraic Program. 78(5), 293–303 (2009)
Macedo, H., Nilsson, R., Larsen, P.: The harvest coach architecture: embedding deviation-tolerance in a harvest logistic solution. Computers 8(2), 31 (2019)
Martínez, G.S., Karhela, T., Vyatkin, V., Miettinen, T., Pang, C.: An OPC UA based architecture for testing tracking simulation methods. In: 2015 IEEE Trustcom/BigDataSE/ISPA, vol. 3, pp. 275–280 (2015)
Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyber-physical system models. Formal Methods Syst. Des. 49(1–2), 33–74 (2016). https://doi.org/10.1007/s10703-016-0241-z
Nakaya, M., Li, X.: On-line tracking simulator with a hybrid of physical and Just-In-Time models. J. Process Control 23(2), 171–178 (2013)
Rajamani, R.: Vehicle Dynamics and Control. Springer, Boston (2012). https://doi.org/10.1007/978-1-4614-1433-9
Rajhans, A., et al.: Supporting heterogeneity in cyber-physical systems architectures. IEEE Trans. Autom. Control 59(12), 3178–3193 (2014)
Rooney, J.J., Heuvel, L.N.V.: Root cause analysis for beginners. Qual. Prog. 37(7), 45–56 (2004)
Sohlberg, B., Jacobsen, E.: Grey box modelling – branches and experiences. IFAC Proc. Vol. 41(2), 11415–11420 (2008)
Tao, F., Zhang, H., Liu, A., Nee, A.Y.C.: Digital twin in industry: state-of-the-art. IEEE Trans. Ind. Inf. 15(4), 2405–2415 (2019)
Van der Auweraer, H., Anthonis, J., De Bruyne, S., Leuridan, J.: Virtual engineering at work: the challenges for designing mechatronic products. Eng. Comput. 29(3), 389–408 (2013). https://doi.org/10.1007/s00366-012-0286-6
Vangheluwe, H.: Foundations of modelling and simulation of complex systems. Electron. Commun. EASST 10 (2008)
Zhao, J.S., Liu, Z.J., Dai, J.: Design of an Ackermann type steering mechanism. J. Mech. Eng. Sci. 227, 2549–2562 (2013)
Acknowledgements
We acknowledge the European Union for funding the INTO-CPS project (Grant Agreement 644047), which developed the open tool chain and the INTO-CPS Application; the Poul Due Jensen Foundation that funded subsequent work on taking this forward towards the engineering of digital twins; and the European Union for funding the HUBCAP project (Grant Agreement 872698). We acknowledge support from the UK EPSRC for funding for the RoboCalc (EP/M025756/1) and RoboTest projects (EP/R025479/1). Finally, we acknowledge support from the Royal Society and National Natural Science Foundation of China for funding for the project Requirements Modelling for Cyber-Physical Systems IEC/NSFC/170319. Early versions of the ideas in this paper were presented to the Digital Twin Centre in Aarhus in December 2019 (twice) and to the RoboStar team in York in January 2020. We are grateful for their feedback.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Woodcock, J., Gomes, C., Macedo, H.D., Larsen, P.G. (2021). Uncertainty Quantification and Runtime Monitoring Using Environment-Aware Digital Twins. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends. ISoLA 2020. Lecture Notes in Computer Science(), vol 12479. Springer, Cham. https://doi.org/10.1007/978-3-030-83723-5_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-83723-5_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-83722-8
Online ISBN: 978-3-030-83723-5
eBook Packages: Computer ScienceComputer Science (R0)