杨志斌

Personal Information

More  >>

Professor   Supervisor of Doctorate Candidates  

Profile

以下信息由研究生系统导入,请酌情修改完善

杨志斌,男,博士,南京航空航天大学计算机学院教授、博士生导师,目前担任软件科学与工程系副主任。长期从事安全关键软件开发与验证方法研究。                                                      

20122月在北京航空航天大学计算机学院获博士学位。20124月-201412月在法国图卢兹大学作博士后研究,博士后期间,获得一项法国航空航天基金(STAE)资助(2013.72014.6)。2015年3月到南航工作,主持国家自然科学面上基金、青年基金、GF基础研究重点项目、ZF重大项目子课题、GF基础、江苏省自然科学青年基金、航空科学基金等课题。在IEEE transactions on industrial informatics, IEEE Transactions on Reliability, JSS, FAC, SCP、JSA等重要国际期刊和国际会议发表论文70余篇,申请专利32项,其中授权16项。中国计算机学会形式化方法专委委员、中国计算机学会抗恶劣计算机专委委员、中国航空学会计算与仿真分会委员、航空电子3A基础架构标准委员会委员。获国防科技进步二等奖(第一完成人)、中国航空工业集团科技进步二等奖、江苏省教学成果二等奖等省部级奖3项。

担任国家自然科学面上(2022年)、青年基金(2021年)通信评审专家,多个会议PC,ACM Trans. on Embedded Computing Systems(TECS)、SCP、JSA、Frontiers of Computer Science(FCS)、Science in China、软件学报等期刊会议审稿人。

 

主讲课程:本科生《编译原理》《编译原理课程设计》

       研究生课程《安全关键软件设计》

研究方向:软件工程

机器学习、强化学习、安全关键嵌入式软件(safety-critical software)、模型驱动开发方法、安全分析、形式化方法

发表学术论文,出版专著情况:

SCI期刊论文:

1) Zhibin Yang, Linquan Xing, Zonghua Gu, Yingming Xiao, Yong Zhou, Zhiqiu Huang, Lei Xue. Model-based Reinforcement Learning and Neural Network-based Policy Compression for Autonomous Spacecraft Rendezvous Guidance. IEEE transactions on industrial informatics. 2022.

2) Jian Xie, Wenan Tan, Zhibin Yang, Shuming Li, Linquan Xing & Zhiqiu Huang. SysML-based compositional verification and safety analysis for safety-critical cyber-physical systems, Connection Science, 34:1, 911-941 (2022)

3)Zhibin Yang, Yang Bao, Yongqiang Yang,  Zhiqiu Huang, Jean-Paul Bodeveix, Mamoun Filali, Zonghua Gu. Exploiting Augmented Intelligence in the Modeling of Safety-Critical Autonomous Systems. Formal Aspects of Computing. 33(3): 343-384 (2021). 

4)Zhibin Yang, Shenghao Yuan, Jean-Paul Bodeveix, Mamoun Filali, Tiexin Wang, and Yong Zhou. Multi-task Ada code generation from synchronous dataflow programs on multi-core: Approach and industrial study. Science of Computer Programming, Volume 207, 1 July 2021, 102644.

5) Zhibin Yang, Zhikai Qiu, Yong Zhou, Zhiqiu Huang, Jean-Paul Bodeveix, Mamoun Filali. C2AADL Reverse: A Model-Driven Reverse Engineering Approach for Development and Verification of Safety-critical Software. Journal of Systems Architecture: Embedded Software Design. Volume 118, September 2021, 102202. 

6)Fei Wang, Zhibin Yang*, Zhiqiu Huang, Chengwei Liu, Yong Zhou, Jean-Paul Bodeveix, Mamoun Filali. An Approach to Generate the Traceability between Restricted Natural Language Requirements and AADL Models. IEEE Transactions on Reliability,2020.

7)Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali.MinSIGNAL: Towards a Simple and Safe Compiler for the Synchronous Language SIGNAL in Objective Caml. Front. Comput. Sci.. 2019, 13 (4): 715-734.

8) Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali,Kai Hu, Yongwang Zhao, Dianfu Ma. Towards a Verified Compiler Prototype for the Synchronous Language SIGNAL. Frontiers of Computer Science10(1):37-53(2016).
9) Yongwang Zhao, Zhibin Yang, Dianfu Ma. A survey on formal specification and verification of separation kernels.Frontiers of Computer Science. Frontiers Comput. Sci. 11(4): 585-607 (2017)
10) Zhibin Yang, Kai Hu, Dianfu Ma, Jean-Paul Bodeveix, Lei Pi, Jean-Pierre Talpin: From AADL to Timed Abstract State Machines: A verified model transformation. Journal of Systems and Software 93: 42-68 (2014).
11) Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali: A comparative study of two formal semantics of the SIGNAL language. Frontiers of Computer Science 7(5): 673-693 (2013)
12) Kai Hu, Teng Zhang, Zhibin Yang, Wei-Tek Tsai: Exploring AADL verification tool through model transformation. Journal of Systems Architecture - Embedded Systems Design 61(3-4): 141-156 (2015). 
13) Jean-Paul Bodeveix, Mamoun Filali, Manuel Garnacho, Régis Spadotti, Zhibin Yang: Towards a verified transformation from AADL to the formal component-based language FIACRE. Science of Computer Programming. 106: 30-53 (2015). 
14) Kai Hu, Teng Zhang, Zhibin Yang, Wei-Tek Tsai: Simulation of real-time systems with clock calculus. Simulation Modelling Practice and Theory 51: 69-86 (2015). 
15) Kai Hu, Teng Zhang, Zhibin Yang: Multi-threaded code generation from Signal program to OpenMP. Frontiers of Computer Science 7(5): 617-626 (2013).
16) Yinling Liu, Guohua Shen, Zhiqiu Huang, Zhibin Yang: Quantitative risk analysis of safety-critical embedded systems. Software Quality Journal 25(2): 503-527 (2017) 

中文A类及重要期刊论文:

17)宗喆, 杨志斌*, 袁胜浩, 周勇, BODELEIX Jean-Paul, FILALI Mamoun. 安全关键异构软件混合建模及代码生成方法.软件学报. 2021.4

18)鲍阳, 杨志斌*, 谢健, 周勇, 岳涛, 黄志球, 郭鹏. 基于限定中文自然语言需求的SysML模型自动生成方法. 计算机研究与发展. 2021.4

19)杨志斌,杨永强, 袁胜浩,周勇, 薛垒,程高辉. 安全关键软件术语推荐和需求分类方法. 计算机科学. 2021.5 (入选期刊封面论文)

20) 袁胜浩, 杨志斌*, 张博林, 周勇, 薛垒, BODEVEIX Jean-Paul, FILALI Mamoun.同步语言多线程代码生成的语义保持证明方法.计算机学报. 2020.43(11).
21) 张博林,杨志斌*,周勇,马燕燕,黄志球,薛垒. 一种面向安全关键软件的AADL模型组合验证方法. 计算机学报. 2020.43(11).
22) 杨志斌, 袁胜浩, 谢健, 周勇, 陈哲, 薛垒, BODEVEIX Jean-Paul,  FILALI Mamoun.一种同步语言多线程代码自动生成工具. 软件学报,2019,30(7):1980-2002
23) 王飞,杨志斌*,黄志球等. 基于限定自然语言需求模板的AADL模型生成方法. 软件学报, 2018(8):2350-2370.
24) 杨志斌, 赵永望,黄志球, 胡凯, 马殿富, Bodeveix Jean-Paul, Filali Mamoun.同步语言的时间可预测多线程代码生成方法. 软件学报2016,27(3):611-8722;632.
25) 杨志斌, 胡凯, 赵永望, 马殿富, Jean-Paul Bodeveix. 基于时间抽象状态机的AADL模型验证. 软件学报. Vol.25, No.2, 2015.
26) 杨志斌, 皮磊, 胡凯, 顾宗华, 马殿富. 复杂嵌入式实时系统体系结构设计与分析语言: AADL. 软件学报, Vol.21, No.5, May 2010, pp. 899-915.
27)胡凯, 张 腾, 尚利宏,杨志斌, Jean-Pierre Talpin. 面向同步规范的并行代码自动生成方法. 软件学报, 2016.
28)王飞,黄志球,杨志斌,阚双龙,沈国华,陈光颖. 一种安全攸关嵌入式系统需求追踪方法. 计算机学报, 2018.3.1, 41(3): 652~669

会议论文:

29) Yingmin Xiao, Zhibin Yang, et al. Run-Time Assured Reinforcement Learning for Safe Spacecraft Rendezvous with Obstacle Avoidance. SETTA 2023.

30) Shenghao Yuan, Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali, Tiexin Wang, and Yong Zhou. Automated Ada Code Generation from Synchronous Dataflow Programs on Multicore: Approach and Industrial Study. FTSCS 2019.
31) Jinmiao Xu, Zhibin Yang, Zhiqiu Huang, et al. Hierarchical Behavior Annex: Towards an AADL Functional Specification Extension. 16th ACM-IEEE International Conference on Formal Methods and Models for System Design. 2018.
32) Zhibin Yang. A Practical AADL Study in Aerospace Software: from Requirement to Implementation. Memocode 2018.
33) Zhe Chen, Chuanqi Tao, Zhiyi Zhang, Zhibin Yang: Beyond spatial and temporal memory safety. ICSE (Companion Volume) 2018: 189-190
34) Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi, Zhibin Yang: Parametric Runtime Verification of C Programs. TACAS 2016: 299-315
35) Yongwang Zhao, Zhibin Yang, David Sanán:Event-based Formalization of Safety-critical Operating System Standards: An Experience Report on ARINC 653 using Event-B. 26th IEEE International Symposium on Software Reliability Engineering (ISSRE 2015), NOVEMBER 2–5, 2015, GAITHERSBURG, MD, USA.
36) Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali. Multi-core Code Generation from Polychronous Programs with Time-Predictable Properties. Architecture Centric Virtual Integration (ACVI) Workshop of ACM/IEEE 17th International Conference on Model Driven Engineering Languages and Systems (MoDELS 2014), Valencia, Spain. 09/2014.
37) Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali, Kai Hu, Dianfu Ma. A Verified Transformation: from Polychronous Programs to a Variant of Clocked Guarded Actions. Proceedings of 17th International Workshop on Software and Compilers for Embedded Systems, SCOPES’14, Sankt Goar, Germany, 10/06/2014-11/06/2014, ACM,128-137.
38) Zhibin Yang, Kai Hu, Jean-Paul Bodeveix, Lei Pi, Dianfu Ma, Jean-Pierre Talpin. Two formal semantics of a subset of the AADL. Proceedings of 16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011, 344-349.
39) Zhibin Yang, Kai Hu, Dianfu Ma, Lei Pi. Towards a formal semantics for the AADL behavior annex. Proceedings of 2009 Design, Automation and Test in Europe Conference and Exhibition, DATE'09, 1166-1171. 
40) Zhibin Yang, Kai Hu, Dianfu Ma, Lei Pi, Jean-Paul Bodeveix. Formal Semantics and Verification of AADL Modes in Timed Abstract State Machine. IEEE International Conference on Progress in Informatics and Computing (PIC). 1098-1103. 2010.
41) Lei Pi, Zhibin Yang, J-P Bodeveix, M. Filali, Kai Hu, Dianfu Ma. A comparative study of FIACRE and TASM to define AADL real time concepts. 14th IEEE International Conference on Engineering of Complex Computer Systems. 347-352. 2009.


科研成果获奖及专利:

  1. 杨志斌,林翰鑫等. 一种基于大语言模型的安全关键软件失效模式识别方法. 2023116974845

  2. 杨志斌, 刘渠等. 一种基于神经元覆盖的目标检测对抗样本生成方法. 202311730923.8

  3. 杨志斌, 苏祥等. 一种面向目标检测神经网络的蜕变测试方法. 2023116984442

  4. 杨志斌,杨珍等. 一种面向神经网络的变异测试用例评估与优化方法. 2023117174052

  5. 杨志斌,王喜龙等. 一种基于深度学习的安全关键软件需求术语推荐方法. 202311214966.0

  6. 杨志斌,王喜龙等. 一种基于预训练语言模型的安全关键软件需求分类方法. 202311157515.8

  7. 杨志斌,肖应民等. 一种面向连续控制问题的安全强化学习方法. 202310814726.8

  8. 杨志斌, 王翰丰等. 一种基于自然语言需求的验证性质自动生成方法. 202310303728.0

  9. 杨志斌,胡乔乔等. 面向综合化航空电子系统的组合调度分析方法. 202310246390.X

  10. 杨志斌, 刘晨等. 一种面向负载均衡的多核IMA可预测性调度方法. ZL202211444693.4 已授权

  11. 杨志斌,曾清华等. 一种基于约束规划的综合化航空电子系统任务分配与调度方法. 202211444664.8(已授权)

  12. 杨志斌,凌仕翔等. 一种面向ARINC653操作系统的综合化航空电子系统安全代码自动生成方法. 202211101227.6 已授权

  13. 杨志斌,邵温欣,张泽伦,周勇,王海珍. 一种面向SCADE模型的测试用例生成方法. 202211101277.6.

  14. 杨志斌、幸林泉、肖应民、周勇、黄志球、薛垒. 一种基于强化学习的航天器自主交会对接制导策略生成方法. 202111231850.9

  15. 杨志斌、张泽伦、李晓劼、周勇、黄志球、李维.一种基于机器学习的SCADE模型组合验证环境假设自动生成方法. 202111228147.2

  16. 杨志斌、李晓劼、张泽伦、周勇、薛垒、李维. 基于自然语言需求的AADL模型组合验证性质自动生成方法. 202111226642.X

  17. 杨志斌, 李书铭等. 基于SysML的安全关键智能软件建模方法.202110480086.2

  18. 杨志斌,杨永强等.一种面向安全关键软件的术语推荐及系统. 2020102301171460.

  19. 杨志斌,邱宝等.一种面向IMA的AADL多范式建模及自动生成C代码方法. 202010909187.2 (已授权)

  20. 杨志斌,宗喆等. 一种基于规范与描述语言的AADL功能行为扩展方法. 201910475574.7 (已授权)

  21. 杨志斌,李书铭等. SysML安全性扩展及其到AADL故障模型的自动转换方法.201910471898.3 (已授权)

  22. 杨志斌,邱志凯等. 一种基于源代码的AADL模型逆向重构方法.201910475582.1 (已授权)

  23. 杨志斌,冯思喆等. AADL模型求精方法及其支持的Ada可执行代码自动生成方法. 201910158762.7. (已授权)

  24. 杨志斌,马燕燕等. 面向安全关键嵌入式系统的SysML实时性扩展及AADL模型自动转换方法.201811203099.X (已授权)

  25.  杨志斌,李文心,王铁鑫等. 一种面向航天应用的AADL模型求精及其支持的C代码自动生成方法. 201811224473.4 (已授权)

  26. 杨志斌,袁胜浩等. 一种基于图形化卫式命令演算的多任务编译方法. 201810045360.1. (已授权)

  27. 杨志斌,许金淼等. 一种图形化AADL功能行为建模方法. 201810122737.9 (已授权)

  28. 杨志斌,张博林等. 一种AADL模型组合形式化验证方法. 201811396551.9

  29.  杨志斌,刘承威等. 非形式化需求规约模板到形式化设计模型的自动转换方法. 201711297282.6 (已授权)

  30.  杨志斌,袁胜浩等. 一种同步数据流语言的形式化编译方法. 201610832046.9.(已授权)

  31. 胡凯,蒋树,杨志斌等. AADL2TASM模型转换方法. 201110369259X. (已授权)

  32. 胡凯,张腾,杨志斌等. TASM2UPPAAL模型转换方法. 201210027759X. (已授权)

承担的科研项目情况:

目前主持/参与的部分项目:

1)神经网络可靠性测试技术, 2023.1-2024.12.

2)分布式航空电子系统组合可调度分析,90万元,2021.6-2023.6,主持

3)国家自然科学基金面上项目,基于契约的安全关键异构软件AADL架构模型组合验证方法,56万,2021.1-2024.12,主持

4)**基础科研项目,2021.1-2023.12,65万(总经费260万),主持
5)航空科学基金,12万,2019.10-2021.9,主持

6) 航天基金,多处理器系统架构建模与验证技术研究,2019.1-2019.12,28万,主持

7)**重大项目子课题,150万,2018.1-2020.12,主持

8) 中央高校研究基金,NS2019057,2019.1-2021.6,10万元,主持

9)国家自然科学基金(青年),面向安全关键系统的时间可预测多核代码生成方法研究,2016.1-2018.12, 23.8万元,主持

10)**基础研究重点项目,2016.1-2018.12, 200万元(项目总经费650万元),主持

11)江苏省自然科学基金(青年),2015.7-2018.6, 20万元,主持

12) 中央高校研究基金,NP2017205,2017.1-2018.12,15万元,主持

13)航空科学基金,2015.10-2017.9,10万元,主持

14)(北京航空航天大学)软件开发环境国家重点实验室开放课题,2015.3-2017.1, 10万元,主持

15)(华东师范大学)上海市高可信计算重点实验室开放课题,2015.7-2017.6,2万元,主持


目前参与的项目:

1) 工信部民机预研-中欧航空技术合作研究:机载共性技术. 2021-2025.

2)中法国际联合实验室项目:CONVEX:Compositional Verification of Cyber-Physical Systems, 2018.6-  http://liama.ia.ac.cn/ShowNewsContent.aspx?newsid=130

3)国家重点研发计划,“基于大数据的软件智能开发方法和环境”项目(北京大学牵头)子课题“复杂软件分析与验证智能化关键技术与支撑环境”(南京大学牵头),2016.7-2019.6.


参与过的部分项目:

1)法国航空航天基金,实时可靠嵌入式网络系统(TORRENTS-TOAST) 2013.7-2014.6,3.2万欧元。

2)国家自然科学基金面上项目,面向航空关键系统的AADL转换语义及其特性保持证明研究,2011.1-2013.12,30万元,主要科研人员。

3)北京神舟航天软件技术有限公司合作项目,基于模型的安全关键软件开发工具研究,2014.12-2015.12,30万元,主要科研人员。

4)航天502所合作项目,2010.9-2011.9,30万元,主要科研人员。

5)航空基金,2012.10-2014.10,10万元,主要科研人员。

6)航空基金,2008.10-2010.10,10万元,主要科研人员。

7)航空基金,2007.10-2009.10,10万元,主要科研人员。

8)航空基金,2006.10-2008.10,10万元,主要科研人员。


教改项目和论文:

1)南京航空航天大学教师教学能力提升研究课题,面向高安全系统软件工程的科研教学相促机制研究与实践,2017.1-2018.12,主持

2)杨志斌,周勇,王立松. 面向航空航天特色新工科的编译原理教学改革探索. 软件导刊.2021.

3)杨志斌,黄志球. 面向安全关键嵌入式软件工程的编译原理课程教学探索. 工业和信息化教育. 2016.

学术交流:

邀请国内外著名专家,组织安全关键软件系列讲座:1) 2015.9,法国国家信息与自动化研究所INRIA,Thierry Gautier研究员,Polychrony: A Model and an Open-source Toolset for Safety-critical System Design2)2015.11, 中科院软件所,李广元研究员,时间Büchi自动机的模型检测3)2016.4.17-2016.4.28,法国图卢兹大学,Mamoun Filali研究员,Jean-Paul Bodeveix教授,Introduction to the functional language: OCAML,Introduction to the formal development method B,Introduction to the proof assistant Coq4)2016.4,国家千人计划专家,陈钢教授,一种基于梯形图仿真的PLC程序测试方法5)2016.6, 国家千人计划专家,刘志明教授,Design by Contract of Evolving Component-Based Architectures6)2016.12,北京航空航天大学,赵永望副教授,报告题目1:符合工业标准的操作系统内核形式规约与安全分析,报告题目2:形式化方法: Event-B理论与实践. 7) 2017.5.4,法国国家信息与自动化研究所INRIA Jean-Pierre Talpin教授,报告题目为System integration using mathematics and logic: Formal methods for CPS design。8) 2018.4.27-2018.5.10,法国图卢兹大学,Mamoun Filali研究员,Jean-Paul Bodeveix教授 9) 2020.12 安全关键智能软件形式化验证方法论坛.


欢迎对航空航天软件事业有兴趣、积极主动、努力刻苦的研究生和高年级本科生(大三、大四)!优秀学生有到国外学习交流的机会。

Educational Experience

2006.9 2012.2

  • 北京航空航天大学
  • 计算机软件与理论
  • Doctoral Degree in Engineering
  • With Certificate of Graduation for Doctorate Study

2004.9 2006.7

  • 北京航空航天大学
  • 计算机应用
  • 无学位
  • 其他

2000.9 2004.7

  • 石家庄铁道大学
  • 计算机科学与技术
  • Bachelor's Degree in Engineering
  • University graduated

Work Experience

2012.4 2014.12
  • 法国图卢兹大学
2012.3 2015.6
  • 北京航空航天大学

Social Affiliations

Research Focus

  • 形式化方法
  • 安全关键软件
  • 智能软件工程

Research Group