软件工程中的系统文献映射研究实例-软件开发中有哪些方法和工具被用来支持假设条件管理？（第六部分）

之前的博客详细描述了软件工程中的系统文献映射研究方法。这里接着给出一个我曾经做过的工作作为例子，以更直观地展示这种研究类型。该研究的背景信息这里不再赘述。        

这篇博客主要介绍第五个研究问题的结果，即软件开发中有哪些方法和工具被用来支持假设条件管理。

下表列出识别的假设条件管理方法，并按假设条件管理活动分类。注意并非每个假设条件管理活动均有方法支持，且一个方法可能用于支持一个或多个假设条件管理活动。其次，只有入选文献明确说明某方法如何支持某假设条件管理活动，才会在下表中列出。例如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.