个人简历

杨志斌，男，博士，南京航空航天大学计算机学院副教授。长期从事安全关键嵌入式软件及形式化方法研究。
2012年2月在北京航空航天大学计算机学院获博士学位。读博期间，作为主要科研人员，先后参加了国家自然科学基金面上项目、航空科学基金、国家863重大项目子课题、军口863、航天合作项目等课题。2012年4月－2014年12月在法国图卢兹大学作博士后研究，博士后期间，获得一项法国航空航天基金（STAE）资助（2013.7－2014.6）。2015年3月到南航工作，目前主持国家自然科学面上基金、青年基金、GF科技基础研究重点项目、装发共性技术预研、GF基础科研、江苏省自然科学青年基金、航空科学基金等课题。在IEEE Transactions on Reliability, JSS, FAC, SCP、JSA等重要国际期刊和国际会议发表论文50余篇，申请专利19项，其中授权13项。AADL国际标准委员会委员、中国计算机学会抗恶劣计算机专委委员、中国计算机学会形式化方法专委委员。获国防科技成果鉴定2项（分别为第一完成人和主要完成人），江苏省教学成果二等奖1项（参与）。
主讲课程：
本科生《编译原理》《编译原理课程设计》,
研究生课程《安全关键软件设计》
科研成果获奖及专利：
杨志斌、幸林泉、肖应民、周勇、黄志球、薛垒. 一种基于强化学习的航天器自主交会对接制导策略生成方法. 202111231850.9
杨志斌、张泽伦、李晓劼、周勇、黄志球、李维.一种基于机器学习的SCADE模型组合验证环境假设自动生成方法. 202111228147.2
杨志斌、李晓劼、张泽伦、周勇、薛垒、李维. 基于自然语言需求的AADL模型组合验证性质自动生成方法. 202111226642.X
杨志斌, 李书铭等. 基于SysML的安全关键智能软件建模方法.202110480086.2
杨志斌，杨永强等.一种面向安全关键软件的术语推荐及系统. 2020102301171460.
杨志斌，邱宝等.一种面向IMA的AADL多范式建模及自动生成C代码方法. 202010909187.2 （已授权）
杨志斌,宗喆等. 一种基于规范与描述语言的AADL功能行为扩展方法. 201910475574.7 （已授权）
杨志斌,李书铭等. SysML安全性扩展及其到AADL故障模型的自动转换方法.201910471898.3 （已授权）
杨志斌,邱志凯等. 一种基于源代码的AADL模型逆向重构方法.201910475582.1 （已授权）
杨志斌，冯思喆等. AADL模型求精方法及其支持的Ada可执行代码自动生成方法. 201910158762.7. （已授权）
杨志斌，马燕燕等. 面向安全关键嵌入式系统的SysML实时性扩展及AADL模型自动转换方法.201811203099.X （已授权）
杨志斌，李文心，王铁鑫等. 一种面向航天应用的AADL模型求精及其支持的C代码自动生成方法. 201811224473.4 （已授权）
杨志斌,袁胜浩等. 一种基于图形化卫式命令演算的多任务编译方法. 201810045360.1. （已授权）
杨志斌，许金淼等. 一种图形化AADL功能行为建模方法. 201810122737.9 （已授权）
杨志斌，张博林等. 一种AADL模型组合形式化验证方法. 201811396551.9
杨志斌，刘承威等. 非形式化需求规约模板到形式化设计模型的自动转换方法. 201711297282.6 （已授权）
杨志斌,袁胜浩等. 一种同步数据流语言的形式化编译方法. 201610832046.9.（已授权）
胡凯，蒋树，杨志斌等. AADL2TASM模型转换方法. 201110369259X. （已授权）
胡凯，张腾，杨志斌等. TASM2UPPAAL模型转换方法. 201210027759X. （已授权）
承担的科研项目情况：
目前主持的部分项目：
1）安全关键系统一体化安全分析方法及工具，主持
2)分布式航空电子系统组合可调度分析，90万元，2021.6-2023.6，主持
3)国家自然科学基金面上项目，基于契约的安全关键异构软件AADL架构模型组合验证方法，56万，2021.1-2024.12，主持
4)GF基础科研项目，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)GF基础研究重点项目，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 安全关键智能软件形式化验证方法论坛.
教育经历
2006.9 - 2012.2\t北京航空航天大学 计算机软件与理论 博士研究生毕业 工学博士学位
2004.9 - 2006.7\t北京航空航天大学 计算机应用 其他 无学位
2000.9 - 2004.7\t石家庄铁道大学 计算机科学与技术 大学本科毕业 工学学士学位
工作经历
2012.4 - 2014.12\t法国图卢兹大学
2012.3 - 2015.6\t北京航空航天大学
科研项目
[1] 基于限定自然语言的安全关键软件需求建模及其模型转换、验证方法
[2] 基于需求规约的系统功能建模技术
[3] 面向多核处理器的时间可预测机载软件建模与代码生成方法研究
[4] 安全需求建模与验证方法研究
[5] 面向安全关键系统的时间可预测多核代码生成方法研究
[6] 同步语言时间可预测多线程代码生成方法研究
[7] 安全关键嵌入式软件形式化验证技术研究
[8] 面向高安全系统软件工程的科研教学相促机制研究与实践
[9] 面向多核处理器的安全关键嵌入式软件自动代码生成方法
[10] 面向多核处理器的时间可预测机载软件建模与代码生成方法研究
[11] 时间可预测安全关键软件建模与多核代码生成方法研究
[12] 时间可预测安全关键嵌入式软件多核代码生成方法研究
[13] 弹载计算机软件****
[14] 基于 AADL 多核扩展的航空电子实时系统设计与分析方法
[15] 基于模型的安全关键软件开发工具研究
[16] 实时可靠嵌入式网络系统
[17] 面向航天控制系统的AADL 建模与验证平台
[18] 基于同步语言的时间可预测多线程代码生成方法研究
[19] 可信机载软件****
[20] 机载软件容错技术

研究领域

软件工程
大数据/智能化软件工程、安全关键嵌入式软件(safety-critical software)、模型驱动开发方法、需求工程、形式化方法"安全关键嵌入式软件"

近期论文

1) Zhibin Yang, et al. Model-based Reinforcement Learning and Neural Network-based Policy Compression for Autonomous Spacecraft Rendezvous Guidance. IEEE transactions on industrial informatics. (under revision)
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) 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.
30) 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.
31) Zhibin Yang. A Practical AADL Study in Aerospace Software: from Requirement to Implementation. Memocode 2018.
32) Zhe Chen, Chuanqi Tao, Zhiyi Zhang, Zhibin Yang: Beyond spatial and temporal memory safety. ICSE (Companion Volume) 2018: 189-190
33) Zhe Chen, Zhemin Wang, Yunlong Zhu, Hongwei Xi, Zhibin Yang: Parametric Runtime Verification of C Programs. TACAS 2016: 299-315
34) 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.
35) 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.
36) 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.
37) 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.
38) 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.
39) 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.
40) 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] 杨志斌,,等.系统架构描述语言AADL的功能行为建模扩展.计算机科学与探索,2019
[2] 杨志斌,杨志斌,杨志斌等.Hierarchical behavior annex: Towards an AADL functional specification extension.ACM/IEEE Int. Conf. Formal Methods Model. Syst. Des., MEMOCODE,2018
[3] 杨志斌,,等.一种同步语言多线程代码自动生成工具.软件学报,2019
[4] 杨志斌,,等.面向限定自然语言需求的AADL自动生成工具.小型微型计算机系统,2019
[5] 杨志斌,,等.Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL.Front. Comput. Sci.,2019
[6] 杨志斌,,等.基于限定自然语言需求模板的AADL模型生成方法.软件学报,2018
担任2021年国家自然科学基金通信评审专家，多个会议PC，ACM Trans. on Embedded Computing Systems(TECS)、SCP、JSA、Frontiers of Computer Science(FCS)、Science in China、软件学报等期刊会议审稿人