[發明專利]一種基于雙語自動轉換的間接形式化方法

無效

• 申請號: 201010175296.2
• 申請日: 2010-05-18
• 公開（公告）號: CN102253934A
• 公開（公告）日: 2011-11-23
• 發明（設計）人: 鄒曉輝;鄒順鵬
• 申請（專利權）人: 鄒順鵬;鄒曉輝
• 主分類號: G06F17/30
• 分類號: G06F17/30
• 代理公司: 暫無信息
• 代理人: 暫無信息

技術領域

本發明涉及一種間接形式化方法及雙文雙語并行計算系統，進一步是一種基于雙語自動轉換的間接形式化方法，屬于專用于理論計算機如何轉化為實用計算機的高級信息技術課程計算機輔助教學系統和基于知識本體數據倉庫的雙語界面處理技術領域。

背景技術

形式化方法是基于嚴密的、數學上的形式機制的計算機系統研究方法。從20世紀90年代開始，計算機學科相關專業的形式化方法的教育引起了歐美教育界的高度重視和關注。歐洲的英國、德國、法國、意大利、荷蘭、西班牙等國家的高校相繼為研究生開設了形式化方法方面的課程，并推廣至本科生教育。從20世紀90年代中期開始，美國高校也開展了形式化方法教育研究，并在美國頂尖的35所大學的計算機學科實施了研究生和本科生的教育實踐。形式化方法(FM-Formal?Method)知識體系中的6個知識領域為：①基礎(Foundations)；②形式化規格(Formal?specification?paradigms)；③正確性驗證及演算(Correctness，verification?andcalculation)；④形式化語義(Formal?semantics)；⑤可執行規格支持(Support?forexecutable?specification)；⑥其他(Other?Topics)。形式化方法教育過程中，相關形式化方法工具的支持是非常重要和必要的。歐洲高等院校在形式化方法研究和教育過程中，開發了許多相關工具。形式化工具有：Actress、Alloy、AtelierB、B-Toolkit(Btlk)、BDDC、CADP、CADiZ、CASL、Coq、CommUnity、CWB、ESCJava、FDR、FuZZ、GHC、Gofer、Hugs、HOL、集成網絡分析器(INA)、Isabelle、IVDM、Lotrec、LTSA、NuSMV、Petri網程序設計環境(Petri)、PVS、PicT、RAISEtools、RAT、RML、SPIN、T-Logic、TRIO、UPAAL、VDMT、WHY、ZANS、ZEVES、ZTC等已在相關課程教學中得到使用。形式化方法教育得到歐、美國家高等院校的重視和大力推廣不過是十余年的時間，建立完善的知識體系和課程教學內容還需要進一步的努力。從歐洲58所高校的課程開設情況來看，雖然形式化方法教育得到了大范圍的實施，但是課程內容、授課教材、輔助工具等還比較散雜，建立形式化方法課程的知識內容規范、編寫相關規范指導下的教材、開發相關規范指導下的輔助工具，是亟待解決的問題。形式化方法的工業應用需求和教學過程實踐的經驗積累，已愈來愈體現出計算機相關專業形式化方法教育的必要性和可行性。國內計算相關專業的形式化方法教育還相當薄弱，尚未在高等院校得到有效推廣和實施。計算機相關專業形式化方法課程教學的有效推進還有賴于課程教材、實驗環境、支撐工具以及應用環境等方面的突破。[教育部高等學校計算機科學與技術教學指導委員會.高等學校計算機科學與技術專業發展戰略研究報告暨專業規范(試行)[M].北京：高等教育出版社，2006.]國內有關形式化方法申報發明專利的就更是鳳毛麟角，僅有200610041621.X一種基于Web頁面元數據的用戶訪問行為形式化描述方法，200710123161.X基于XML的圖書內容結構的形式化表示方法，200810101244.3一種基于形式化描述和狀態遷移的XML轉換方法，200910067931.2加入攻擊路徑形式化分析的威脅建模方法。

發明內容

本發明需要解決的技術問題是彌補上述背景技術所欠缺的形式化方法教育，尤其是計算機輔助教學和計算機輔助研究的間接形式化技術，而試圖提供一種基于知識本體數據倉庫的在人機界面可實現廣義的雙語之間在同義并列的前提下對應轉換的間接形式化方法。