Making Hard Fun in Crowdsourced Model Checking -- Balancing Crowd Engagement and Efficiency to Maximize Output in Proof by Games

Author

Moffitt, Kerry ; Ostwald, John ; Watro, Ron ; Church, Eric

Author_Institution

Raytheon BBN Technol., Cambridge, MA, USA

fYear

2015

fDate

19-19 May 2015

Firstpage

30

Lastpage

31

Abstract

We describe Proof by Games, a system that mathematically proves software to be free from certain defects by transforming the refinement of formal model checking results into a public, browser-based, crowd sourced game. We then introduce Ghost Map: Hyperspace, the second-generation game in the Proof by Games system, and describe how we are introducing game elements whose sole purpose is to increase the level of engagement. This may reduce player efficiency but should increase crowd size and engagement - and ultimately increase the total level of crowd contribution to the real-world task.

Keywords

computer games; formal specification; Ghost Map; Proof by Games system; crowd engagement; crowdsourced model checking; formal model checking; game elements; proof by games; Crowdsourcing; Entertainment industry; Games; Model checking; Security; Software; Tutorials; CEGAR; browser-based; crowdsourcing; formal methods; model checking; software; video games;

fLanguage

English

Publisher

ieee

Conference_Titel

CrowdSourcing in Software Engineering (CSI-SE), 2015 IEEE/ACM 2nd International Workshop on

Conference_Location

Florence

Type

conf

DOI

10.1109/CSI-SE.2015.13

Filename

7169426