SRI智库和大学将软件验证变成游戏

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

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

Xylem games使用众包技术来搜索软件程序没有漏洞的证据，”SRI计算机科学实验室的项目主管、整个Chekofv项目的首席调查员约翰默里(crowd source有助于参考优化形式验证的应急知识(The这些迷人的益智游戏中插入了一些软件代码，玩家可以通过发现岛上植物行为的模式来识别新的植物物种。玩游戏并正确识别模式的人越多，验证的代码就越多，他们将与软件程序的其余部分一起工作——就像解决一个巨大的拼图游戏一样。

Xylem益智游戏是名为Chekofv的SRI项目的一部分。这是DARPA资助的众包正式验证计划的一部分。玩游戏，不需要懂什么软件。

游戏设定在一个新发现的名叫米拉弗罗拉的岛上。玩家是一名植物学家，被派去描述岛上许多不寻常的开花植物。勇敢的探险者会得到一个“植物相比较仪”来检查植物。使用这个装置，玩家可以找到植物上花朵特征之间的数学关系。随着玩家团体发现并描述植物，他们可以看到岛上有多少地方已经被探索过了。游戏也有故事情节。

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

“花的数量实际上是软件循环中变量的值。通过发现花朵之间的这些关系，你实际上是在描述一种循环行为，”UCSC巴斯金工程学院计算机科学系教授兼主任、该大学木质部首席研究员吉姆怀特黑德解释道。

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

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

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

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

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

在加州大学圣克鲁斯分校的游戏和可玩媒体中心，大约有20名员工、研究生和本科生参与了游戏的制作。这款游戏可在苹果iTunes应用商店免费下载，并将于2014年面向安卓平板电脑推出。

　　免责声明：本文由用户上传，与本网站立场无关。财经信息仅供读者参考，并不构成投资建议。投资者据此操作，风险自担。 如有侵权请联系删除！