In logical reasoning, specification inference attempts to synthesize an explanatory hypothesis from a given conclusion. We consider the specification synthesis problem for database-backed web-applications where only an oracle access to the application is available. Such is a real case for test teams where they are not provided access to the application. Our algorithm begins with an initial hypothesis constructed from responses of the web-application on a sampled dataset, and then improves this hypothesis iteratively via carefully constructed queries to the application (via an SMT solver). Finally, statistical tests are used to validate the soundness and maximality of the constructed hypothesis. We implement our algorithm in a tool, Vivaran, and demonstrate its capabilities on a large web-based enterprise resource planning (ERP) software. Vivaran infers semantically equivalent specifications as the ground-truth in all cases.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Specification Inference Modulo Oracles for Database-Backed Web Applications

  • Nitesh Trivedi,
  • Subhajit Roy

摘要

In logical reasoning, specification inference attempts to synthesize an explanatory hypothesis from a given conclusion. We consider the specification synthesis problem for database-backed web-applications where only an oracle access to the application is available. Such is a real case for test teams where they are not provided access to the application. Our algorithm begins with an initial hypothesis constructed from responses of the web-application on a sampled dataset, and then improves this hypothesis iteratively via carefully constructed queries to the application (via an SMT solver). Finally, statistical tests are used to validate the soundness and maximality of the constructed hypothesis. We implement our algorithm in a tool, Vivaran, and demonstrate its capabilities on a large web-based enterprise resource planning (ERP) software. Vivaran infers semantically equivalent specifications as the ground-truth in all cases.