Formal Verification Technology for Asynchronous Communication Protocol

被引:2
作者
Hu, Yayun [1 ]
Li, Dongfang [1 ]
机构
[1] Beijing Inst Comp Technol & Applicat, Dept Software Engn & Software Evaluat, Beijing, Peoples R China
来源
2019 COMPANION OF THE 19TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY (QRS-C 2019) | 2019年
关键词
formal verification; asynchronous communication; property; PSL; assert;
D O I
10.1109/QRS-C.2019.00092
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
For aerospace FPGA software products, traditional simulation method faces severe challenges to verify product requirements under complicated scenarios. Given the increasing maturity of formal verification technology, this method can significantly improve verification work efficiency and product design quality, by expanding coverage on those "blind spots" in product design which were not easily identified previously. Taking UART communication as an example, this paper proposes several critical points to use formal verification for asynchronous communication protocol. Experiments and practices indicate that formal verification for asynchronous communication protocol can effectively reduce the time required, ensure a complete verification process and more importantly, achieve more accurate and intuitive results.
引用
收藏
页码:482 / 486
页数:5
相关论文
共 9 条
[1]  
[Anonymous], IEEEP1850
[2]  
[Anonymous], 2003, PROP SPEC LANG REF M
[3]  
Bustan D., 2005, AUTOMATA CONSTRUCTIO
[4]  
Clarke E.M., 2001, Model Checking
[5]  
DAMORIM M, 2005, CAV, V3576, P364
[6]  
Gordon Michael J. C., FORMAL ASPECTS COMPU
[7]  
Jobstmann B, 2006, PROCEEDINGS OF FORMAL METHODS IN COMPUTER AIDED DESIGN, P117
[8]  
Kim N., 2014, DES VER C DVCON 2014
[9]  
Singhal Vigyan, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P44, DOI 10.1007/978-3-642-22110-1_5