Research Interests: 

• Model-based System Engineering : Model-based System Specification and Transformation, Formal Methods for System and Software Verification. 

• Safety Critical Systems: Model-based Safety Analysis, and Verification for Complex Critical System and Software

Projects in recent years: 

• 2023.1-2026.12: “Model-based Specification and Verification for the Requirments of Automatic Critical System Mode Logics .” Supported by Joint Funds of the National Natural Science Foundation of China. (Grant No. U2241216)(Co-PI) 

• 2016.11-2019.11: “Research on Resource Allcation and Evaluation Technology for Integrated Systems.” Supported by Ministry of Industry and Information of China Special Funding. (Major Participant) 

• 2014.1-2019.1: “Research on Key Techology of Safety Analysis for Next-Gen Integrated Systems in Large Aircraft.” Supported by National Basic Research Program of China (973 Program)(Grant No.2014CB745000) (Major Participant) 

• 2013.10-2015.10 : “Non-Functional Property Modelling and Analysis for Cyber-Physic System.” Supported by Science Foundation for Youth Science and Technology Innovation of NUAA.(Grant No.NS2014098)(PI)

Projects participated before 2015: 

• 2012.1-2014.12: “Research on Software Symbolic Model Checking based on Abstraction Technology.” Supported by National Natural Science Foundation (Grant No.61170043)(Co-PI) 

• 2011.10-2015.12:: “Research on the Key Technology of The Design And Evaluation of An Advanced Design Platform.” Supported by ”12th Five-Year” NUAA Advance Research Program (Grant No. 1015/ABA12004-01). (Co-PI) 

• 2010.4-2012.4: “A Formal Analysis and Verification Method for Cyber-Physical System Model.” Scientific Research Foundation for the Returned Overseas Chinese Scholars, National Education Ministry of China (PI) 

• 2007.9-2010.9: “Non-Functional Property Modelling and Analysis for Embedded Critical System” . National Research Foundation for Doctoral Program of Higher Education of China (Grant No. 20070287052) (PI) 

• 2006.5-2008.5: “Formal Analysis and Verification for Non-functional Properties of Embedded Software Designs Based on Interface Automata”. Supported by State Key Laboratory of Novel Software Technology (Nanjing University)(PI)

Publications: 2018-2022:

• [1] Hu Jun, Lv Jiarun, Wang Mingming, Kang Jiexiang, etc. Case Study on Formal Modeling and Analysis of Airborne Software Requirements. In: Journal of Software, 2022,33(5):1652- 1673. DOI:10.13328/j.cnki.jos.006554.

• [2] Zhan Wanli, Hu Jun, Gu Qingfan, etc. Model-based Fault Tree Automatic Generation Method. In: Journal of Computer Science. 2021,48(12):159-169. DOI:10.11896/jsjkx.200800177. 

• [3] Hu Jiancheng, Hu Jun, Wang Wenxuan, etc. Constructing Formal Specification Models from Domain Specific Natural Language Requirements. In: Journal of Chinese Computer Systems. 2021,42(8):1639-1648. DOI:10.3969/j.issn.1000-1220.2021.08.012. 

• [4] Qi Jian, Hu Jun, Qu Qingfan, etc. A Class Flattening Method for AltaRica 3 .0 Model. In: Journal of Computer Science. 2021,48(5):51-59. DOI:10.11896/jsjkx.200700184. 

• [5] Chen Shuo, Hu Jun, Tang Hongying, Shi Mengye etc. Transformation Method for AltaRica3 .0 Model to NuSMV Model. In: Journal of Computer Science. 2020,47(12):73-86. DOI:10.11896/jsjkx.190400035.

• [6] Chen Shuo, Hu Jun, Wang Lisong. Design and Implementation of Flattening Algorithm for AltaRica 3.0 Model Based on ANTLR. In: Journal of Chinese Computer Systems. 2020,41(7):1476-1487. DOI:10.3969/j.issn.1000-1220.2020.07.023.

• [7] Tang Hongying, Hu Jun, Chen Shuo, etc. A System Safety Analysis Tool for SysML and Case Study. In: Journal of Computer Science. 2020,47(5):284-294. DOI:10.11896/jsjkx.190600169.

• [8] Shi Mengye, Hu Jun. Case Study of Formal Model Based System Safety Modeling Analysis. In: Journal of Chinese Computer Systems. 2020,41(2):327-332. DOI:10.3969/j.issn.1000- 1220.2020.02.017. 

• [9] Hu Jun, Chen Shuo, Chen Defeng, etc. An ANTLR-based flattening framework for AltaRica 3.0 model. In: International Journal of Performability Engineering, 2019, 15(9 ): 2462-2475.

• [10] Zhang Weijun, Hu Jun, Li Wanqian etc. Case Study of Formal Modeling Analysis for SafetyCritical System Requirements. In: Journal of Frontiers of Computer Science and Technology. 2019,13(8):1295-1306. DOI:10.3778/j.issn.1673-9418.1806044. 

• [11] Hu Jun, Zhang Weijun, Li Wanqian etc. A requirement oriented formal modeling and verification method for safety critical systems. In: Journal of Computer Engineering and Science. 2019,41(8):1426-1433. DOI:10.3969/j.issn.1007-130X.2019.08.013. 

• [12] Wang Lisong, Chen Miaofang and Hu Jun. Formal Verification Method for Configuration of Integrated Modular Avionics System Using MARTE. In: International Journal of Aerospace Engineering, 2018, DOI: 10.1155/2018/7019838.

• [13] Zhan Yunjiao, Wei Ou, and Hu Jun. Formal Modeling and Analysis of Cockpit Display System Requirements. In: Journal of Computer Engineering and Science. 2018,28(3):20- 25,31. DOI:10.3969/j.issn.1673-629X.2018.03.005.

• [14] Zhan Yunjiao, Wei Ou, and Hu Jun. Formal Description of Requirement of Slats and Flaps Control System for DO-178C Case. In: Journal of Computer Science. 2018,45(4):196-202. DOI:10.11896/j.issn.1002-137X.2018.04.033.

Publications before 2018: 

• [1] Wu Zhipeng, Hu Jun, Chen Song. Safety Verification Methodology of Embedded System Based on AltaRica Model. In: Journal of Frontiers of Computer Science and Technology, 2017,11(1):24-36. DOI:10.3778/j.issn.1673-9418.1511003. 

• [2] Hu Jun, Wang Mingming, Chen Song. A transformation method for AltaRica3.0 to Promela and its verification. In: Journal of Computer Engineering and Science, 2017,39(4):708-716. DOI:10.3969/j.issn.1007-130X.2017.04.014. 

• [3] Hu Jun, Shi Jiaojie, Cheng Zhen. System Safety Specification Modelling and Analysis based on Four-Variable Models. In: Journal of Computer Science. 2016,43(11):193-199,229. DOI:10.11896/j.issn.1002-137X.2016.11.038.

• [4] Hu Jun, Cheng Zhen, Shi Jiaojie, Ma Jingjing. A modelling and test case generation method for UAV flight control software. In: Journal of Computational Information System. 11:23(2015), 8595-8606.

• [5] Hu Jun, Ma Jingjing, Liu Xue. Model-Driven Reconfiguration Information Verification for Safety-Critical Systems. In:Journal of Frontiers of Computer Science and Technology, 2015(4):385-402. 

• [6] Hu Jun, Cheng Zhen, Ma Jinjing, Shi Jiaojie, Chen Song. Schedulable Verification Framework for IMA System Based on Model-Transformation. In: Transactions of Nanjing University of Aeronautics and Astronautics. 2015,(3):403-411. 

• [7] Hu Jun, Ma Jinjing, Yuan Xiang, Cheng Zhen, Shijiaojie. Correctness Verification for Integrated Modular System Configuration Based on AADL Model. In: Transactions of Nanjing University of Aeronautics and Astronautics.2014,46(6):920-930 . 

• [8] XU Bing-feng, HUANG Zhi-qiu, HU Jun, WEI Ou, LI Weiwei. Time Property Analysis Method for State/Event Fault Tree”,In: Journal of Software.. In: Journal of Software. 2015,26(2):427-446. 

• [9] HUANG Chuan-lin,HUANG Zhi-qiu,HU Jun,XU Bing-feng,QU Chang-liang. Research on Safety Verification of Extended SysML Activity Diagram for Embedded System Design.. In: Journal of Chinese Computer Systems, 2015, 36(3): 408-417. 

• [10] QU Chang-liang,HU Jun,XU Bing-feng,HUANG Zhi-qiu. A Approach for Critical Software Safety Verification Based on Operation Expression Model. In: Journal of Chinese Computer Systems, 2014, 35(7): 1578-1584.

• [11] HUANG Zhi-qiu, XU Bing-feng, KAN ShuangLong, HU Jun, CHEN Zhe. Survey on Embedded Software Safety Analysis Standards, Methods and Tools for Airborne System. In: Journal of Software. 2014,25(2):200-218.

• [12] XU Bing-feng, HUANG Zhi-qiu, HU Jun, WEI Ou, XIAO Fang-xiong. A Method for Quantitative Analysis of State/Event Fault Tree. In: Chinese Journal of Electronic. 2013, 41(8): 1480-1486. 

• [13] Xu Bingfeng, Huang Zhiqiu, Hu Jun, Wei Ou, Zhou Yu. Minimal Cut Sequence Generation for State Event Fault Trees. In: Middleware doctoral symposium 2013, 2013:1-6.

• [14] ZHANG Jian, HU Jun, GUO Li-juan. Research on Monitoring-oriented Runtime Verification Method Based on Multi-core Architecture.. In: Journal of Chinese Computer Systems, 2012, 33(1): 102-109.

• [15] Xu Bingfeng, Huang Zhiqiu, Hu Jun. Model-driven Safety Dependence Verification for Component-based Airborne Software Supporting Airworthiness Certification. In:Acta Aeronautica ET Astronautica Sinica. 2012?No.5, Vol.33 .796-808.

• [16] Wu Liming, HU Jun, Xu Bingfeng. Research on Modeling and Test Case Generation for UAV Flight Control Software System. In: Journal of Computer Science. 2012? No.7, Vol.39, pp. 112-118.

• [17] Guo Lijuan, HU Jun, Zhang Jian. Improved Design and Implementation of T-CBESD Based on On-the-Fly Verification Methods. In: Journal of Computer Science. 2011, No.8,Vol.10, pp.145-151.

• [18] Fangxiong Xiao, Zhiqiu Huang, Zining Cao, Jun Hu, Min Yuan. Unified Modelling Functional and Non-Functional Aspect of Web Services Composition Using PTCCS . In: Int. Journal of Web Services Res. (JWSR) 8(4):47-80, 2011.

• [19] XU Bing-feng, HU Jun, CAO Dong, HUANG Zhi-qiu, GUO Li-juan, ZHANG Jian. TCBESD: a Formal Verification Tool for Component-based Embedded Software Designs. . In: Journal of Chinese Computer Systems, 2010, 31(11): 2129-2137.

• [20] Hu Jun, Huang Zhiqiu, Cao Dong, Xu Bingfeng. Formal Analysis and Verification of Resource Adaptability for Internetware. In: Journal of Software . Vol.19, No.5, pp1182-1196. May 2008.

• [21] Jun Hu, Xuandong Li, Guoliang Zheng, Chenghua Wang. Modelling and Analysis of Power Consumption for Component-Based Embedded Software.In: Proceedings of the 2006 IFIP International Conference on Embedded And Ubiquitous Computing (EUC’2006-Workshops), Lecture Notes in Computer Science 4097, pp 795-804, Springer, Aug.2006, Korean.

• [22] Hu Jun, Zhang Yan, Yu Xiaofeng, Zhang Tian, Wang Linzhang, Li Xuandong and Zheng Guoliang. Scenario-based Verification for Component-based Embedded Software Designs.In: Proceedings of the 2005 International Conference on Parallel Processing Workshops(ICPPEC-05), IEEE Computer Society. June 2005, pp.240-247, Norway.

• [23] Hu Jun, Yu Xiaofeng, Zhang Yan, Li Xuandong and Zheng Guoliang. Checking Componentbased Embedded Software Designs for Scenario-based Timing Specification. In: Proceedings of the 2005 IFIP International Conference on Embedded And Ubiquitous Computing (EUC’2005), Lecture Notes in Computer Science 3824,pp 395-404, Springer, Dec.2005 , Japan.

• [24] Hu Jun, Zhang Yan, Yu Xiaofeng, Wang Linzhang, Li Xuandong and Zheng Guoliang. Checking Component-based Designs for Senario-based Specifications. In: Chinese Journal of Computers . Vol.29, No.4. 2006, pp.2-14.

• [25] Hu Jun, Yu Xiaofeng, Zhang Yan, Li Xuandong and Zheng Guoliang. Consistency Verification of Real-time Component-based Designs for Scenario-based Specifications.In: Journal of Software . Vol.17, No.1, January 2006, pp.0048-0058.

• [26] Hu Jun, Zhang Yan, Yu Xiaofeng, Wang Linzhang£¬ Li Xuandong and Zheng Guoliang. The Research and Development on Modeling, Implementation, and Verification for Embedded Software. In: Journal of Computer Science . In: Vol.32, No. 12, 2005, pp 16-23.

• [27] Xuandong Li, Bu Lei, Jun Hu, Jianhua Zhao, Tao Zhang and Guoliang Zheng. ScenarioBased Timing Consistency Checking for Time Petri Nets. In: Proceedings of 26th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE 2006), Lecture Notes in Computer Science 4229,pp 388-403, Springer, 2006 , France.

• [28] Yan Zhang, Jun Hu, Xiaofeng Yu, Tian Zhang, Xuandong Li, Guoliang Zheng. Deriving Available Behavior All Out from Incompatible Component Compositions. In: Proceedings of the 2nd International Workshop on Formal Aspects of Component Software (FACS 2005). Electronic Notes in Theoretical Computer Science, Vol.160. Elsevier, 2006, pp.349- 361, Macau.

• [29] Yan Zhang, Jun Hu, Xiaofeng Yu, Tian Zhang, Xuandong Li, Guoliang Zheng. Scenariobased Component Behavior Derivation. In: Proceedings of the 8th International Conference on Formal Engineering Methods (ICFEM 2006). Lecture Notes in Computer Science 4260. Springer, 2006, pp.206-225, Macau.

• [30] Xiaofeng Yu, Yan Zhang, Tian Zhang, Linzhang Wang, Jun Hu, Jianhua Zhao, Xuandong Li. A model-driven development framework for enterprise Web services. In: Information Systems Frontiers 9(4): 391-409 (2007).

• [31] Li Xuandong, Hu Jun, Bo Lei, Zhao Jianhua, and Zheng Guoliang. Consistency Checking of Concurrent Models for Scenario-Based Specifications. In: Proceedings of the 12th International SDL Forum (SDL2005), Lecture Notes in Computer Science 3530, Springer, 2005, pp.298-312, Norway.

• [32] Zhang Yan, Hu Jun, Yu Xiaofeng, Li Xuandong, Zheng Guoliang. Interface Automata-A Formal System for Components Composition. In: Journal of Computer Science , In: Vol.31, No. 11, 2005, pp212-217.

• [33] Wang Linzhang, Yuan Jiesong, Yu Xiaofeng, Hu Jun, Li Xuandong and Zheng Guoliang. Generating Cases from UML Activity Diagram based on Gray-Box Method. In: Proceedings of Asia-Pacific Software Engineering Conference 2004. IEEE Computer Society. Nov.2004 pp284-291. 

• [34] Hu Jun, Xu Xiaohao. Research on Flight Wake Turbulence of ATC. In: Journal of Civil Aviation University of China . Aug. 2002. Volume 20, No. 4.

• [35] Hu Jun, Xu Xiaohao. Research on Probabilistic Models for the Flight Sepearation. In: Proceedings of the Fourth National Communications and Transportation Conference . Oct, 2001. Nanjing, P.R.China.