Formal Verification Technology for Asynchronous Communication Protocol
Title | Formal Verification Technology for Asynchronous Communication Protocol |
Publication Type | Conference Paper |
Year of Publication | 2019 |
Authors | Hu, Yayun, Li, Dongfang |
Conference Name | 2019 IEEE 19th International Conference on Software Quality, Reliability and Security Companion (QRS-C) |
ISBN Number | 978-1-7281-3925-8 |
Keywords | aerospace FPGA software products, assert, asynchronous communication, asynchronous communication protocol, blind spots, Clocks, Collaboration, complete verification process, composability, compositionality, field programmable gate arrays, formal verification, formal verification technology, policy-based governance, privacy, process control, Product design, product design quality, property, protocol verification, Protocols, PSL, pubcrawl, Software, traditional simulation method, UART communication, verification work efficiency |
Abstract | 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. |
URL | https://ieeexplore.ieee.org/document/8859490 |
DOI | 10.1109/QRS-C.2019.00092 |
Citation Key | hu_formal_2019 |
- policy-based governance
- verification work efficiency
- UART communication
- traditional simulation method
- Software
- pubcrawl
- PSL
- Protocols
- protocol verification
- property
- product design quality
- Product design
- process control
- privacy
- aerospace FPGA software products
- formal verification technology
- formal verification
- field programmable gate arrays
- Compositionality
- composability
- complete verification process
- collaboration
- Clocks
- blind spots
- asynchronous communication protocol
- asynchronous communication
- assert