软件验证听起来不是一个有趣的工作。它涉及检查程序以确保它没有常见的漏洞。因此，一支由计算机科学家组成的团队制作了一款名为Xylem的游戏。iPad益智游戏可帮助程序员找到“循环不变量”，或正式软件验证的重要部分。

加利福尼亚州门洛帕克的SRI国际智库和加州大学圣克鲁兹分校的团队已经接受了“游戏化”，或者使用类似游戏的机制来使日常任务变得更有趣。在这种情况下，益智游戏将利用普通消费者来执行验证任务。如果他们受理，他们可以更加警觉并发现更多的错误。最重要的是，更广泛的人群可以访问进行验证的任务。

Xylem游戏利用众包技术搜索软件程序没有漏洞的证据，”SRI计算机科学实验室的项目主管，整个Chekofv项目的首席调查员John Murray说道(人群来源帮助简称优化形式验证的应急知识(The。“这些引人入胜的益智游戏中插入了一些软件代码，玩家可以通过发现岛上植物行为的模式来识别新的植物物种。玩游戏并正确识别模式的人越多，验证的代码就越多，它们将与软件程序的其余部分一起工作 - 就像解决一个巨大的拼图游戏一样。

Xylem益智游戏是名为Chekofv的SRI项目的一部分。它是由美国国防高级研究计划局(DARPA)资助的Crowd Sourced Formal Verification计划的一部分。要玩游戏，您不必了解任何软件。

游戏设置在一个名为Miraflora的新发现的岛屿上。该玩家是一名植物学家，被派去描述岛上许多不寻常的开花植物。勇敢的探险家被给予一个“floraphase比较器”用于检查植物。使用该设备，玩家可以找到植物上花朵特征之间的数学关系。随着玩家群体发现并描述植物，他们可以看到该岛有多少被探索过。游戏也有故事情节。

Xylem是DARPA CSFV计划中的五款电脑游戏之一，可在Verigames网站上找到。

“花的数量实际上是软件循环中变量的值。通过发现花之间的这些关系，你实际上是在描述一个循环的行为，“UCSC巴斯金工程学院的教授和计算机科学系主任，以及该大学Xylem的首席研究员Jim Whitehead解释道。

通常，在软件程序中查找循环不变量是一项具有挑战性的任务，需要进行培训。

“这对于计算机科学专业学生来说是一个难以理解的概念，”怀特黑德说。“通过把它变成一个游戏，它就变成了一个没有基本数学技能的未经训练的人可以做到的事情。”

正式的软件验证使用不多，因为很少有人接受过正确的培训。

“没有足够的专家来正式验证正在开发的所有类型的软件，”他说。

SRI International计算机科学实验室主任Patrick Lincoln表示，“Chekofv项目是一项积极的研究计划，以高度创新的方式解决这些复杂的软件问题。通过使正式的软件验证更易于访问和娱乐，更多人可以通过玩Xylem游戏来帮助提高全球关键软件的可靠性和安全性。“

在加州大学圣克鲁兹分校的游戏和可玩媒体中心，约有20名员工，研究生和本科生 参与了游戏的制作。该游戏在Apple iTunes App Store中免费提供，并将于2014年面向Android平板电脑推出。