基于時序邏輯的Open Solaris內(nèi)核進(jìn)程形式化描述與求精.pdf

1、XYZ系統(tǒng)理論基于Manna-Pnueli線性時序邏輯，其中時序邏輯語言XYZ/E既是一個時序邏輯系統(tǒng)，又可作為可執(zhí)行程序的不同抽象層次的系統(tǒng)描述。作為驗證軟件可靠性和生產(chǎn)軟件工具引擎，具有重要理論價值和實踐意義。 形式化分析操作系統(tǒng)內(nèi)核進(jìn)程通常是基于專用操作系統(tǒng)，這將導(dǎo)致開發(fā)和維護(hù)的難度都很大。而對通用操作系統(tǒng)內(nèi)核進(jìn)程進(jìn)行形式化分析，由于沒有充分開放的授權(quán)，給實際應(yīng)用帶來專利壁壘。Open Solarls是Sun公司開發(fā)的一個

2、多任務(wù)、多用戶操作系統(tǒng)，具有高度實時性、最佳利用率、高可用性、高性能、極高安全性及平臺選擇多樣性。其基于CDDL(通用開發(fā)和發(fā)布許可)開放標(biāo)準(zhǔn)，給研究操作系統(tǒng)和工業(yè)應(yīng)用帶來一次契機(jī)。 本文闡述了Open Solaris內(nèi)核進(jìn)程機(jī)制與現(xiàn)行的Sun Solaris業(yè)界開放標(biāo)準(zhǔn)(CDDL)，基于XYZ/E語言描述了多任務(wù)操作系統(tǒng)內(nèi)核進(jìn)程機(jī)制，使用Sun DTrace工具細(xì)化分析了內(nèi)核進(jìn)程數(shù)據(jù)結(jié)構(gòu)、內(nèi)核進(jìn)程的創(chuàng)建、系統(tǒng)調(diào)度，采用動態(tài)取值