小型微型计算机系统
小型微型計算機繫統
소형미형계산궤계통
MINI-MICRO SYSTEMS
2013年
7期
1537-1542
,共6页
操作系统%模型检测%Spin%Modex
操作繫統%模型檢測%Spin%Modex
조작계통%모형검측%Spin%Modex
operating system%model checking%Spin%Modex
传统的模型检测摒除了很多软件实现细节,要检测实际的代码,就需要从代码中直接建立抽象描述.而操作系统内核结构复杂,手动对源代码进行抽象存在建模工作量大、人工参与过多易出错以及属性难以描述和检测等问题.本文以Linux内核作为实验对象,提出了一种基于属性的OS内核自动验证方法,利用模型抽取工具Modex自动的从inux内核源代码抽取模型,试图保证模型与实现代码一致性的同时减少因人工参与产生的人为错误,然后用时间轴属性来描述属性,最后用模型检测工具Spin对Linux内核代码模型进行检测.实验选取了Linux内核中接口和数据结构相对复杂的调度器进行模型的自动抽取与属性检测,验证了该方法在操作系统内核模型检测中的有效性和实用性.
傳統的模型檢測摒除瞭很多軟件實現細節,要檢測實際的代碼,就需要從代碼中直接建立抽象描述.而操作繫統內覈結構複雜,手動對源代碼進行抽象存在建模工作量大、人工參與過多易齣錯以及屬性難以描述和檢測等問題.本文以Linux內覈作為實驗對象,提齣瞭一種基于屬性的OS內覈自動驗證方法,利用模型抽取工具Modex自動的從inux內覈源代碼抽取模型,試圖保證模型與實現代碼一緻性的同時減少因人工參與產生的人為錯誤,然後用時間軸屬性來描述屬性,最後用模型檢測工具Spin對Linux內覈代碼模型進行檢測.實驗選取瞭Linux內覈中接口和數據結構相對複雜的調度器進行模型的自動抽取與屬性檢測,驗證瞭該方法在操作繫統內覈模型檢測中的有效性和實用性.
전통적모형검측병제료흔다연건실현세절,요검측실제적대마,취수요종대마중직접건립추상묘술.이조작계통내핵결구복잡,수동대원대마진행추상존재건모공작량대、인공삼여과다역출착이급속성난이묘술화검측등문제.본문이Linux내핵작위실험대상,제출료일충기우속성적OS내핵자동험증방법,이용모형추취공구Modex자동적종inux내핵원대마추취모형,시도보증모형여실현대마일치성적동시감소인인공삼여산생적인위착오,연후용시간축속성래묘술속성,최후용모형검측공구Spin대Linux내핵대마모형진행검측.실험선취료Linux내핵중접구화수거결구상대복잡적조도기진행모형적자동추취여속성검측,험증료해방법재조작계통내핵모형검측중적유효성화실용성.
