Fuzzing Executable ASMETA Models

Specifications of modern complex systems can become so large that model cutting or abstraction is required to enable automatic analysis by model checkers. Moreover, relying solely on model simulators or scenario-based validation does not provide sufficient guarantees regarding the model’s compliance with requirements or its satisfaction of desired properties. Building on the idea of code fuzzing and leveraging the executability of models, this paper introduces a model fuzzing approach for Abstract State Machine specifications developed in ASMETA. The supporting tool, specified in ASMETA, enables randomized executions of models with the aim of triggering unexpected behaviors such as crashes, assertion failures, or security vulnerabilities. To evaluate our approach, we consider two well-known case studies from the literature, one from security protocols and one from concurrent systems, to demonstrate its analysis capabilities.