3.1.2　基于形式規約語言

在基于形式規約語言的嵌入式軟件建模及測試技術中，有代表性的是RTRSM、CSP、TCSP、Z語言、TTCN-3語言和ATLAS語言等。實時嵌入式軟件的建模應當支持事件驅動、狀態遷移描述、復雜動態交互行為和嚴格時間限制等領域特征。

嵌入式軟件系統的需求建模規約語言RTRSM（Real-time Requirements Specification Model）以擴充的層次并發有窮狀態機HCA為核心，以支持合成的模板為基本組成單元，利用轉換有效期和事件預定機制來描述時間限制，具有較強的時間限制描述能力，能自然而直接地支持交互行為的建模，可執行且具有良好的形式語義。RTRSM通過模板來支持系統的分解，其具體表現形式為包括接口和數據定義的表格以及與狀態圖等價的形式化的規則集。

CSP（Communication Sequences Processes，通信序列進程）是Hoare于1978年提出的一種能夠對具有并發關系的系統進行建模的形式化語言，它基于順序通信，主要通過進程事件的集合和進程的軌跡來描述進程的行為，可以通過并發、選擇、遞歸等來描述進程之間的關系。在CSP的基礎上加入時間因素形成TCSP（Timed CSP，時間通信序列進程）描述語言。這種語言具有良好的形式化基礎，語法語義定義良好，對帶時間的并發進程的表達清晰簡潔。

Z語言是由英國牛津大學程序研究組（Programming Research Group，PRG）開發設計的。Z本身是一個書寫規格說明的語言，或者說是一種表示方法。IBM公司利用Z語言對其用戶信息控制系統（CICS）進行規格說明的重寫并獲得了成功，使軟件開發費用降低了9%，對Z語言產生了極大的影響。Z語言是基于一階謂詞邏輯和集合論的形式規格說明語言，具有精確、簡潔、無二義等優點，有利于保證程序的正確性，尤其適合無法進行現場調試的高安全性系統的開發。它的另一個主要特點是可以對Z規格說明進行推理和證明，這種特點使得軟件開發人員或用戶能夠很快找出規格說明的不一致、不完整之處，從而提高軟件開發的效率。隨著技術的不斷發展，出現了Z的一些擴展語言，如Object-Z和Real-Time Object-Z等。一種基于Z規格說明的軟件測試用例自動生成技術如圖3-2所示，其具體做法是：通過對軟件Z規格說明的分析，找出描述軟件輸入、輸出的線性謂詞；將上述線性謂詞轉換成相應的線性不等式組，并求解該線性不等式組得到相應的區域邊界頂點；找出區域邊界附近的點，經過輸入、輸出逆變換得到測試用例。此外，還有利用Z規格說明進行軟件測試和度量的方法，但該方法需測試人員具有豐富的測試經驗和深厚的數學基礎才能完成，而且由于是手工測試，測試的效率比較低。由于Z語言基于數學的概念，過于抽象、簡明，因此用它編寫的形式規格說明過于抽象、難懂，而軟件開發和測試人員習慣于非形式方法，缺少基于形式方法的訓練。由于Z語言尚缺乏自動化工具的支持，且基于Z語言的形式規格說明的正確性證明費時費力，因此限制了其工程應用。

圖3-2　基于Z語言的測試用例自動生成

TTCN-3（Testing and Test Control Notation 3）是一種基于文本的測試描述語言，它由TTCN（Tree and Tabular Combined Notation）改進、擴展而來，在形式方面有較大改進，內容方面統一了原來混亂的概念和定義，簡化了表示方法。TTCN-3適用于各種交互系統的描述，目前已廣泛應用于協議測試、Web服務測試和基于CORBA的平臺測試等領域。當前測試領域主要對TTCN-3采用圖形表示，然后將圖形轉換為代碼描述；圖形通過MSC（Message Sequence Chart）來表示，通過MSC能很好地表達系統與其交聯環境的通信行為。TTCN-3通過模塊來完整描述測試套件，模塊包括定義部分和操作部分，定義部分給出測試組件、測試端口、數據類型、變量、常量、函數以及測試用例，控制部分則進行一些局部定義以及調用測試用例并控制其執行順序。通過基本的MSC圖可以描述測試用例中表示的測試動作，而通過HMSC（High-Level MSC）可在更高的層次上組織這些基本MSC表示的測試用例。上述分層次的表示方法可以很好地表達較為復雜的測試過程，圖3-3給出了構建一個TTCN-3測試套件的思路。

圖3-3　TTCN-3測試套件建立思路

ATLAS語言是國際測試標準ABBET（廣域測試環境）和SMART（標準的模塊式航空電子設備維修與測試）定義的UUT描述語言。它采用面向信號的描述方式，描述了UUT的測試需求在特定的ATS上解釋執行的過程。

ATLAS有兩個較為成熟的版本，ARINCStd626（由ARINC領導，1976年發布）和IEEEStd716（由IEEE設立的SCC20（Standard Coordinating Committee 20）領導，1985年發布）。隨著在工程應用中的實踐，ATLAS給出了一種面向信號設計ATS的有效方式，但也暴露了很多問題，比如：

·版本變化太多，不同版本之間發生了顯著的變化；

·語言過于冗長，關鍵字過多；

·語言的更新周期長，跟不上需求的變化和新技術發展的步伐；

·開發工具昂貴，培訓費用高，支持文檔少；

·隨著新技術的不斷引入，ATLAS體系變得龐大、雜亂，出現了信號定義模糊、相似信號的屬性難以區分、同一術語重復定義、關鍵字定義重復等問題。

上述問題限制了ATLAS的進一步發展，SCC20意識到這個問題，開始把各種軟件新技術應用到ATLAS的升級版本中，對ATLAS進行變革，推出了ATLAS2000。ATLAS2000是多層次結構的語言，其基礎由內核和原語組成，用于創建測試應用需求。ATLAS2000語言體系的模塊化結構能夠封裝可復用的測試單元，這樣的結構使用戶能夠開發和描述基于底層單元的復雜測試需求。