Abstract
Tokamak fusion reactors generate energy by using a magnetic control system to confine hot plasma in a toroidal chamber. In large reactors, incorrect implementation of plasma stabilization algorithms can result in significant physical damage to the reactor. This paper explains how a combination of formal verification and numerical simulation can be used to analyze the safety of a vertical stabilization algorithm of a tokamak fusion reactor.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
There are also conditions on the occurrences of these variables in \(\varphi \); however, in our case, those conditions are irrelevant because \(\varphi \) is simply a formula of first-order logic over real arithmetic and there are therefore no conditions. Platzer’s uniform substitution calculus provides a full discussion of the static semantics of [35].
References
Peeters, A.G.: The Physics of Fusion Power (2008)
Althoff, M., Krogh, B.H., Stursberg, O.: Analyzing Reachability of Linear Dynamic Systems with Parametric Uncertainties. In: Rauh, A., Auer, E. (eds.) Modeling, Design, and Simulation of Systems with Uncertainties. Mathematical Engineering, vol. 3, pp. 69–94. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-15956-5_4
Ambrosino, G., Albanese, R.: Magnetic control of plasma current, position, and shape in tokamaks: a survey or modeling and control approaches. IEEE Control Syst. Mag. 25(5), 76–92 (2005)
Bajaj, V., Elmaaroufi, K., Fulton, N., Platzer, A.: Verifiably safe scuba diving using commodity sensors: work-in-progress. In Proceedings of the International Conference on Embedded Software Companion, EMSOFT 2019, New York, NY, USA (2019). Association for Computing Machinery
Bulgakov, A.A.: A new theory of controlled rectifiers (1970). (in Russian)
Chen, X., Sankaranarayanan, S.: Decomposed reachability analysis for nonlinear systems. In: 2016 IEEE Real-Time Systems Symposium (RTSS), pp. 13–24 (2016)
Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12(3), 299–328 (1991)
De Tommasi, G.: Plasma magnetic control in tokamak devices. J. Fusion Energy 38(3), 406–436 (2019)
A. Kallenbach for the ASDEX Upgrade Team and the EUROfusion MST1 Team: Overview of ASDEX upgrade results. Nucl. Fusion 57 (2017)
Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. STTT 10(3), 263–279 (2008)
Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_30
Fulton, N., Mitsch, S., Bohrer, B., Platzer, A.: Bellerophon: tactical theorem proving for hybrid systems. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 207–224. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66107-0_14
Fulton, N., Mitsch, S., Quesel, J.-D., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527–538. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_36
Fulton, N., Platzer, A.: Safe reinforcement learning via formal methods: toward safe control through proof and learning. In: McIlraith, S., Weinberger, K. (eds.) Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence (AAAI 2018), pp. 6485–6492. AAAI Press (2018)
Fulton, N., Platzer, A.: Verifiably safe off-model reinforcement learning. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019, Part I. LNCS, vol. 11427, pp. 413–430. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_28
Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208–214. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_14
Garcia, L., Mitsch, S., Platzer, A.: HyPLC: hybrid programmable logic controller program translation for verification. In: Bushnell, L., Pajic, M. (eds.) ICCPS, pp. 47–56 (2019)
Ghorbal, K., Jeannin, J.-B., Zawadzki, E., Platzer, A., Gordon, G.J., Capell, P.: Hybrid theorem proving of aerospace systems: applications and challenges. J. Aerospace Inf. Sys. 11(10), 702–713 (2014)
Hunt, N., Fulton, N., Magliacane, S., Hoang, N., Das, S., Solar-Lezama, A.: Verifiably safe exploration for end-to-end reinforcement learning. ar**v preprint ar**v:2007.01223 (2020)
Hunter, J.D.: Matplotlib: a 2D graphics environment. Comput. Sci. Eng. 9(3), 90–95 (2007)
Janeschitz, G., et al.: The ITER divertor concept. J. Nucl. Mater. 220–222, 73–88 (1995). Plasma-Surface Interactions in Controlled Fusion Devices
Keilhacker, M.: H-mode confinement in tokamaks. Plasma Phys. Control. Fusion 29(10A), 1401–1413 (1987)
Khayrutdinov, R.R., Lukash, V.E.: Studies of plasma equilibrium and transport in a tokamak fusion device with the inverse-variable technique. J. Comput. Phys. 109(2), 193–201 (1993)
Kirnev, G.S., et al.: Superconducting tokamak T-15 upgrade. In FT/P7-3, Proceedings of the 21st IAEA Fusion Energy Conference (2006)
Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: \({\delta }\)-reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200–205. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_15
Lahtinen, J.: Model checking large nuclear power plant safety system designs: dissertation. Ph.D. thesis, Aalto University, Finland, 2016. BA1606 SDA: SHP: SASUNE Nuclear Project code: 108550 165 p. + app. 75
Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: hybrid, distributed, and now formally verified. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 42–56. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21437-0_6
Mitrishkin, Y.V., Pavlova, E.A., Kuznetsov, E.A., Gaydamaka, K.I.: Continuous, saturation, and discontinuous tokamak plasma vertical position control systems. Fusion Eng. Des. 108, 35–47 (2016)
Müller, A., Mitsch, S., Retschitzegger, W., Schwinger, W., Platzer, A.: Tactical contract composition for hybrid system component verification. STTT 20(6), 615–643 (2018). Special issue for selected papers from FASE’17
Németh, E., Bartha, T., Fazekas, Cs., Hangos, K.M.: Verification of a primary-to-secondary leaking safety procedure in a nuclear power plant using coloured Petri nets. Reliab. Eng. Syst. Saf. 94(5), 942–953 (2009)
Pakonen, A. , Mätäsniemi, T., Lahtinen, J., Karhela, T.: A toolset for model checking of plc software. In: 2013 IEEE 18th Conference on Emerging Technologies Factory Automation (ETFA), pp. 1–6 (2013)
Pironti, A., Walker, M.: Fusion, tokamaks, and plasma control: an introduction and tutorial. IEEE Control Syst. Mag. 25(5), 30–43 (2005)
Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reas. 41(2), 143–189 (2008)
Platzer, A.: The complete proof theory of hybrid systems. In: LICS, pp. 541–550. IEEE (2012)
Platzer, A.: A uniform substitution calculus for differential dynamic logic. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 467–481. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_32
Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-63588-0
Rea, C., et al.: Disruption prediction investigations using machine learning tools on DIII-D and Alcator C-Mod. Plasma Phys. Control. Fusion 60(8), 084004 (2018)
Cristina, R., Granetz, R.S.: Exploratory machine learning studies for disruption prediction using large databases on DIII-D. Fusion Sci. Technol. 74(1–2), 89–100 (2018)
Shimomura, Y., Aymar, R., Chuyanov, V., Huguet, M., Parker, R., et al.: ITER overview. Nucl. Fusion 39(9Y), 1295 (1999)
Sogokon, A., Mitsch, S., Tan, Y.K., Cordwell, K., Platzer, A.: Pegasus: a framework for sound continuous invariant generation. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 138–157. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_10
Tarski, A.: A decision method for elementary algebra and geometry (1948)
Virtanen, P., et al.: SciPy 1.0: fundamental algorithms for scientific computing in Python. Nat. Methods 17, 261–272 (2020)
Wassyng, A., Lawford, M.: Lessons learned from a successful implementation of formal methods in an industrial project. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 133–153. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45236-2_9
Williams, R.L., Lawrence, D.A., et al.: Linear State-Space Control Systems. Wiley, Hoboken (2007)
Acknowledgments
We thank Cristina Rea, Darren Garnier, and other members of the MIT Plasma Science and Fusion Center for their helpful conversations. We also thank the anonymous reviewers for their helpful feedback.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Wu, M., Rosenberg, J., Fulton, N. (2020). A Formally Verified Plasma Vertical Position Control Algorithm. In: ter Beek, M.H., Ničković, D. (eds) Formal Methods for Industrial Critical Systems. FMICS 2020. Lecture Notes in Computer Science(), vol 12327. Springer, Cham. https://doi.org/10.1007/978-3-030-58298-2_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-58298-2_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-58297-5
Online ISBN: 978-3-030-58298-2
eBook Packages: Computer ScienceComputer Science (R0)