基本信息
王淑灵  女  硕导  中国科学院软件研究所
电子邮件: wangsl@ios.ac.cn
通信地址: 北京市中关村南四街4号中科院软件园区5号楼332室
邮政编码:

招生信息

   
招生专业
081202-计算机软件与理论
招生方向
嵌入式系统建模与验证,交互式定理证明

教育背景

2003-09--2008-07   北京大学数学科学学院   博士学位
1999-09--2003-07   兰州大学数学系   学士学位

工作经历

   
工作简历
2017-09~现在, 中科院软件所计算机科学国家重点实验室, 副研究员
2012-09~2017-09,中科院软件所计算机科学国家重点实验室, 助理研究员
2010-09~2012-08,中科院软件所计算机科学国家重点实验室, 博士后
2008-08~2010-07,联合国大学国际软件技术研究所, 博士后

出版信息

   
发表论文
[1] Xiong Xu, Shuling Wang, Bohua Zhan, Xiangyu Jin, Jean-Pierre Talpin, Naijun Zhan. Unified graphical co-modeling, analysis and verification of cyber-physical systems by combining AADL and Simulink/Stateflow. Theoretical Computer Science[J]. 2022, 903: 1-25, [2] Tengshun Yang, Shuling Wang, Bohua Zhan, Naijun Zhan, Jinghui Li, Shuangqing Xiang, Zhan Xiang, Bifei Mao. Formal Analysis of 5G Authentication and Key Management for Applications (AKMA). Journal of Systems Architecture. 2022, 126: [3] Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Bohua Zhan, Naijun Zhan. Semantics Foundation for Cyber-Physical Systems Using Higher-Order UTP. ACM Trans. Softw. Eng. Methodol.[J]. 2022, 1-47, [4] Zhan, Bohua, Gu, Bin, Xu, Xiong, Jin, Xiangyu, Wang, Shuling, Xue, Bai, Li, Xiaofeng, Chen, Yao, Yang, Mengfei, Zhan, Naijun, IEEE COMP SOC. Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander. 2021 IEEE 27TH REAL-TIME AND EMBEDDED TECHNOLOGY AND APPLICATIONS SYMPOSIUM (RTAS 2021)null. 2021, 457-460, [5] Yan, Gaogao, Jiao, Li, Wang, Shuling, Wang, Lingtai, Zhan, Naijun. Automatically Generating SystemC Code from HCSP Formal Models. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY[J]. 2020, 29(1): [6] Lin, QianQian, Wang, ShuLing, Zhan, BoHua, Gu, Bin. Modelling and Verification of Real-Time Publish and Subscribe Protocol Using Uppaal and Simulink/Stateflow. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY[J]. 2020, 35(6): 1324-1342, http://lib.cqvip.com/Qikan/Article/Detail?id=7103652898.
[7] Liu Junyi, Zhan Bohua, Wang Shuling, Ying Shenggang, Liu Tao, Li Yangjia, Ying Mingsheng, Zhan Naijun, Dillig I, Tasiran S. Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. COMPUTER AIDED VERIFICATION, CAV 2019, PT IInull. 2019, 11562: 187-207, [8] 詹乃军. Generating SystemC code from delay HCSP. APLAS. 2017, [9] Wang, Shuling, Zhan, Naijun, Zhang, Lijun. A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems. FORMAL ASPECTS OF COMPUTING[J]. 2017, 29(4): 751-775, https://www.webofscience.com/wos/woscc/full-record/WOS:000404155400007.
[10] Wang Shuling, Nielson Flemming, Nielson Hanne Riis, Zhan Naijun. Modelling and Verifying Communication Failure of Hybrid Systems in HCSP. The Computer Journal[J]. 2017, [11] Yan, Gaogao, Jiao, Li, Wang, Shuling, Zhan, Naijun, Chang, BYE. Synthesizing SystemC Code from Delay Hybrid CSP. PROGRAMMING LANGUAGES AND SYSTEMS (APLAS 2017)null. 2017, 10695: 21-41, [12] Wang, Shuling, Nielson, Flemming, Nielson, Hanne Riis, Zhan, Naijun. Modelling and Verifying Communication Failure of Hybrid Systems in HCSP. COMPUTER JOURNAL[J]. 2017, 60(8): 1111-1130, https://www.webofscience.com/wos/woscc/full-record/WOS:000407592100001.
[13] Yan Gaogao, Jiao Li, Li Yangjia, Wang Shuling, Zhan Naijun, Fitzgerald J, Heitmeyer C, Gnesi S, Philippou A. Approximate Bisimulation and Discretization of Hybrid CSP. FM 2016: FORMAL METHODSnull. 2016, 9995: 702-720, [14] 郭丹青, 吕继东, 王淑灵, 唐涛, 詹乃军, 周达天, 邹亮. 中国高速铁路列控系统的形式化分析与验证. 中国科学. 信息科学[J]. 2015, 45(3): 417-438, [15] Wang Shuling, Nielson Flemming, Nielson Hanne Riis. Denial-of-service security attack in the continuous-time world. 34th IFIPWG6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2014 - Held as Part of the 9th International Federated Conference on Distributed Computing Techniques, DisCoTec 2014null. 2014, 149-165, http://ir.iscas.ac.cn/handle/311060/16503.
[16] Guelev Dimitar P, Wang Shuling, Zhan Naijun, Zhou Chaochen. Super-dense computation in verification of hybrid CSP processes. 10th International Symposium on Formal Aspects of Component Software, FACS 2013null. 2014, 13-22, http://ir.iscas.ac.cn/handle/311060/16514.
[17] Wei KE, Zhiming LIU, Shuling WANG, Liang ZHAO. A graph-based generic type system for object-oriented programs. 中国计算机科学前沿:英文版. 2013, 109-134, http://lib.cqvip.com/Qikan/Article/Detail?id=45066777.
[18] Ke, Wei, Liu, Zhiming, Wang, Shuling, Zhao, Liang. A graph-based generic type system for object-oriented programs. FRONTIERS OF COMPUTER SCIENCE[J]. 2013, 7(1): 109-134, https://www.webofscience.com/wos/woscc/full-record/WOS:000316261500009.
[19] Shu, Qin, Qiu, Zongyan, Wang, Shuling. Confinement framework for encapsulating objects. FRONTIERS OF COMPUTER SCIENCE[J]. 2013, 7(2): 236-256, https://www.webofscience.com/wos/woscc/full-record/WOS:000317303800008.
[20] Griesmayer, Andreas, Liu, Zhiming, Morisset, Charles, Wang, Shuling. A framework for automated and certified refinement steps. INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING[J]. 2013, 9(1): 3-16, [21] Qin SHU, Zongyan QIU, Shuling WANG. Confinement framework for encapsulating objects. 中国计算机科学前沿:英文版. 2013, 236-256, http://lib.cqvip.com/Qikan/Article/Detail?id=45714033.
[22] Wang Shuling, Zhan Naijun, Guelev Dimitar. An assume/guarantee based compositional calculus for hybrid csp. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)null. 2012, 72-83, http://ir.iscas.ac.cn/handle/311060/15723.
发表著作
(1) Formal Verification of Simulink/Stateflow Diagrams: A Deductive Approach, Springer, 2017-01, 第 2 作者

科研活动

   
科研项目
( 1 ) 面向程序验证的自动定理证明理论、方法 与工具研究, 参与, 国家级, 2018-01--2022-12
( 2 ) 多异质嵌入式系统的建模、仿真与验证研究, 主持, 国家级, 2020-01--2023-12

指导学生

现指导学生

易士程  硕士研究生  081200-计算机科学与技术