Crowdsourced formal verification: a business case analysis toward a human-centered business model
Xie, Geoffrey G.
MetadataShow full item record
The DARPA project Crowd Sourced Formal Verification (CSFV) tries to investigate whether offering free games via the Internet that translate player’s actions into program annotations helps to overcome the challenges of the expensive and time-consuming formal verification of software by human experts. This business case analysis evaluates the results of the CSFV-project phase 1. Based on data of the games, the author identifies three problems of the current CSFV approach. The author concludes, in accordance with the Gartner Hype Cycle Research Methodology, that the technology currently is not sufficiently mature to justify a financial investment, but that the cutting-edge approach may reach the plateau of productivity within two to five years, due to parallel maturation of some technologies. The author argues that a human-centered approach is necessary to transform the customer base in order to mitigate the identified deficiencies and to leverage crowdsourced formal verification as a sustainable business. He first explains the concepts relevant in the context of crowdsourced formal verification and the technologies having impact on it. He then identifies the current issues and existing obstacles in the current technology. Based on future trends and visions in the respective fields of technology, and the needs and motivations of people, he proposes a human-centered business model that may foster the implementation of crowdsourced formal verification of software in organizations that depend on security-critical and safety-critical software.
Approved for public release; distribution is unlimited
Showing items related by title, author, creator and subject.
Dumlupinar, Mahmut Firuz (Monterey, California: Naval Postgraduate School, 2013-09);Manual formal software verification is an expensive and time-consuming process. Military software is currently verified manually by highly skilled analysts. To reduce the high costs of the formal verification, DARPA started ...
Phelps, David; Levin, Timothy E.; Auguston, Mikhail (International Conference on i-Warfare and Security, 2008-06-01);We describe the specification of the formal security policy model and formal top-level specification for the Least Privilege Separation Kernel (LPSK) in Alloy, a relatively new modelling language and analysis tool. The ...
Framework for evaluating loop invariant detection games in relation to automated dynamic invariant detectors Yilmaz, Mehmet (Monterey, California: Naval Postgraduate School, 2015-09);Software has a huge and negative impact on the economy. Formal verification is an effective method to check whether a piece of software contains certain kinds of errors. Defense Advanced Research Projects Agency (DARPA) ...