Skip to main content
SpringerLink
Log in

A Formally Verified Plasma Vertical Position Control Algorithm

  • Conference paper
  • First Online:
Book cover Formal Methods for Industrial Critical Systems (FMICS 2020)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12327))

  • 574 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 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

  1. Peeters, A.G.: The Physics of Fusion Power (2008)

    Google Scholar 

  2. 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

    Chapter  Google Scholar 

  3. 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)

    Article  Google Scholar 

  4. 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

    Google Scholar 

  5. Bulgakov, A.A.: A new theory of controlled rectifiers (1970). (in Russian)

    Google Scholar 

  6. Chen, X., Sankaranarayanan, S.: Decomposed reachability analysis for nonlinear systems. In: 2016 IEEE Real-Time Systems Symposium (RTSS), pp. 13–24 (2016)

    Google Scholar 

  7. Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12(3), 299–328 (1991)

    Article  MathSciNet  Google Scholar 

  8. De Tommasi, G.: Plasma magnetic control in tokamak devices. J. Fusion Energy 38(3), 406–436 (2019)

    Article  Google Scholar 

  9. A. Kallenbach for the ASDEX Upgrade Team and the EUROfusion MST1 Team: Overview of ASDEX upgrade results. Nucl. Fusion 57 (2017)

    Google Scholar 

  10. Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. STTT 10(3), 263–279 (2008)

    Article  Google Scholar 

  11. 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

    Chapter  Google Scholar 

  12. 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

    Chapter  Google Scholar 

  13. 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

    Chapter  Google Scholar 

  14. 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)

    Google Scholar 

  15. 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

    Chapter  Google Scholar 

  16. 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

    Chapter  Google Scholar 

  17. 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)

    Google Scholar 

  18. 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)

    Google Scholar 

  19. Hunt, N., Fulton, N., Magliacane, S., Hoang, N., Das, S., Solar-Lezama, A.: Verifiably safe exploration for end-to-end reinforcement learning. arXiv preprint arXiv:2007.01223 (2020)

  20. Hunter, J.D.: Matplotlib: a 2D graphics environment. Comput. Sci. Eng. 9(3), 90–95 (2007)

    Article  Google Scholar 

  21. Janeschitz, G., et al.: The ITER divertor concept. J. Nucl. Mater. 220–222, 73–88 (1995). Plasma-Surface Interactions in Controlled Fusion Devices

    Article  Google Scholar 

  22. Keilhacker, M.: H-mode confinement in tokamaks. Plasma Phys. Control. Fusion 29(10A), 1401–1413 (1987)

    Article  Google Scholar 

  23. 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)

    Article  Google Scholar 

  24. Kirnev, G.S., et al.: Superconducting tokamak T-15 upgrade. In FT/P7-3, Proceedings of the 21st IAEA Fusion Energy Conference (2006)

    Google Scholar 

  25. 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

    Chapter  Google Scholar 

  26. 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

    Google Scholar 

  27. 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

    Chapter  Google Scholar 

  28. 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)

    Article  Google Scholar 

  29. 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

    Article  Google Scholar 

  30. 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)

    Google Scholar 

  31. 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)

    Google Scholar 

  32. Pironti, A., Walker, M.: Fusion, tokamaks, and plasma control: an introduction and tutorial. IEEE Control Syst. Mag. 25(5), 30–43 (2005)

    Article  Google Scholar 

  33. Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reas. 41(2), 143–189 (2008)

    Article  MathSciNet  Google Scholar 

  34. Platzer, A.: The complete proof theory of hybrid systems. In: LICS, pp. 541–550. IEEE (2012)

    Google Scholar 

  35. 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

    Chapter  Google Scholar 

  36. Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-63588-0

    Book  Google Scholar 

  37. 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)

    Article  Google Scholar 

  38. 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)

    Google Scholar 

  39. Shimomura, Y., Aymar, R., Chuyanov, V., Huguet, M., Parker, R., et al.: ITER overview. Nucl. Fusion 39(9Y), 1295 (1999)

    Article  Google Scholar 

  40. 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

    Chapter  Google Scholar 

  41. Tarski, A.: A decision method for elementary algebra and geometry (1948)

    Google Scholar 

  42. Virtanen, P., et al.: SciPy 1.0: fundamental algorithms for scientific computing in Python. Nat. Methods 17, 261–272 (2020)

    Article  Google Scholar 

  43. 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

    Chapter  Google Scholar 

  44. Williams, R.L., Lawrence, D.A., et al.: Linear State-Space Control Systems. Wiley, Hoboken (2007)

    Book  Google Scholar 

Download references

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

  1. Massachusetts Institute of Technology, Cambridge, USA

    May Wu

  2. MIT-IBM Watson AI Lab, IBM Research, Cambridge, USA

    May Wu, Jessie Rosenberg & Nathan Fulton

Authors
  1. May Wu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jessie Rosenberg
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nathan Fulton
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nathan Fulton .

Editor information

Editors and Affiliations

  1. ISTI, Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. AIT Austrian Institute of Technology GmbH, Vienna, Austria

    Dejan Ničković

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics

Search

Navigation