對自動(dòng)機(jī)模型學(xué)習(xí)問題的分析與研究

張圣迪

摘要：形式化方法在模型為導(dǎo)向的軟件工程中起到非常重要的作用，其中模型檢驗(yàn)已經(jīng)成為軟件驗(yàn)證和糾錯(cuò)的一種重要方法，而模型學(xué)習(xí)是對于模型檢驗(yàn)的一種有效補(bǔ)充技術(shù)。本文將對模型學(xué)習(xí)的概念和研究意義進(jìn)行介紹，匯總了幾種常見的對于寄存器自動(dòng)機(jī)和時(shí)間自動(dòng)機(jī)的模型學(xué)習(xí)的方法，并提出了一種對于時(shí)間自動(dòng)機(jī)進(jìn)行學(xué)習(xí)模仿的算法思想，最后對于模型學(xué)習(xí)的主要研究方向進(jìn)行了闡述。

關(guān)鍵詞：模型學(xué)習(xí)；形式化方法；時(shí)間自動(dòng)機(jī)；寄存器自動(dòng)機(jī)

中圖分類號：TP311 文獻(xiàn)標(biāo)識碼：A

文章編號：1009-3044（2019）10-0171-03

開放科學(xué)（資源服務(wù)）標(biāo)識碼（OSID）：

1 引言

任何一個(gè)軟硬件系統(tǒng)在開發(fā)之前都有一個(gè)事先預(yù)定的系統(tǒng)規(guī)約，然后根據(jù)系統(tǒng)的需求進(jìn)行設(shè)計(jì)和開發(fā)。最后經(jīng)過測試才能保證系統(tǒng)能夠一定程度上完成需求規(guī)約中描述的功能和行為。如果我們想要對一個(gè)系統(tǒng)進(jìn)行分析，可以采取在需求文檔階段進(jìn)行仿真的方法，也可以對開發(fā)后的真實(shí)系統(tǒng)進(jìn)行實(shí)際的測試分析。當(dāng)用形式化的方法分析一個(gè)軟硬件系統(tǒng)時(shí)，學(xué)者們希望通過某種手段推斷系統(tǒng)的抽象模型，然后根據(jù)模型檢驗(yàn)來對系統(tǒng)的行為進(jìn)行分析。模型學(xué)習(xí)的目標(biāo)是通過用觀察得到的系統(tǒng)行為序列和相關(guān)的數(shù)據(jù)來構(gòu)建軟件和硬件系統(tǒng)的狀態(tài)圖模型，可以解決上述的系統(tǒng)模型建立問題。其中涉及的模型學(xué)習(xí)算法的設(shè)計(jì)和實(shí)現(xiàn)是一個(gè)非常具有研究價(jià)值的問題。從理論角度分析，這種形式化的方法更具有可信度和完備性。

本文對于近十年來可用性強(qiáng)的一些模型學(xué)習(xí)算法進(jìn)行了匯總，其中設(shè)計(jì)的模型主要分為確定性有限自動(dòng)機(jī)模型，寄存器自動(dòng)機(jī)模型和時(shí)間自動(dòng)機(jī)模型。并在之后提出了一個(gè)用于學(xué)習(xí)時(shí)間自動(dòng)機(jī)的框架。

2 背景

有很多推斷軟件組件模型的方法，比如分析具體代碼、挖掘系統(tǒng)日志、執(zhí)行測試等等。也有很多不同種類的模型能支持這些推斷方法，比如馬爾可夫模型、變量之間的關(guān)系模型、類圖模型等等。本文的關(guān)注點(diǎn)是在一種特定類型的模型之內(nèi)，即狀態(tài)圖（又稱自動(dòng)機(jī)），其對于理解許多軟件系統(tǒng)的行為至關(guān)重要，例如安全協(xié)議、網(wǎng)絡(luò)協(xié)議和嵌入式控制軟件。模型推斷技術(shù)可以基于白盒或黑盒，區(qū)別在于是否需要訪問代碼。黑盒技術(shù)的優(yōu)點(diǎn)是相對容易使用，并可以應(yīng)用在我們沒有代碼訪問權(quán)限或有效的白盒工具的情況下。主動(dòng)學(xué)習(xí)的技術(shù)是通過主動(dòng)地對軟件進(jìn)行實(shí)驗(yàn)測試來完成它們的任務(wù)的技術(shù)。此外，還有被動(dòng)學(xué)習(xí)的方法，其中的模型是根據(jù)軟件的許多的運(yùn)行行為的集合而構(gòu)建的。主動(dòng)學(xué)習(xí)的優(yōu)點(diǎn)是它能夠提供軟件組件的全部完備的行為的模型，而不像被動(dòng)學(xué)習(xí)那樣僅僅提供在實(shí)際操作期間發(fā)生的某系特定運(yùn)行行為的模型。

近年來，模型學(xué)習(xí)技術(shù)已經(jīng)具有了許多成功應(yīng)用到不同領(lǐng)域的實(shí)際案例，比如西門子的電信系統(tǒng)的回歸測試分析，法國電信的集成測試分析，在施普林格出版社線上會議服務(wù)系統(tǒng)的自動(dòng)化測試分析，在沃爾沃科技公司的線控制動(dòng)系統(tǒng)的需求測試分析等等。事實(shí)上，模型學(xué)習(xí)正在成為銀行卡、網(wǎng)絡(luò)協(xié)議、遺產(chǎn)軟件等領(lǐng)域中能夠?qū)嶋H使用的一種高效的漏洞尋找技術(shù)。

3 學(xué)習(xí)算法

3.1 確定性有限自動(dòng)機(jī)

目前學(xué)術(shù)界對于確定性有限狀態(tài)自動(dòng)機(jī)的模型學(xué)習(xí)已經(jīng)有了一些不錯(cuò)的研究成果。在1987 年，Angluin 發(fā)表了相關(guān)研討論文[2]，她根據(jù) Myhill-Nerode定理（對于給定一種語言L，和一對字符串x和y，定義一個(gè)能產(chǎn)生區(qū)別的延續(xù)字符串z，使得兩個(gè)字符串xz和yz中只有一個(gè)屬于L。對于這樣的字符串的定義一種RL規(guī)則：如果對于x和y不存在上述的能區(qū)別的延續(xù)字符串z，則x RL y可以看出來，RL是字符串上的一種等價(jià)關(guān)系，可以利用這個(gè)關(guān)系將字符串的集合劃分為若干個(gè)等價(jià)類。）表明可以使用詢問方式來學(xué)習(xí)到有限自動(dòng)機(jī)，并稱之為MAT框架。在該框架中，學(xué)習(xí)被看作是一種博弈，其中學(xué)習(xí)者模塊必須通過詢問教師模塊來推斷一個(gè)未知的狀態(tài)圖的行為。學(xué)習(xí)者的任務(wù)是通過兩種類型的詢問來學(xué)習(xí)原始模型：成員查詢：學(xué)習(xí)者詢問一個(gè)行為序列是否是能被原始自動(dòng)機(jī)接收，教師使用接收或拒絕來回答。等價(jià)查詢：學(xué)習(xí)者通過成員查詢所得的行為序列集合來構(gòu)建一個(gè)初步的假設(shè)模型，然后向教師詢問該假設(shè)模型與原始模型是否等價(jià)，即兩個(gè)模型對于任一行為序列的接收能力是否等同。如果情況屬實(shí)，教師回答「是」。否則教師回答「否」，并提供一個(gè)反例的行為序列來區(qū)分兩個(gè)模型，并將反例返回給學(xué)習(xí)者。學(xué)習(xí)者通過反例繼續(xù)修改假設(shè)模型，繼續(xù)以上兩種提問，直到教師對于等價(jià)查詢回答「是」。

Angluin提出的L*算法的設(shè)計(jì)能夠通過多項(xiàng)式數(shù)量級（多項(xiàng)式數(shù)的大小對應(yīng)于規(guī)范的自動(dòng)機(jī)的規(guī)模）的復(fù)雜度的成員查詢和等價(jià)查詢來學(xué)習(xí)自動(dòng)機(jī)。L*算法只是一種簡單的設(shè)計(jì)和表達(dá)，而后來更多學(xué)者對這個(gè)算法進(jìn)行了擴(kuò)展和優(yōu)化，但是MAT框架依然是一種有效的模型學(xué)習(xí)框架。

3.2 寄存器自動(dòng)機(jī)

盡管學(xué)習(xí)自動(dòng)機(jī)模型的基本算法研究工作已經(jīng)取得了進(jìn)展，但是這些算法只能處理規(guī)模比較小的有限狀態(tài)自動(dòng)機(jī)，而且很難應(yīng)用于實(shí)際的系統(tǒng)分析。能初步應(yīng)用于部分領(lǐng)域的一種自動(dòng)機(jī)模型稱為寄存器自動(dòng)機(jī)，這種自動(dòng)機(jī)模型能夠存儲中間過程中產(chǎn)生的數(shù)據(jù)值，實(shí)現(xiàn)對數(shù)據(jù)流的部分操作，能夠用于描述一部分實(shí)際系統(tǒng)的操作行為，比如模擬一個(gè)存儲隊(duì)列的行為。在寄存器自動(dòng)機(jī)中，所有數(shù)據(jù)值都是完全對稱的（只做數(shù)據(jù)值的判等，而不對數(shù)據(jù)值進(jìn)行直接修改），在學(xué)習(xí)算法中可以利用這種對稱性。在寄存器自動(dòng)機(jī)的模型學(xué)習(xí)過程中，比較重要的一點(diǎn)是如何處理一個(gè)數(shù)據(jù)語句中那些需要被存入寄存器的值，因?yàn)檫@些值很可能之后要被用來與參數(shù)值進(jìn)行比較或者用作輸出。

Sofia Cassel等人定義了一種可以滿足Mihill Nerode定理的特殊的寄存器自動(dòng)機(jī)，并提出了對應(yīng)這種自動(dòng)機(jī)的模型學(xué)習(xí)算法SL*[3，4]。模型學(xué)習(xí)算法通常依賴于這種右同余關(guān)系來識別學(xué)習(xí)自動(dòng)機(jī)的狀態(tài)和遷移：如果兩個(gè)語句的剩余語言一致，則這兩個(gè)語句會到達(dá)同一狀態(tài)。其基本思想是為寄存器自動(dòng)機(jī)定義類似Nerode的同余，用來推斷確定自動(dòng)機(jī)的狀態(tài)，遷移上的寄存器約束和遷移上寄存器的賦值。該算法利用了觀察表以及自動(dòng)機(jī)的對稱性質(zhì)，實(shí)現(xiàn)的基礎(chǔ)數(shù)據(jù)結(jié)構(gòu)被稱為符號決策樹。

學(xué)習(xí)寄存器自動(dòng)機(jī)的另一種實(shí)用的方法[5]，是Aarts等人在軟件工具Tomte中實(shí)現(xiàn)的。一種確定性的右不變的寄存器自動(dòng)機(jī)，也是基于右同余的關(guān)系進(jìn)行學(xué)習(xí)。Tomte能夠支持學(xué)習(xí)帶輸入輸出的寄存器自動(dòng)機(jī)，整個(gè)算法需要多個(gè)輔助模塊：原始的學(xué)習(xí)者可以學(xué)習(xí)構(gòu)建一個(gè)有限的確定性Mealy機(jī)，再利用抽象模塊可以學(xué)習(xí)一個(gè)限制種類的寄存器自動(dòng)機(jī)，而預(yù)兆先知模塊讓學(xué)習(xí)種類更加寬泛的寄存器自動(dòng)機(jī)成為可能，確定器模塊可以幫助學(xué)習(xí)遷移上帶有新輸出的輸入輸出寄存器自動(dòng)機(jī)。整個(gè)想學(xué)習(xí)過程的設(shè)計(jì)基于映射器的思想，并且被證明是學(xué)習(xí)寄存器自動(dòng)機(jī)的一種有效方法。

3.3 時(shí)間自動(dòng)機(jī)

時(shí)間自動(dòng)機(jī)是一個(gè)帶有有限時(shí)鐘集合的有窮狀態(tài)機(jī)，提供了一種簡單而有效的方法來描述帶有時(shí)間因素的系統(tǒng)狀態(tài)轉(zhuǎn)換圖，屬于混合自動(dòng)機(jī)的一個(gè)重要分支。它主要用于對計(jì)算機(jī)軟件和硬件系統(tǒng)的時(shí)間行為進(jìn)行建模和分析，比如一般的實(shí)時(shí)系統(tǒng)和網(wǎng)絡(luò)系統(tǒng)。對于時(shí)間自動(dòng)機(jī)的檢驗(yàn)?zāi)繕?biāo)主要集中于安全性和響應(yīng)程度的性質(zhì)檢驗(yàn)。

瑞典烏普薩拉大學(xué)計(jì)算機(jī)系的Olga Grinchtein等人在MAT的模型學(xué)習(xí)框架下提出了對時(shí)間自動(dòng)機(jī)的一個(gè)子類--確定性事件記錄自動(dòng)機(jī)的學(xué)習(xí)算法LSGDERA（學(xué)習(xí)帶有明確時(shí)間監(jiān)視的確定性事件記錄自動(dòng)機(jī)）[6]，通過確定性事件記錄自動(dòng)機(jī)與確定性有限自動(dòng)機(jī)的同構(gòu)性和相關(guān)的語言等價(jià)性，將學(xué)習(xí)確定性有限自動(dòng)機(jī)的算法成功改進(jìn)成為學(xué)習(xí)一個(gè)事件記錄自動(dòng)機(jī)的算法。另外他們對于一般的事件記錄自動(dòng)機(jī)，利用LSGDERA和相關(guān)的合并操作得到一個(gè)比較廣泛的學(xué)習(xí)算法。他們的算法非常有開創(chuàng)性，但是算法的復(fù)雜度非常高且難以實(shí)現(xiàn)。

之后Olga又提出用時(shí)間決策樹的方法[7]去學(xué)習(xí)一個(gè)時(shí)間確定性的事件記錄自動(dòng)機(jī)，在事件記錄自動(dòng)機(jī)中時(shí)鐘變量記錄的是一個(gè)事件前一次發(fā)生之后所度過的時(shí)間。對每一個(gè)事件，事件記錄自動(dòng)機(jī)維護(hù)一個(gè)時(shí)鐘來保存這個(gè)時(shí)間變量。其接收的行為序列是時(shí)鐘語句，這種時(shí)鐘語句可以從一般的時(shí)間語句轉(zhuǎn)換而來。該學(xué)習(xí)算法中提出了最強(qiáng)后置條件的設(shè)定，根據(jù)成員詢問與等價(jià)詢問生成和修改時(shí)間決策樹，并在這個(gè)數(shù)據(jù)結(jié)構(gòu)中結(jié)合最強(qiáng)后置條件來對狀態(tài)節(jié)點(diǎn)進(jìn)行劃分，來產(chǎn)生自動(dòng)機(jī)中的時(shí)間監(jiān)視約束，并對統(tǒng)一行為的節(jié)點(diǎn)進(jìn)行合并，最終將整個(gè)時(shí)間決策樹折疊成一個(gè)時(shí)間確定性的事件記錄自動(dòng)機(jī)。它是第一個(gè)避免使用時(shí)間層域的概念來學(xué)習(xí)時(shí)間自動(dòng)記錄自動(dòng)機(jī)的學(xué)習(xí)算法。它的優(yōu)勢在于能推廣拓展到確定性的時(shí)間自動(dòng)機(jī)，有強(qiáng)的表達(dá)能力，但是劣勢在于高的復(fù)雜度。

荷蘭代爾夫特理工大學(xué)的Sicco Verwer等人根據(jù)Miguel Bugalho等人提出了以DFA學(xué)習(xí)的紅藍(lán)邊狀態(tài)合并算法為基礎(chǔ)的對于單個(gè)時(shí)鐘的實(shí)時(shí)自動(dòng)機(jī)進(jìn)行模型學(xué)習(xí)的啟發(fā)式狀態(tài)合并算法[8]。根據(jù)系統(tǒng)對于抽樣的時(shí)間行為軌跡樣本的接受與否，將樣本集合分為接受集合和拒絕集合，并根據(jù)這些行為軌跡集合生成相應(yīng)的樹形結(jié)構(gòu)APTA（擴(kuò)增前綴樹接收結(jié)構(gòu)）。在APTA的基礎(chǔ)上可以對其中的結(jié)點(diǎn)進(jìn)行三類操作：合并，分離，染色。該算法根據(jù)樣本接受狀態(tài)的一致性問題制定了相應(yīng)的評分制度對操作進(jìn)行評分，其中分高的操作先執(zhí)行。最終APTA整合成一個(gè)待時(shí)間約束的確定性自動(dòng)機(jī)，該自動(dòng)機(jī)是單時(shí)鐘，并且每次遷移都要重置時(shí)鐘。這個(gè)算法有一定的實(shí)用性，但是在具體的實(shí)踐應(yīng)用中，開始時(shí)軌跡的樣本是事先一次性確定好的，而最終該算法學(xué)習(xí)出實(shí)時(shí)自動(dòng)機(jī)模型是與最初對系統(tǒng)行為的抽樣緊密相關(guān)的。該算法屬于被動(dòng)學(xué)習(xí)的范疇，對于一個(gè)比較復(fù)雜的系統(tǒng)而言，我們不可能窮盡它所有的行為抽樣，所以最終學(xué)習(xí)得到的模型和真正系統(tǒng)中的隱含模型很可能只是一個(gè)部分相交的關(guān)系。所以在使用這個(gè)算法時(shí)，為了得到一個(gè)更加精準(zhǔn)的模型，就必須使最初的抽樣覆蓋更多的系統(tǒng)特征操作。

4 學(xué)習(xí)時(shí)間自動(dòng)機(jī)的一種新方案

上面的模型學(xué)習(xí)過程有些設(shè)計(jì)到轉(zhuǎn)化的問題，將一個(gè)難以學(xué)習(xí)的自動(dòng)機(jī)模型通過一定條件制約轉(zhuǎn)化成另一種較為簡單學(xué)習(xí)的自動(dòng)機(jī)模型，然后再進(jìn)行學(xué)習(xí)處理，會讓可學(xué)習(xí)的模型種類更加寬泛。

時(shí)間自動(dòng)機(jī)是處理時(shí)間語句的自動(dòng)機(jī)模型，而寄存器自動(dòng)機(jī)是處理數(shù)據(jù)流語句的模型，兩種模型雖然有不同的含義，但是在幾個(gè)判定問題上具有相同的可判定性和復(fù)雜度結(jié)果。有研究[9]表明兩種模型之間在特殊的語句形式和同構(gòu)關(guān)系下可以產(chǎn)生相互的映射，并且能夠保持一些特性，比如確定性。這使得我們可以對于其中一個(gè)種類的給定模型，計(jì)算出另一種類的結(jié)果模型，而兩個(gè)模型的接收情況是針對特殊的語句來進(jìn)行對應(yīng)。根據(jù)這樣的思想，我們可以將這種關(guān)系應(yīng)用到對于時(shí)間自動(dòng)機(jī)的學(xué)習(xí)中來，并取得了一些進(jìn)展。通過將時(shí)間自動(dòng)機(jī)計(jì)算生成對應(yīng)的寄存器自動(dòng)機(jī)，然后針對這個(gè)寄存器自動(dòng)機(jī)進(jìn)行模型學(xué)習(xí)，然后將學(xué)習(xí)得到的寄存器自動(dòng)機(jī)模型轉(zhuǎn)化為一個(gè)時(shí)間自動(dòng)機(jī)的假設(shè)模型，最后得到的這個(gè)時(shí)間模型能夠覆蓋原本給定時(shí)間自動(dòng)機(jī)的所有行為。整個(gè)過程（見圖1）可以實(shí)現(xiàn)對原時(shí)間自動(dòng)機(jī)的行為的模仿，最終時(shí)間自動(dòng)機(jī)的滿足特殊語句形式的運(yùn)行行為路徑可以在一定條件下還原為原本時(shí)間自動(dòng)機(jī)的行為路徑。但限制在于學(xué)習(xí)過程中的教師模塊的設(shè)定較為特殊，而且最終產(chǎn)生的行為集合對原本的行為集合是一種包含關(guān)系。

5 研究方向

上面所有的學(xué)習(xí)過程大都無法保證我們得到的模型和原模型是完全等價(jià)的，一般是包含所有的原始自動(dòng)機(jī)的行為或者不能判定。而判定等價(jià)所需要的計(jì)算力是難以達(dá)到。所以一致性的測試是非常重要的一個(gè)問題。目前已知的一個(gè)可行的方案是通過輸入語句上的概率分布應(yīng)用來讓學(xué)習(xí)得到的模型更加可靠，這是一種概率近似正確的策略，能夠在保證學(xué)習(xí)結(jié)果基本可用的前提下大量減少學(xué)習(xí)過程的復(fù)雜度，缺點(diǎn)是可能對目標(biāo)系統(tǒng)有其他的限制。這種策略要考慮如何在可用性和復(fù)雜度之間取得平衡，我們?nèi)孕枰度氪罅康难芯縼斫沂酒鋵φ嬲龑?shí)際系統(tǒng)項(xiàng)目的學(xué)習(xí)效果。

另外，在實(shí)際應(yīng)用中對于不同的系統(tǒng)的情況，可以考慮制定不同的學(xué)習(xí)策略。比如在部分系統(tǒng)內(nèi)部已知的情況下，可以縮減學(xué)習(xí)模型的范圍，可認(rèn)為是白盒技術(shù)與黑盒的技術(shù)的結(jié)合使用；對于不同的系統(tǒng)還能使用不用的對應(yīng)輔助模塊，類似之前算法中涉及的映射器模塊，可能又因?yàn)橄到y(tǒng)本身特點(diǎn)的不同而呈現(xiàn)不同的特殊定制模塊來輔助整個(gè)學(xué)習(xí)過程。定制化可能成為工業(yè)化道路上的一個(gè)有效策略，但是整個(gè)學(xué)習(xí)過程的前置代價(jià)會比較大。

6 總結(jié)

本文對于模型學(xué)習(xí)的概念進(jìn)行了介紹，并對相關(guān)模型的學(xué)習(xí)算法進(jìn)行了簡述，并提出了一個(gè)時(shí)間自動(dòng)機(jī)的模型學(xué)習(xí)方法，最后提出了模型學(xué)習(xí)流程研究的現(xiàn)階段需要探索的方向。模型學(xué)習(xí)仍處于發(fā)展的階段，我們希望越來越多的學(xué)者能夠投入相關(guān)的研究工作，為模型學(xué)習(xí)的工業(yè)化提供更多的支持，這對于形式化方法的發(fā)展和軟件的有效驗(yàn)證都有非常重要的意義。

參考文獻(xiàn)：

[1] Frits Vaandrager. Model learning[J] .Communications of the ACM， 2017，（60） 2： 86-95.

[2] Dana Angluin. Learning regular sets from queries and counterexamples[J]. Information & Computation， 1987， 75（2）：87-106.

[3] Malte Isberner， Falk Howar， and Bernhard Steffen. Learning register automata：from languages to program structures. Machine Learning， 96（1-2）：65–98， 2014.

[4] Falk Howar， Bernhard Steffen， Bengt Jonsson， and Sofia Cassel. Inferring canonical register automata. In Viktor Kuncak and Andrey Rybalchenko， editors， Verification， Model Checking， and Abstract Interpretation， volume 7148 of Lecture Notesin Computer Science， pages 251–266.Springer Berlin Heidelberg，2012.

[5] F Aarts.Tomte： Bridging the Gap between Active Learning and Real-World Systems. PhD thesis， Radboud University Nijmegen， October 2014.

[6] Grinchtein O， Jonsson B， Leucker M. Learning of event-recording automata[J]. Lecture Notes in Computer Science， 2004， 3253：379-395.

[7] Grinchtein O， Jonsson B， Pettersson P. Inference of event-recording automata using timed decision trees[J]. Lecture Notes in Computer Science， 2006， 4137：435-449.

[8] Verwer S，Weerdt M D，Witteveen C.An algorithm for learning real-time automata[J].Proceedings of the BENELEARN，2007，pp.33-42.

[9] Figueira D， Hofman P ， Lasota S. Relating timed and register automata[J].Mathematical Structures in Computer Science， 2016， 26（06）：993-1021.

【通聯(lián)編輯：梁書】