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