北京廣利核系統(tǒng)工程有限公司 孫王強(qiáng)
摘要:多線程并行運(yùn)行的軟件在提高性能的同時(shí),其交互的組合隨著程序規(guī)模增大變得更為復(fù)雜,給軟件的設(shè)計(jì)與驗(yàn)證帶來(lái)了挑戰(zhàn)。本文從常見(jiàn)的并行缺陷入手,提出使用模型檢測(cè)的方法對(duì)其進(jìn)行檢測(cè)和分析,實(shí)踐表明,使用該方法可有效檢測(cè)此類并行缺陷。
關(guān)鍵詞:并發(fā)缺陷;多線程軟件;模型檢測(cè)
Abstract: Multithreading parallel running software not only improves the performance, but also brings challenges to software design and verification, because the combination of its interaction becomes more complex with the increase of program size. In this paper, the common concurrent defects are analyzed and verified by using model checking method. The practice shows that this method can effectively this kind of concurrent defects.
Key words: Concurrent defects; Multithreading software; Model check
點(diǎn)擊預(yù)覽:模型檢測(cè)技術(shù)在軟件并行缺陷檢測(cè)中的應(yīng)用.pdf
摘自《自動(dòng)化博覽》2021年4月刊