Testing is in practice commonly performed by executing carefully planned scripts, which exercise particular planned scenarios. Fuzz testing can be applied as a complementary approach, to exercise a system outside the boundaries of the expected. However, fuzz testing can be too random. In this work, we explore an approach to fuzz testing using an expressive temporal logic named MaTL (Matching Temporal Logic) for expressing constraints on tests, restricting generated tests to only such that satisfy the provided constraints. MaTL is a linear temporal logic that supports future and past time operators and a match construct that selects argument values from events, similar to pattern matching in functional programming languages. Constraint solving is performed using the Z3 SMT solver.

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

Fuzz Testing with Temporal Constraints

  • Klaus Havelund,
  • Tracy Clark,
  • Vivek Reddy

摘要

Testing is in practice commonly performed by executing carefully planned scripts, which exercise particular planned scenarios. Fuzz testing can be applied as a complementary approach, to exercise a system outside the boundaries of the expected. However, fuzz testing can be too random. In this work, we explore an approach to fuzz testing using an expressive temporal logic named MaTL (Matching Temporal Logic) for expressing constraints on tests, restricting generated tests to only such that satisfy the provided constraints. MaTL is a linear temporal logic that supports future and past time operators and a match construct that selects argument values from events, similar to pattern matching in functional programming languages. Constraint solving is performed using the Z3 SMT solver.