Contents

Rational Delegation Computing Protocol Based on Rational Trust Model FENG Neng-Xian, TIAN You-Liang Published June 06, 2021 (13 pages) 2021,32(6):1910-1922 [Abstract(2002)]  [View PDF(3928)1.30 M]

Special Issue's Articles

形式化方法与应用专题前言 田聪，邓玉欣，姜宇 Published June 06, 2021 (2 pages) 2021,32(6):1579-1580 [Abstract(2640)]  [View PDF(7880)297.02 K]

C2P: Formal Abstraction Method and Tool for C Protocol Code Based on Pi Caculus ZHANG Xie-Li, ZHU Yue-Fei, GU Chun-Xiang, CHEN Xi Published June 06, 2021 (16 pages) 2021,32(6):1581-1596 [Abstract(3113)]  [View PDF(6963)1.72 M]

Automatic Generation of Large-Granularity Pull Request Description KUANG Li, SHI Ru-Yi, ZHAO Lei-Hao, ZHANG Huan, GAO Hong-Hao Published June 06, 2021 (15 pages) 2021,32(6):1597-1611 [Abstract(2737)]  [View PDF(6832)1.60 M]

Reverse Unfolding of Petri Nets and its Application in Program Data Race Detection HAO Zong-Yin, LU Fa-Ming Published June 06, 2021 (19 pages) 2021,32(6):1612-1630 [Abstract(2746)]  [View PDF(5902)2.15 M]

Verification of Operating System Exception Management for SPARC Processor Architecture MA Zhi, QIAO Lei, YANG Meng-Fei, LI Shao-Feng Published June 06, 2021 (16 pages) 2021,32(6):1631-1646 [Abstract(2893)]  [View PDF(6503)1.59 M]

Code Generation Method of Data Flow Model Based on Branch Marking SU Zhuo, WANG Dong-Yan, YANG Yi-Xiao, ZHANG Ming-Rui, JIANG Yu, SUN Jia-Guang Published June 06, 2021 (16 pages) 2021,32(6):1647-1662 [Abstract(2882)]  [View PDF(6528)1.55 M]

On Schedulability Analysis of AADL Architecture with Storage Resource Constraint LU Yin, QIN Shu-Dong, XI Le-Qi, DONG Yun-Wei Published June 06, 2021 (19 pages) 2021,32(6):1663-1681 [Abstract(2359)]  [View PDF(5931)1.79 M]

Deadlock Detection of Multithreaded Programs Based on Lock-augmented Segmentation Graph LU Fa-Ming, ZHENG Jia-Jing, BAO Yun-Xia, ZENG Qing-Tian, DUAN Hua, WANG Xiao-Yu Published June 06, 2021 (19 pages) 2021,32(6):1682-1700 [Abstract(2700)]  [View PDF(6770)2.00 M]

Taint Analysis Tool of Android Applications Based on Tainted Value Graph ZHANG Jie, TIAN Cong, DUAN Zhen-Hua Published June 06, 2021 (16 pages) 2021,32(6):1701-1716 [Abstract(3298)]  [View PDF(7298)1.54 M]

Executable Semantics of Ethereum Intermediate Language HAN Ning, LI Xi-Meng, ZHANG Qian-Ying, WANG Guo-Hui, SHI Zhi-Ping, GUAN Yong Published June 06, 2021 (16 pages) 2021,32(6):1717-1732 [Abstract(2723)]  [View PDF(6988)1.55 M]

Smooth Intervention Model of Individual Interaction Behavior LIU Xiao, ZHANG Zhao-Hui, WEI Zi-Ming, WANG Peng-Wei Published June 06, 2021 (15 pages) 2021,32(6):1733-1747 [Abstract(2641)]  [View PDF(6429)1.60 M]

Raft with Out-of-order Executions GU Xiao-Song, WEI Heng-Feng, QIAO Lei, HUANG Yu Published June 06, 2021 (31 pages) 2021,32(6):1748-1778 [Abstract(3292)]  [View PDF(7960)2.82 M]

Hybrid AADL Modeling and Model Transformation for CPS Time and Space Properties Verification CHEN Xiao-Ying, ZHU Yi, ZHAO Yu, WANG Jin-Yong Published June 06, 2021 (20 pages) 2021,32(6):1779-1798 [Abstract(2646)]  [View PDF(6617)2.09 M]

Formal Method of Functional Verification for Chip Development YAO Guang-Yu, ZHANG Nan, TIAN Cong, DUAN Zhen-Hua, LIU Ling-Min, SUN Feng-Jin Published June 06, 2021 (19 pages) 2021,32(6):1799-1817 [Abstract(3173)]  [View PDF(7313)1.86 M]

Modeling and Analysis of ROS2 Data Distribution Service for Data Flow LU Qian, LI Xiao-Juan, GUAN Yong, WANG Rui, SHI Zhi-Ping Published June 06, 2021 (12 pages) 2021,32(6):1818-1829 [Abstract(3325)]  [View PDF(7128)1.51 M]

Formal Verification of Ptolemy Discrete Event Model LU Zhi-Hao, WANG Rui, KONG Hui, GUAN Yong, SHI Zhi-Ping Published June 06, 2021 (19 pages) 2021,32(6):1830-1848 [Abstract(2721)]  [View PDF(6541)2.08 M]

Formal Verification of Smart Contract Based on MSVL WANG Xiao-Bing, YANG Xiao-Yu, SHU Xin-Feng, ZHAO Liang Published June 06, 2021 (18 pages) 2021,32(6):1849-1866 [Abstract(3090)]  [View PDF(6818)1.88 M]

Differential Fuzz Testing of Robot Operating System WANG Ying, WANG Bing-Qing, GUAN Yong, LI Xiao-Juan, WANG Rui Published June 06, 2021 (15 pages) 2021,32(6):1867-1881 [Abstract(3068)]  [View PDF(7294)1.66 M]

Formalization of Operations of Block Matrix Based on Coq MA Ying-Ying, MA Zhen-Wei, CHEN Gang Published June 06, 2021 (28 pages) 2021,32(6):1882-1909 [Abstract(2796)]  [View PDF(7869)3.44 M]