文 |黛月白
编辑 |黛月白
引言
驱动的软件工程和形式验证是当今软件开发领域中备受关注的重要主题，通过将驱动原则应用于软件开发过程中，并结合形式验证技术，可以提高软件系统的可靠性和安全性，同时，基于ACOhg-live算法的策略改进与性能比较实验也成为研究人员关注的焦点。
搜索驱动的软件工程及其在形式验证中的应用
驱动的软件工程是一门研究领域，目的在于利用搜索方法来解决软件工程中的各种问题。这些搜索方法包括群体智能和元启发式算法，它们基于分布式、多智能体和集体智能的思想，能够高效地找到更优的解决方案。
尽管搜索驱动的软件工程可以应用于多个研究主题，例如软件设计和重构，但其中最具潜力的领域之一是形式验证，形式验证是一种通过形式化的方法，来验证软件系统的正确性和安全性的过程，搜索驱动的软件工程可以通过搜索方法来寻找最优的验证策略，从而提高形式验证的效率和效果。
形式验证是一种数学方法，用于证明或否定软件系统的正确性，重点介绍模型检测，该方法可以自动验证软件系统的行为方面，在模型检测中，目标系统的重要行为描述称为模型，系统的期望属性以规范的形式书写。
模型检测假设模型和规范由用户给定，然后判断模型是否满足规范，该问题可以简化为对由模型，和规范构建的状态空间进行穷举搜索，如果模型检测工具得出结论，即模型不满足规范，它将输出一个违规行为，即一个反例。
模型检测存在两个主要的研究挑战，状态爆炸问题和生成易理解和简短反例的问题，状态爆炸是一个与验证效率相关的问题，状态空间往往非常庞大，并发和多处理系统中的状态数量，往往随着组件进程数量的线性增加而呈指数增长。
状态爆炸问题认为，由于经典的穷尽算法耗尽了计算资源，巨大的状态空间使得模型检测在实践中变得不可行，另一方面，生成易理解的反例是一个与可用性相关的问题，反例提供了诊断信息，帮助人类用户轻松理解规范的违反情况。
获得简短的反例比获得冗长的反例更为有利，这些问题之间存在权衡关系，当想要一个简短的反例时，需要进行穷举搜索，但这会导致状态爆炸，需要寻求一种搜索算法，以在效率和反例简短性之间取得最佳平衡。
为了缓解这些问题并实现适当的平衡，研究人员积极开发利用群体智能，和元启发式算法的非穷举验证技术，其中一种算法是蚁群优化，ACO能够有效地解决最短路径搜索问题，ACOhg是ACO的一个变种，并且适用于具有庞大状态空间的模型检测。
两种新颖的探索策略，旨在提高ACOhg-live的性能，分别称这两种策略为跳过策略和替换策略，通常对于大的状态空间，需要探索许多状态才能到达目标状态。
基于这一思想，所提出的策略采用简单的随机方法，来实现对许多状态的有效和高效探索，通过进行比较实验，确认所提出的策略相对于，ACOhg-live在效率和反例简短性之间，改善了平衡性。
经典的自动机理论模型检测，采用基于深度优先搜索的穷举搜索算法，例如Nested DFS和Tarjan算法，由于状态爆炸问题，这些经典方法很难生成简短的反例，近期的工作尝试充分利用多核处理器的能力以提高效率。
Schuppan和Biere研究了从自动机构造的角度生成简短反例，但代价是增大状态空间，模型检测的另一个研究方向是，使用启发式搜索来提高检测效率，有向模型检测研究了用于模型检测的启发式方法。
还提出了一些随机算法，例如带有随机回溯的DFS和Vagabond算法，Swarm verification并行化了多个搜索策略，包括随机化方法，自上世纪90年代以来，形式验证的元启发式方法一直受到研究。
遗传算法是一种开创性的方法，已经得到了深入研究，除了ACOhg之外，还提出了基于ACO的几种技术，其他研究采用了粒子群优化、分布估计算法、贝叶斯优化算法和蒙特卡洛树搜索。
采用模拟退火方法，并通过比较实验证明了元启发式方法，在模型检验中优于传统的确定性方法，为了提高模型检验的效率，一些研究采用了混合方法，结合了多种搜索方法，研究人员将引力搜索和PSO进行了混合。
将人工蜂群算法与SA结合使用，以及将ACOhg与随机后向搜索结合使用，上述研究充分证明了启发式，和元启发式方法在模型检验中的有效性，重点介绍ACOhg方法，旨在改善模型检验中效率和可理解性之间的平衡。
基于ACOhg-live的策略改进与性能比较实验
对原始的ACOhg-live和使用提出的策略修改后的，ACOhg-live进行了性能比较实验，并使用了两个基准测试，使用Python 3.6从头开始实现了运行ACOhg-live，和提出的策略的原型工具，模型和规范被输入为标记迁移系统。
LTSs适用于描述并发状态转换系统的事件序列，为了使原型工具高效，实现了即时检查，根据需要创建状态空间，工具输出一个事件序列作为反例，如果发现违规行为，否则输出特殊值None，即Python内置的特殊值。
准备了两个基准测试，第一个基准测试是一个数据库环系统，基准测试描述了一个由多个通信节点组成的分布式数据库，这些节点组织成一个环形网络，每个节点从其相邻节点之一接收更新信息，并更改其内部存储的数据。
节点将信息通知其他相邻节点，以保持网络的一致性，准备了三个规范，称为Spec. A、B和C，这些规范与所有节点成功更新其内部状态的要求相关，另一个基准测试是由随机图组成的模型，生成了五个Erdős-Rényi图，其中节点数为20，创建边的概率为0.1。
然后将这些图转换为LTSs，将LTSs视为组件进程，按照这个过程生成了规范的另一个Büchi自动机，这次随机选择了一些状态作为接受状态，设置了以下搜索条件，并对每个规范和实验条件运行原型30次。
OR，运行不使用提出的策略的原始ACOhg-live，ORT，将原始ACOhg-live的第一阶段终止条件对应为到达时停止的条件，并运行它，以评估在公平终止条件下的策略，SK，在第一阶段应用均匀分布的跳过策略。
SF，在第一阶段应用由公式定义的，加权概率和前向索引的跳过策略，SB，在第一阶段应用由公式定义的，加权概率和后向索引的跳过策略，RE，在第二阶段应用替换策略，RET，将原始ACOhg-live的，第一阶段终止条件对应为到达时停止的条件，并在第二阶段应用替换策略。
HY，分别在第一和第二阶段应用均匀分布的，跳过策略和替换策略，HF，分别在第一和第二阶段，应用由公式定义的加权概率，和前向索引的跳过策略和替换策略，HB，分别在第一和第二阶段应用，由公式定义的加权概率，和后向索引的跳过策略和替换策略。
对于每个实验条件，测量了检测到的反例的长度、运行时间和内存消耗，反例的长度评估了可理解性问题，运行时间和内存消耗评估了状态爆炸问题的处理效率，使用了ACOhg-live的参数设置。
选择了这个配置，以调整之前建立的研究，ACOhg被认为结合了启发式方法，在实验中，由于接受状态事先未知，在第一阶段没有使用任何启发式方法，对于第二阶段，采用了状态的二进制表示的汉明距离。
该启发式方法估计了当前状态，与待搜索的接受状态之间的距离，在实验中使用了一台搭载Intel Core i7-8700、CPU 3.20GHz、内存16.0GB和Windows 10 Pro的HP ProDesk 600 G4 SFF计算机。
为了避免垃圾回收对性能的影响，在运行原型时关闭了Python中内置的垃圾回收功能，反例的长度、运行时间和内存消耗分别用’Length’、‘Time’和’Memory’表示，术语’Sp.’、‘Avg.’、&39;SD’和’MD’分别是目标规范、平均值、标准偏差和中位数的缩写。
根据结果显示，跳过策略在运行时间和内存消耗方面，比原始的ACOhg-live和带有到达终点条件的ACOhg-live有所改进，结果表明，跳过策略能够有效地探索状态空间，相比于OR、ORT和RE，SK、SF和SB往往生成稍长的反例，特别是对于规范B和C。
SK、SF和SB使得许多智能体倾向于优先扩展他们的探索，削弱了ACOhg-live生成短反例的特性，替换策略与OR相比，性能没有显著差异，观察结果表明，仅通过替换策略很难改善ACOhg-live的性能。
接下来，讨论将跳过策略和替换策略结合起来的有效性，对于规范A的运行时间，HY、HF和HB的平均值和中位数几乎与相应的跳过策略相当，且远小于OR、ORT、RE和RET，根据规范B的结果，混合方法HY、HF和HB的平均值、标准差和中位数最小。
对于规范C，混合方法HY、HF和H，B在运行时间和内存消耗方面都表现最高效，除了规范A的运行时间外，与相应的跳过策略SK、SF和SB相比，HY、HF和HB往往降低了运行时间和内存消耗的标准差。
虽然混合方法找到的反例长度特别是对于规范B和C而言有所恶化，但认为性能改进与策略的混合化，能够弥补检测到长反例的这个缺点，策略有望为ACOhg-live提供性能和反例可理解性之间的良好平衡。
在跳过策略中使用的三种随机路径选择方法中，使用正向索引给出的加权概率往往在运行时间和内存消耗方面表现良好，特别是在规范B和C中，所有路径选择方法生成的反例长度几乎相当。
在所有实验条件中，OR平均生成最短的反例，对于运行时间和内存消耗，与OR相比，到达终点条件和策略均表现出良好的结果，虽然策略的内存消耗与到达终点条件相当，但策略对于运行时间的贡献比到达终点条件更为可观。
考虑到这些观察结果，与原始的ACOhg-live相比，提出的策略在效率和反例可理解性方面，在数据库环系统案例中取得了良好的平衡，没有观察到跳过策略的，三个变体之间的显著差异。
讨论为什么提出的策略使得ACOhg-live生成了相对较长的反例，根据实验结果，回想一下，相较于原始的ACOhg-live，Stop-on-Arrival条件往往会生成较长的反例，猜测这个条件可能削弱了ACOhg缩短路径的效果。
事实上，使用Stop-on-Arrival条件意味着缩短路径的过程，在到达某个接受状态之前工作得很好，与普通的ACO不同，ACOhg带有Stop-on-Arrival条件只缩短子路径，并且有时会陷入局部最优解。
虽然Stop-on-Arrival条件在解的质量方面有缺点，但它在时间和空间性能方面具有优势，改善这一缺点的一个潜在方法是使用有效的启发式方法，因为它们对性能和解的质量有很大影响。
在实验中，研究了三种跳过策略的变体，根据结果，虽然使用正向索引定义的加权概率在数据库环系统中的性能最好，但在随机生成的模型中，观察到这些变体之间的差异很小，这些结果表明必须根据验证问题选择最合适的变体。
需要进行进一步的调查，以了解所提出的变体与验证问题特性的关系，接下来，讨论实验的内部问题，原型实现在性能增强方面有很大的改进空间，计划将各种模型检查的优化技术，如部分有序缩减纳入进来。
由于实现以顺序方式运行，可以通过并行化来提高所提出的策略和搜索过程的性能，对ACOhg的参数设置可能会影响其收敛效率，虽然设置是基于先前研究中建立的设置，但对于每个基准测试问题来说，可能存在更高效的设置。
这样的设置可能过于特定于问题领域，对于泛化可能会带来困难，第三，因为ACO是一种随机搜索算法，必须进行多次采样并观察平均性能，不幸的是，一般情况下很难确定适当的样本大小。
在实验中，对每个条件独立采样了30次运行，认为样本大小是合理的，还讨论了实验结果的外部条件，数据库环基准测试是一种典型的分布式并发系统，由于模型检查最显著的特点之一是验证并发系统，认为实验非常适合在模型检查的代表性用例下评估所提出的策略。
另一个基准测试由随机图组成，期望该基准测试不依赖于特定于数据库环基准测试的特征，该模型提供了关于所提出的策略的一般有效性的证据。
解决了模型检查中的两个主要挑战，状态爆炸问题和寻找短反例的问题，方法涉及基于搜索的软件工程，试图通过基于群体智能的非穷举搜索算法来克服问题，提出了两种新颖的探索策略，以使基于蚁群优化的现有模型检查技术ACOhg-live更加高效。
实验结果得出结论，采用所提出的策略的ACOhg-live，在运行时间性能方面优于原始算法，虽然策略检测到的反例比原始的ACOhg-live要长，但认为这个缺点是微妙的，作为未来的工作，计划将合适的启发式方法与策略相结合。
将在实验中选择适用于自动机理论模型检查形式化的启发式方法，还需要将所提出的策略与ACOhg-live之外的其他搜索方法进行比较。
结语
通过对驱动的软件工程，及其在形式验证中的应用进行探讨，以及对基于ACOhg-live的策略改进与性能比较实验进行分析，展示了软件开发和验证领域的研究进展。
通过驱动原则和形式验证技术的结合，可以提升软件系统的质量和可信度，同时，ACOhg-live算法的策略改进也为优化软件开发过程提供了新的思路。
参考文献
1.Alba, E., & Chicano, F. (2007a). ACOhg: dealing with huge graphs. In 9th Annual Conference on Genetic and Evolutionary Computation (pp. 10–17) Association for Computing Machinery.
2.Alba, E., & Chicano, F. (2007b). Finding safety errors with ACO. In 9th Annual Conference on Genetic and Evolutionary Computation . Association for Computing Machinery. (pp. 1066–1073).
3.Alba, E., & Troya, J. M. (1996). Genetic algorithms for protocol validation. In 4th International Conference on Parallel Problem Solving from Nature . Springer (pp. 870–879).
4.Chicano, F., & Alba, E. (2008a). Ant colony optimization with partial order reduction for discovering safety property violations in concurrent models. Information Processing Letters, 106(6), 221–231.
5.Francesca, G., Santone, A., Vaglini, G., & Villani, M. L. (2011). Ant colony optimization for deadlock detection in concurrent systems. In IEEE 35th Annual Computer Software and Applications Conference (pp. 108–117).
