Constrained Automated Requirements Formalization for Rigorous Analysis with Alloy

Abstract

Early detection of security flaws in software requirements is crucial yet challenging due to the inherent ambiguity of natural language (NL) specifications. While manual reviews are labor-intensive and lack formal rigor, automated formal verification remains bottlenecked by the steep expertise barrier required for manual specification. This paper addresses these challenges through Constrained Automated Requirements Formalization (CARF). Instead of generating arbitrary formal formulas from scratch, our approach restricts the translation domain by leveraging Large Language Models (LLMs) to map unstructured NL requirements onto a predefined, bounded logic of an existing framework for common design weaknesses. We evaluate our methodology across five real-world security requirements datasets against traditional heuristic baselines. The experimental results demonstrate that CARF is robust, successfully outperforming keyword matching and showing structural resilience to minor translation imperfections when identifying missing design controls. We position our tool as a powerful collaborative assistant that significantly lowers the barrier to adopting formal security verification methods during the early software design lifecycle.