[2] Wang X Z, Dai F Z[M]. Integrated circuit and lithographictool(2020).

[3] Bakshi V[M]. EUV lithography(2018).

[4] Qian X S, Xu G Z, Wang S Y. The technologyof organization management: systems engineering[J]. Journal of University of Shanghai for Science and Technology, 33, 520-525(2011).

[5] Schlager K J. Systems engineering-key to modern development[J]. IRE Transactions on Engineering Management, EM-3, 64-66(1956).

[6] Hao Y, Fan J H[M]. Systems engineering methods and applications(2007).

[7] Zhang Y F. Apolloprogram management: lessons for China’s large-scale S & T programs[J]. World Sci-Tech R&D, 34, 1046-1050(2012).

[8] Goode H H, Machol R E[M]. Systems engineering(1957).

[10] Hall A D. Three-dimensional morphology of systems engineering[M]. Rapp F. Contributions to a philosophy of technology, 5, 174-186(1974).

[11] Fisher J. Systems engineering for commercial space programs[J]. INCOSE International Symposium, 2, 225-230(1992).

[12] Balaji S, Murugaiyan M. Waterfall vsv-model vs agile: a comparative study on SDLC[J]. International Journal of Information Technology and Business Management, 2, 26-29(2012).

[13] Forsberg K, Mooz H, Cotterman H[M]. Visualizing project management(2005).

[14] Boehm B W. A spiral model of software development and enhancement[J]. Computer, 21, 61-72(1988).

[15] INCOSE. Systems engineering vision[R/OL]. http://www.ccose.org/media/upload/SEVision2020_20071003_v2_03.pdf

[16] Zhao X M. System design based on model system[J]. Science & Technology Review, 37, 44-48(2019).

[17] Guo Y, Zang R, Zhou L S et al. Application of model-based systems engineering to aero engine control design[J]. Science & Technology Review, 37, 96-101(2019).

[18] Lu J Z, Wang G X, Zheng X H et al. Model-based systems engineering application investigation in China[J]. Science & Technology Review, 36, 57-66(2018).

[19] Schiffelers R R H, Alberts W, Voeten J P M. Model-based specification, analysis and synthesis of servo controllers for lithoscanners[C], 55-60(2012).

[20] Tretmans J[M]. Tangram: model-based integrationand testing of complex high-tech systems(2007).

[21] Behrmann G, David A, Larsen K G. A tutorial on UPPAAL[M]. Bernardo M, Corradini F. Formal methods for the design of real-time systems, 3185, 200-236(2004).

[23] Cervin A, Henriksson D, Lincoln B et al. How does control timing affect performance? Analysis and simulation of timing using Jitterbug and TrueTime[J]. IEEE Control Systems Magazine, 23, 16-30(2003).

[24] Fowler M[M]. Domain specific languages(2010).

[25] O’Regan G[M]. Concise guide to formalmethods: theory, fundamentals and industryapplications(2017).

[26] The Coq Development Team (Project TypiCal). The Coq proof assistant reference manual[EB/OL]. https://coq.inria.fr/distrib/current/refman/

[27] Leonardo M, Soonho K, Jeremy A et al. The lean theorem prover (system description)[C], 378-388(2015).

[28] Lamport L. Specifying concurrent systems with TLA+[M]. Broy M, Steinbrüggen R. NATO science series, 183-247(2000).

[29] Holzmann G J[M]. The SPIN model checker: primer and reference manual(2004).

[30] Cimatti A, Clarke E, Giunchiglia F et al. NUSMV: a new symbolic model checker[J]. International Journal on Software Tools for Technology Transfer, 2, 410-425(2000).

[31] Levine J[M]. Flex & bison: text processing tools(2009).

[32] Levine J[M]. Lex &YACC(1992).

[33] Parr T J, Quong R W. ANTLR: apredicated-LL(k) parser generator[J]. Software: Practice and Experience, 25, 789-810(1995).

[34] Tao F, Liu W R, Liu J H et al. Digital twin and its potential application exploration[J]. Computer Integrated Manufacturing Systems, 24, 1-18(2018).

[35] Baheti R, Gill H. Cyber-physical systems[J]. The Impact of Control Technology, 12, 161-166(2011).