Software verification games: Designing Xylem, The Code of Plants.
FDG(2014)
摘要
Formal software verification is a software engineering technique for modeling a software system’s source code, and then proving properties about it, such as freedom from security vulnerabilities. Though proofs are largely automated, formal source code modeling is time consuming and requires substantial human attention. Xylem: The Code of Plants is an iPad game where players make observations about unusual plants, and thereby model the behavior of software loops. With large numbers of players, the goal of Xylem is to have players model the behavior of large software systems faster, and at lower cost, than is currently achievable with formal verification experts. We present an overview of major design challenges and approaches encountered in the design of a game for crowd-sourced formal software verification. A core challenge is the need to accurately reflect the structure of real-world software source code in a game setting, without showing the source code text to players. This goal created a tension with the need to design a game that is a fun, engaging experience, which often requires simplification of the core activities of the player. Another challenge is not knowing what is the solution to a particular problem, and the resulting difficulty in providing scoring feedback to the player. These design considerations are of interest for crowd-sourcing games in general, and software engineering games in particular.
更多查看译文
AI 理解论文
溯源树
样例
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要