軟體工程中的系統文獻映射研究執行個體-軟體開發中有哪些方法和工具被用來支援假設條件管理？（第六部分）

之前的部落格較長的描述了軟體工程中的系統文獻映射研究方法。這裡接着給出一個我曾經做過的工作作為例子，以更直覺地展示這種研究類型。該研究的背景資訊這裡不再贅述。        

這篇部落客要介紹第五個研究問題的結果，即軟體開發中有哪些方法和工具被用來支援假設條件管理。

下表列出識别的假設條件管理方法，并按假設條件管理活動分類。注意并非每個假設條件管理活動均有方法支援，且一個方法可能用于支援一個或多個假設條件管理活動。其次，隻有入選文獻明确說明某方法如何支援某假設條件管理活動，才會在下表中列出。例如assume-guarantee reasoning也可支援假設條件的維護。但部分描述assume-guarantee reasoning的相關文獻中并未明确關聯假設條件的維護。是以此類文獻不會被分類到“假設條件維護”類别中。

注：總共有134篇入選文獻。

方法	數量（%）
假設條件制定	62 (46.3%)
假設條件描述	65 (48.5%)
假設條件評價	40 (29.9%)
假設條件維護	11 (8.2%)
假設條件追溯	5 (3.7%)
假設條件監視	3 (2.2%)
假設條件恢複	1 (0.7%)

以下舉例說明某方法如何支援假設條件管理活動。

1. 假設條件制定和評價

根據此系統文獻映射研究的結果，最具代表性的假設條件制定和評價的方法為assume-guarantee reasoning。若需要驗證某系統是否滿足某屬性，assume-guarantee reasoning将系統分解為構件（規模較小且更易于驗證）；為其中一個構件生成假設條件以滿足該屬性；并檢查其他構件是否滿足生成的假設條件；最後得到結果。目前存在多種對assume-guarantee reasoning的解釋，此處提供兩個例子。在文獻[1]中，作者指出一般的assume-guarantee規則為：（a）将一個系統分解為M1和M2兩個構件；（b）為M1生成一個假設條件使其滿足需要被滿足的屬性；（c）将該假設條件應用于M2的環境。若結果為真，則得出系統滿足該屬性。在文獻[2]中，作者描述assume-guarantee reasoning的過程為：（a）為系統中的一個構件的環境制定一個假設條件，且此假設條件關于該構件期望的行為；（b）基于該假設條件構造構件的環境；（c）檢查整個系統以确定在該假設條件的基礎上，構件是否滿足其期望的行為而無錯誤。

2. 假設條件描述

現存多種描述假設條件的方法，如文檔、語言、架構、模型、圖、接口、協定、人物角色、類比。在文獻[3]中，作者将假設條件的描述內建至構件模闆中，包括構件假設條件和接口假設條件。在文獻[4]中，作者采用Semantic Web Rule語言來描述假設條件。在文獻[5]中，作者提出假設條件歸檔方法。該方法采用自然語言并聚焦于假設條件如何與需求關聯，且哪些假設條件未被使用。

3. 假設條件維護

在部分assume-guarantee reasoning方法中（如[1][6][7]），評價假設條件後，存在精化未滿足的假設條件的步驟。在文獻[4]中，作者提出假設條件維護的架構（如修改失效的假設條件）。在文獻[8]中，作者在構件和接口的維護中，提出一個有四個步驟的假設條件維護過程。

4. 假設條件追溯

大部分假設條件追溯的方法（5篇文獻中的4篇；80%）用于假設條件和需求追溯。在文獻[9]中，作者提出假設條件、需求、代碼追溯的方法，且該方法可展示哪些需求可能與假設條件關聯。在文獻[10]中，作者同樣追溯假設條件和需求。但他們聚焦于可信的假設條件和安全性需求之間的關系。在文獻[11]中，作者提出采用目标模型以追溯假設條件和需求。該目标模型包括三個部分：目标、領域假設條件、目标和假設條件之間的關系。

5. 假設條件監視

在文獻[12]中，作者在運作時需求模型中提出假設條件監視的方法（使用目标和目标模型）。在文獻[13]中，作者讨論假設條件監視的意義（如其可被用于運作時假設條件的評價），并提出相關方法。該方法可生成關于假設條件的日志。

6. 假設條件恢複

在文獻[14]中提出的假設條件恢複方法采用五種來源以探測可疑的事物：自由通路、财務報告、文檔、版本控制、代碼，并通過引導的通路來識别假設條件。

在入選文獻中識别出34種工具。其中超過半數的工具（34種工具中的19種；55.9%）用于支援assume-guarantee reasoning。如下表所示，本研究将這些工具分為兩類：Assume-guarantee reasoning和其他。注意表中的連結、開發者、開源的相關資訊不僅來源于入選文獻，也來源于網絡。表中的“未知”表示無法找到相關資訊。

（1）Assume-guarantee reasoning

此類型下的工具用于支援assume-guarantee reasoning的方法。例如在文獻[15]中，為支援作者提出的方法（如假設條件學習架構），作者開發了LTSA (Labelled Transition System Analyzer)工具。

工具	連結	開發者	開源
LTSA (Labelled Transition System Analyzer)	http://www.doc.ic.ac.uk/ltsa/	學術界	未知
NuSMV model checker	http://nusmv.fbk.eu/	學術界	是
Java PathFinder	http://javapathfinder.sourceforge.net/	工業界	是
SPIN model checker	http://spinroot.com/spin/whatispin.html	學術界	是
AG tool	未知	學術界	未知
AR tool	未知	學術界	未知
SpaceEx (a symbolic hybrid model checker)	http://spaceex.imag.fr/	學術界	是
BEG (Bandera Environment Generator) New name: Open Components and Systems Environment Generator (OCSEGen)	https://forge.cis.ksu.edu/projects/beg/ https://code.google.com/archive/p/envgen/	學術界	是
BPC Checker (Behavior Protocol Model Checker)	未知	未知	未知
EnvGen (Environment Generator for Java PathFinder)	未知	學術界	是
SPARK (a prototype tool in Python)	http://www.altran.co.uk/	工業界	未知
SGM (State-Graph Manipulators)	https://www.cs.ccu.edu.tw/~pahsiung/sgm/ http://embedded.cs.ccu.edu.tw/~esl_web/Project/Ch/SGM/	學術界	未知
SafetyADD	http://vedder.se/SP/SafetyAddDraft.pdf	學術界	未知
LUTE checker	未知	未知	未知
AGREE	未知	未知	未知
KIND model checker	http://clc.cs.uiowa.edu/Kind/	學術界和工業界	是
An automatic checking tool	未知	學術界	未知
Cadence SMV	http://www.kenmcmil.com/smv.html	學術界	是
SAT solver	未知	工業界	未知

（2）其他

此類型下的工具用于支援具體的假設條件管理活動。在文獻[16]中，作者開發了AREL工具以支援設計原理的識别以及對假設條件和其他元素的追溯（如設計決策）。在文獻[17]中，OCRA工具被主要用于基于構件的設計，但也可支援假設條件的描述。

工具	假設條件管理活動	連結	開發者	開源
Alloy analyzer	描述、評價	http://alloy.mit.edu/alloy/	學術界	未知
OCRA (Othello Contracts Refinement Analysis)	描述	https://es-static.fbk.eu/tools/ocra/	學術界	未知
A prototype tool	制定、描述	http://people.cs.kuleuven.be/~dimitri.vanlanduyt/eaa/	學術界	是
Drools (a Business Rules Management System)	制定、描述、評價	https://www.drools.org/	工業界	是
PicoSAT (an SAT solver)	制定、描述、評價	http://fmv.jku.at/picosat/	學術界	是
Microsoft threat modeling tool	描述	https://www.microsoft.com/en-us/download/details.aspx?id=49168	工業界	未知
Redhat’s RPM	描述	https://www.redhat.com/en	工業界	是
Debian’s APT	描述	https://www.debian.org/index.en.html	工業界	是
XML-based engine (a tool with an XML back-end)	描述、評價	未知	學術界	未知
PAT (Process Analysis Toolset)	描述、評價	未知	未知	未知
SCENARIOTOOLS (an Eclipse-based tool)	描述	http://scenariotools.org/	學術界	是
GASR (General-purpose Aspectual Source Code Reasoner)	評價	https://github.com/cderoove/damp.ekeko.aspectj	學術界	是
AREL (Architecture Rationale and Elements Linkage)	追溯	http://www.ict.swin.edu.au/personal/atang/AREL-Tool.zip	學術界	未知
MAVEN (Modular Aspect Verification)	描述、評價	未知	學術界	未知
CAIRIS (Computer Aided Integration of Requirements and Information Security)	未知	https://github.com/failys/CAIRIS	學術界	是

參考文獻

[1] M.G. Bobaru, C.S. Păsăreanu, and D. Giannakopoulou. Automated assume-guarantee reasoning by abstraction refinement. In: Proceedings of the 20th International Conference on Computer Aided Verification (CAV), Princeton, NJ, USA, pp. 135-148, 2008.

[2] P. Parizek and F. Plasil. Assume-guarantee verification of software components in sofa 2 framework. IET Software, 4(3): 210-211, 2010.

[3] P. Lago and H. van Vliet. Observations from the recovery of a software product family. In: Proceedings of the 3rd International Conference on Software Product Lines (SPLC), Boston, MA, USA, pp. 214-227, 2004.

[4] Z. Lu, S. Li, A. Ghose, and P. Hyland. Extending semantic web service description by service assumption. In: Proceedings of the 2006 IEEE/WIC/ACM International Conference on Web Intelligence (WI), Hong Kong, China, pp. 637-643, 2006.

[5] E. Denney and B. Fischer. A verification-driven approach to traceability and documentation for auto-generated mathematical software. In: Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering (ASE), Auckland, New Zealand, pp. 560-564, 2009.

[6] J.M. Cobleigh, D. Giannakopoulou, and C.S. Păsăreanu. Learning assumptions for compositional verification. In: Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS), Warsaw, Poland, pp. 331-346, 2003.

[7] A. Komuravelli, C.S. Păsăreanu, and E.M. Clarke. Assume-guarantee abstraction refinement for probabilistic systems. In: Proceedings of the 24th International Conference on Computer Aided Verification (CAV), Berkeley, CA, USA, pp. 310-326, 2012.

[8] S. Bauer, R. Hennicker, and A. Legay. A meta-theory for component interfaces with contracts on ports. Science of Computer Programming, 91(10): 70-89, 2014.

[9] E. Denney and B. Fischer. A verification-driven approach to traceability and documentation for auto-generated mathematical software. In: Proceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering (ASE), Auckland, New Zealand, pp. 560-564, 2009.

[10] C.B. Haley, R.C. Laney, J.D. Moffett, and B. Nuseibeh. Using trust assumptions with security requirements. Requirements Engineering, 11(2): 138-151, 2006.

[11] C. Liu, W. Zhang, H. Zhao, and Z. Jin. Analyzing early requirements of cyber-physical systems through structure and goal modeling. In: Proceedings of the 20th Asia-Pacific Software Engineering Conference (APSEC), Bangkok, Thailand, pp. 140-147, 2013.

[12] R. Ali, F. Dalpiaz, P. Giorgini, and V.E.S. Souza. Requirements evolution: from assumptions to reality. In: Proceedings of the 12th International Conference on Enterprise, Business-Process and Information Systems Modeling (BPMDS), London, UK, pp. 372-382, 2011.

[13] A. Nhlabatsi, Y. Yu, A. Zisman, T. Tun, N. Khan, and A. Bandara. Managing security control assumptions using causal traceability. In: Proceedings of the 8th International Symposium on Software and Systems Traceability (SST), Florence, Italy, pp. 43-49, 2015.

[14] R. Roeller, P. Lago, and H. van Vliet. Recovering architectural assumptions. Journal of Systems and Software, 79(4): 552-573, 2006.

[15] C.S. Păsăreanu, D. Giannakopoulou, M.G. Bobaru, J.M. Cobleigh, and H. Barringer. Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Methods in System Design, 32(3): 175-205, 2008.

[16] A. Tang, Y. Jin, and J. Han. A rationale-based architecture model for design traceability and reasoning. Journal of Systems and Software, 80(6): 918-934, 2007.

[17] T. Arts, M. Dorigatti, and S. Tonetta. Making implicit safety requirements explicit. In: Proceedings of the 33rd International Conference on Computer Safety, Reliability, and Security (SAFECOMP), Florence, Italy, pp. 81-92, 2014.