摘要:由于溫室環(huán)境的復(fù)雜性,,系統(tǒng)設(shè)計的不合理會直接導(dǎo)致數(shù)據(jù)的不確定和系統(tǒng)的不穩(wěn)定,?;隗w系結(jié)構(gòu)的物聯(lián)網(wǎng)層次模型對物聯(lián)網(wǎng)的實施具有指導(dǎo)意義,,但是體系結(jié)構(gòu)模型沒有提供系統(tǒng)建模工具和模型驗證的方法?;跁r間自動機理論的建模與模型驗證方法是一種對物聯(lián)網(wǎng)系統(tǒng)建模的有效手段,,能在系統(tǒng)設(shè)計時提高系統(tǒng)的穩(wěn)定性,保證系統(tǒng)設(shè)計的正確性,。通過對智能溫室監(jiān)控物聯(lián)網(wǎng)系統(tǒng)的分析,,從系統(tǒng)實施的角度重新對溫室環(huán)境監(jiān)控物聯(lián)網(wǎng)系統(tǒng)進行了層次劃分,利用時間自動機理論對系統(tǒng)中的相應(yīng)組件進行建模,,在對各個子系統(tǒng)分別建模的基礎(chǔ)上形成了時間自動機網(wǎng)絡(luò)模型,。最后利用時間自動機建模工具UPPAAL,對已經(jīng)建立的形式化模型進行了系統(tǒng)邏輯正確性驗證與系統(tǒng)執(zhí)行時序驗證,。結(jié)果表明,,利用時間自動機理論及其建模工具UPPAAL可以對智能溫室監(jiān)控物聯(lián)網(wǎng)系統(tǒng)進行建模及模型驗證,可以在系統(tǒng)設(shè)計時對系統(tǒng)進行準確的模型分析,,避免系統(tǒng)設(shè)計錯誤,,降低系統(tǒng)設(shè)計缺陷,在系統(tǒng)投入運行中規(guī)避設(shè)計風險,,從而提升系統(tǒng)的穩(wěn)定性與可靠性,,確保系統(tǒng)設(shè)計的正確性。