今日頭條
官方微信
官方抖音
案例頻道北京廣利核系統(tǒng)工程有限公司 谷偉卿，張智慧，白濤，齊敏
摘要：同步數(shù)據(jù)流語(yǔ)言是一種廣泛應(yīng)用于核電及其他安全關(guān)鍵領(lǐng)域的語(yǔ)言，在同步數(shù)據(jù)流語(yǔ)言到順序執(zhí)行語(yǔ)言的翻譯轉(zhuǎn)換過(guò)程中，語(yǔ)義等價(jià)要保證賦值語(yǔ)句的左右值地址互不相交，這至關(guān)重要。本文使用形式化方法描述了翻譯過(guò)程中地址互不相交的性質(zhì)，并通過(guò)定理證明的方式對(duì)其進(jìn)行了驗(yàn)證。基于本方法的編譯器在某核電站的安全保護(hù)系統(tǒng)中得到了應(yīng)用。
關(guān)鍵詞：同步數(shù)據(jù)流；定理證明；Coq；語(yǔ)義等價(jià)；地址不相交
在線預(yù)覽：可信編譯器中地址不相交的保持性證明
摘自《自動(dòng)化博覽》2017年4月刊
北京市公安局海淀分局備案號(hào)：11010802023656號(hào)