• 
<ul id="auswy"><sup id="auswy"></sup></ul>
  • 

  • <ul id="auswy"></ul>
    

    
    
    
    
                                    ABB
                            
    
            關注中國自動化產業發展的先行者！
            
    
                
				
                
                
                
            
    
        
    
    
    

    

    
    
    
    
        
        
        
        
       
					
    
				
    
					
    
												
    
							CAIAC 2025
						
    
												
    
							2025工業安全大會
						
    
												
    
							OICT公益講堂
						
    
						
					
    
				
    
				
    
			
    
		
    
    

    

    
    
    
    

    


    
        
    
            
            當前位置：首頁 >> 案例 >> 案例首頁
        
    
        
    
            
    案例頻道
    
        
    
		
    
			
    
				
    可信編譯器中地址不相交的保持性證明
    
				
    
					
				
    
				
                				
    
                    同步數據流語言是一種廣泛應用于核電及其他安全關鍵領域的語言，在同步數據流語言到順序執行語言的翻譯轉換過程中，語義等價要保證賦值語句的左右值地址互不相交，這至關重要。本文使用形式化方法描述了翻譯過程中地址互不相交的性質，并通過定理證明的方式對其進行了驗證。基于本方法的編譯器在某核電站的安全保護系統中得到了應用。
				
    
                
				
				
    
                    
    北京廣利核系統工程有限公司 谷偉卿，張智慧，白濤，齊敏
    摘要：同步數據流語言是一種廣泛應用于核電及其他安全關鍵領域的語言，在同步數據流語言到順序執行語言的翻譯轉換過程中，語義等價要保證賦值語句的左右值地址互不相交，這至關重要。本文使用形式化方法描述了翻譯過程中地址互不相交的性質，并通過定理證明的方式對其進行了驗證。基于本方法的編譯器在某核電站的安全保護系統中得到了應用。
    關鍵詞：同步數據流；定理證明；Coq；語義等價；地址不相交
    在線預覽：可信編譯器中地址不相交的保持性證明
    摘自《自動化博覽》2017年4月刊
    
				
    
			
    
			
    
                                    
    熱點新聞
    
                    
                
                                    
    推薦產品
    
                    
                			
    
		
    

        


	
    

    









    



    
    
    x
    
    
    


    • 在線反饋
    

    

    


    1.我有以下需求：
    

    
    
        
            
    
            
    
            
    
                
        		

    

    2.詳細的需求：
    

    

    
    姓名:
    

    

    
    單位:
    

    

    
    電話:
    

    

    
    郵件: