系列簡介：形式化方法在計(jì)算機(jī)和軟件工程學(xué)科中作為一個(gè)學(xué)科分支，正在越來越多地進(jìn)入工業(yè)界諸多實(shí)踐領(lǐng)域。以DO-333適航標(biāo)準(zhǔn)為代表的工業(yè)標(biāo)準(zhǔn)，亦對軟件開發(fā)過程明確提出了采用形式化方法的要求。為此，結(jié)合上海控安形式化方法技術(shù)團(tuán)隊(duì)歷年來在航空、航天和軌交等領(lǐng)域的成功應(yīng)用經(jīng)驗(yàn)，本專題將圍繞“形式化方法”特別是形式化方法的工程化應(yīng)用，組織一系列文章，探討形式化方法背后的動因和關(guān)鍵技術(shù)及行業(yè)應(yīng)用。

01

傳統(tǒng)軟件工程面臨的困難

自從1968年“軟件工程”這個(gè)學(xué)科概念提出以來，軟件工程的研究和實(shí)踐有效地解決了軟件的質(zhì)量和研制效率問題。但是傳統(tǒng)軟件工程中存在的大量依賴人工的活動和主觀性判斷等過程和技術(shù)，給軟件帶來了日趨明顯的可信問題。我們以工業(yè)領(lǐng)域最常見的 “V”字模型為例探討傳統(tǒng)軟件工程中的一些局限性。

圖1 常見于工業(yè)標(biāo)準(zhǔn)的V字模型

按照V模型的軟件開發(fā)過程，我們可以看到，即使是工業(yè)界較為推崇的V模型，其描述的軟件研制過程仍然存在明顯的局限性和風(fēng)險(xiǎn)：

（1）軟件研制過程中文檔的準(zhǔn)確性

軟件需求普遍以自然語言來撰寫需求文檔。由于自然語言天然的二義性和模糊性，造成文檔難以精確描述軟件預(yù)期功能和性能。設(shè)計(jì)文檔采用圖形化描述，往往缺乏嚴(yán)格的語法和語義。此類中間產(chǎn)物的缺陷往往持續(xù)傳遞至代碼和測試階段，部分深層次問題幾乎始終無法探測。

（2）軟件研制過程對主觀活動的依賴性

軟件研制過程中，各階段的轉(zhuǎn)換及產(chǎn)物之間的一致性，嚴(yán)重依賴人工判斷。例如設(shè)計(jì)文檔是否與需求文檔中功能和行為描述一致，往往通過人工審查和比對來進(jìn)行。

（3）軟件研制過程的嚴(yán)謹(jǐn)性

軟件研制過程中的中間產(chǎn)物，缺乏嚴(yán)格分析手段。例如，自然語言撰寫的需求文檔難以被嚴(yán)格分析。設(shè)計(jì)文檔刻畫的系統(tǒng)架構(gòu)，通過簡單的仿真進(jìn)行而缺少對系統(tǒng)行為深層次的驗(yàn)證，例如死鎖等安全隱患難以揭示。

盡管業(yè)界和學(xué)術(shù)界在軟件工程理論和實(shí)踐中取得了豐碩成果，軟件質(zhì)量問題始終是行業(yè)的一大難題。2017年11月28日 俄羅斯“聯(lián)盟-2.1B”火箭發(fā)射失敗，軟件錯誤導(dǎo)致19顆衛(wèi)星燒毀。波音737MAX機(jī)型的控制軟件對人機(jī)控制優(yōu)先級的錯誤設(shè)計(jì)，導(dǎo)致2018年和2019年兩次惡性墜機(jī)事件。

隨著軟件產(chǎn)品對社會生產(chǎn)生活的重要性日趨上升，如何改善并發(fā)展現(xiàn)有的軟件工程方法，使其能對軟件的安全可信提供更為可靠的保障，成為了工業(yè)界和學(xué)術(shù)界普遍關(guān)心的問題。在此背景下，形式化方法以其嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)理論基礎(chǔ)和不斷發(fā)展的技術(shù)手段，被視為一種極有潛力的解決方案。

02

形式化方法發(fā)展歷史

在20世紀(jì)60年代，F(xiàn)loyd、Hoare和Manna等試圖用數(shù)學(xué)方法來證明程序的正確性并發(fā)展成了各種程序驗(yàn)證方法。隨后軟件工程界認(rèn)識到了數(shù)學(xué)方法的巨大潛力，形式化方法一詞開始傳播開來。1969-1972年之間， C.A.R Hoare撰寫了"計(jì)算機(jī)編程的公理基礎(chǔ)"和"數(shù)據(jù)表示的正確性證明"兩篇開創(chuàng)性的論文，并提出了規(guī)格說明的概念。

在形式語義與形式化建模以及形式化規(guī)約的基礎(chǔ)上，將計(jì)算機(jī)系統(tǒng)的分析與驗(yàn)證問題轉(zhuǎn)化為邏輯推理問題或者形式模型的判斷問題，用定理證明工具/求解器或者某個(gè)形式模型的原型工具來進(jìn)行驗(yàn)證。交互式定理證明需要用戶與計(jì)算機(jī)相互協(xié)助來進(jìn)行形式化證明。最常用的證明輔助是Coq和Isabelle，均有在空客等航空領(lǐng)域項(xiàng)目中成功應(yīng)用的記錄。

模型檢驗(yàn)的基本思想是通過遍歷系統(tǒng)的狀態(tài)空間以驗(yàn)證系統(tǒng)模型是否滿足給定的關(guān)鍵性質(zhì)，并在不滿足性質(zhì)時(shí)給出具體反例路徑。例如在航空等安全攸關(guān)領(lǐng)域，常用于分析系統(tǒng)是否滿足給定的功能需求或安全性質(zhì)。較有代表性的工具包括SPIN、UPPAAL和 PRISM等，在工業(yè)界尤其是在硬件系統(tǒng)的分析與驗(yàn)證上取得了很大的成功。

關(guān)于形式化驗(yàn)證的定理證明、模型檢測等方法，特別是在軌交、航空、航天和汽車電子及工業(yè)控制等行業(yè)的成功應(yīng)用以及相關(guān)工具的研發(fā)，我們將在后續(xù)的文章中作更為深入和系統(tǒng)化的探討。

03

形式化方法的簡介

形式化方法(Formal Methods)是一種基于數(shù)學(xué)的開發(fā)軟件系統(tǒng)的方法學(xué)，它提供了一種數(shù)學(xué)化的框架，在此框架之下開發(fā)者可以通過定義系統(tǒng)和驗(yàn)證系統(tǒng)的方式，以系統(tǒng)化的手段逐步開發(fā)軟件。

從廣義上講，形式化方法是指將離散數(shù)學(xué)的方法用于解決軟件工程領(lǐng)域的問題，主要包括建立精確的數(shù)學(xué)模型以及對模型的分析活動。狹義地講，形式化方法是運(yùn)用形式化語言，進(jìn)行形式化的規(guī)格描述、模型推理和驗(yàn)證的方法。

通常來說，形式化方法強(qiáng)調(diào)了對軟件預(yù)期功能和行為的“描述（specify）”和“驗(yàn)證（verify）”。描述強(qiáng)調(diào)通過精確的形式化語言刻畫軟件，驗(yàn)證則強(qiáng)調(diào)通過數(shù)學(xué)手段嚴(yán)格地分析軟件是否是一致的、是否滿足給定的性質(zhì)等。由此我們可以認(rèn)為，形式化方法包含兩項(xiàng)目主要分支，形式化規(guī)格說明技術(shù)和形式化驗(yàn)證技術(shù)。這兩種技術(shù)都是基于數(shù)學(xué)基礎(chǔ)，例如集合論、邏輯和代數(shù)理論等，如圖3所示。

圖3 形式方法的構(gòu)成

形式化規(guī)格說明技術(shù)可以視為一種對軟件形式化建模的過程。一般來說，形式化建模需要有特定的形式化語言，此類語言基本上可以分為下述類型：

基于模型的語言

此類形式化語言基本思想是利用一些已知特性的數(shù)學(xué)抽象來為目標(biāo)軟件系統(tǒng)的狀態(tài)特征和行為特征構(gòu)造模型，包括域、元組、集合等。Z、VDM，B等都是面向模型的語言。

代數(shù)方法語言

代數(shù)方法僅使用帶有等詞的一階邏輯的表示，而不引入通常的數(shù)學(xué)對象。常見的代數(shù)方法有Larch等。

進(jìn)程代數(shù)語言

進(jìn)程代數(shù)提供了描述并發(fā)系統(tǒng)所需的并行復(fù)合，選擇，順序復(fù)合等語句。并可通過等式推理（equatioanl reasoning）的方法來驗(yàn)證系統(tǒng)滿足某些性質(zhì)。常見的進(jìn)程代數(shù)語言有CSP等。

形式化驗(yàn)證就是基于已建立的形式化規(guī)格說明的基礎(chǔ)上，對所描述系統(tǒng)的相關(guān)性質(zhì)進(jìn)行分析以評判系統(tǒng)是否滿足期望的性質(zhì)，盡可能地發(fā)現(xiàn)其中的不一致性、模糊性、不完備性等錯誤。形式化驗(yàn)證的主要技術(shù)包括定理和模型檢測。

定理證明技術(shù)是形式方法的核心，定理證明系統(tǒng)是由一個(gè)形式語言和推理機(jī)制構(gòu)成的形式系統(tǒng)。推理機(jī)制由公理和推理規(guī)則組成。通常的定理證明過程需要工具的支持。使用定理證明技術(shù)，我們可以對用戶期望的或系統(tǒng)應(yīng)具有的性質(zhì)進(jìn)行證明，以消除規(guī)格說明中的模糊性、不一致性、不安全性等。

模型檢測是一種自動驗(yàn)證系統(tǒng)正確性的方法。模型檢測器的輸入通常是一個(gè)系統(tǒng)的有限狀態(tài)模型以及一組用時(shí)態(tài)邏輯表達(dá)的系統(tǒng)預(yù)期的性質(zhì)。通過搜索有限狀態(tài)模型所有的可能事件序列來判定系統(tǒng)性質(zhì)是否得到滿足。由于系統(tǒng)的模型是有限的，因此系統(tǒng)狀態(tài)空間的搜索能終止。假如系統(tǒng)的性質(zhì)成立，則模型檢測器輸出一個(gè)肯定結(jié)果。如果性質(zhì)不滿足，則系統(tǒng)輸出一個(gè)以狀態(tài)序列表示的反例。

一個(gè)最簡單的例子：

假如在一個(gè)飛行器中有一款控制軟件，需要完成飛行控制行為。其中某條功能為“求一個(gè)給定正數(shù)的非負(fù)數(shù)平方根”。我們用形式化語言Z來描述這條軟件功能，如圖4所示。

圖4 模式SquareRootSpec

其中的E形框稱為模式框架 (Schema Box)，可以近似看作一個(gè)“操作”，頂部的標(biāo)識符 SquareRootSpec 稱為模式名稱，中間水平線起分隔作用，水平線上部稱為聲明部分，水平線下面是謂詞部分，由若干個(gè)謂詞組成，這些謂詞通過聯(lián)結(jié)詞“∧”形成一個(gè)完整的謂詞。該例中將radicand? 和squareroot! 都聲明為實(shí)數(shù)類型，分別為輸入變量和輸出變量。

從這個(gè)例子可以看出，形式化語言刻畫軟件功能時(shí)，更多地是通過一種數(shù)學(xué)上的“抽象”來精確描述待開發(fā)的軟件。在這個(gè)例子里，求平方根的細(xì)節(jié)過程并不是重點(diǎn)要刻畫的對象，而是通過“squareroot!2= radicand?”這個(gè)等式來表達(dá)一種“關(guān)系”，即“待求的非負(fù)數(shù)平方根，其平方一定等于被開方數(shù)”。對于軟件來說，這種關(guān)系是必然的、唯一的，而代碼實(shí)現(xiàn)求解的方式則是多樣的。

上面這個(gè)例子里，若我們把Z語言撰寫的模式看作是一個(gè)“軟件需求的形式化描述”，那么我們就可以對這個(gè)形式化的需求做進(jìn)一步的分析驗(yàn)證。假定，我們想表達(dá)的是“求一個(gè)給定正數(shù)的非負(fù)數(shù)平方根”，但是寫需求的人員，誤將要輸出的非負(fù)數(shù)平方根變量squareroot!寫成了負(fù)數(shù)平方根，即整個(gè)謂詞部分變成了“radicand?≥0 ∧ squareroot! 2= radicand? ∧squareroot!<0”。此時(shí)我們該如何發(fā)現(xiàn)這個(gè)缺陷呢？

假定需求分析過程中，我們還有一位需求檢查者。檢查者可以通過數(shù)學(xué)證明的方式來發(fā)現(xiàn)這個(gè)缺陷。例如，檢查者可以在謂詞表達(dá)式之后插入一個(gè)斷言“squareroot! ≥0”。此時(shí)，謂詞表達(dá)式應(yīng)該滿足這個(gè)斷言。

通過數(shù)學(xué)證明的方式，顯然可以發(fā)現(xiàn)，“radicand?≥0 ∧ squareroot! 2= radicand? ∧squareroot!<0”是無法推出“squareroot! ≥0”的，即原先撰寫的謂詞與給定的斷言相矛盾。

上面的例子是一個(gè)非常簡單的示例，僅用于說明最簡單的形式化描述和分析過程。在我們后續(xù)的推文中，我們將陸續(xù)深入闡釋形式化建模和形式化驗(yàn)證的相關(guān)技術(shù)以及其行業(yè)應(yīng)用。

審核編輯：符乾江