Designing FSMs Specifications from Requirements with GPT 4.0

1. Problem Statement

The paper addresses the challenge of automatically generating formal specifications for reactive systems, specifically Deterministic Finite State Machines (DFSMs), from natural language requirements.

• Context: Formal specifications (like FSMs) are crucial for model-driven engineering, automated testing, and verification. However, creating them manually is time-consuming and error-prone.
• The Gap: While Large Language Models (LLMs) like GPT-4 show promise in generating code and constraints, their ability to accurately translate unstructured natural language descriptions into rigorous, executable FSM specifications is unproven.
• The Risk: Low-quality generated FSMs lead to undetected faults during testing, increasing the risk of system failure in production.
• Core Challenge: If an LLM generates a faulty FSM, how can it be automatically repaired? Existing methods for FSM repair (based on distinguishing sequences or checking sequences) have not been integrated into LLM-based workflows.

2. Methodology

The authors propose a framework that combines LLM prompt engineering with expert-centric repair strategies based on formal methods.

A. Data Generation (Simulation)

Since real-world industrial data was not available for this study, the authors created a simulation environment:

• Oracles: Randomly generated "Oracle" DFSMs (the ground truth).
• Descriptions: Natural language descriptions (English sentences) automatically generated for each Oracle transition using specific sentence patterns.
• Variables: Experiments varied the number of states (5, 10, 25) and fixed inputs/outputs (5 inputs, 2 outputs).

B. LLM Generation Phase

• Model: GPT-4 (specifically GPT-4o).
• Prompt Engineering: A system role was defined to act as a software engineer. The user prompt provided the natural language description and requested a CSV output with a specific format (State, Input, Output, Next_State).
• Output: The LLM generates a candidate DFSM.

C. Evaluation & Repair Phase

The framework evaluates the generated DFSM against the Oracle and applies one of four repair approaches if faults are detected:

1. Approach 1: Syntactic Fault Repair (Oracle-Assisted)

   • Mechanism: Compares the generated FSM and Oracle directly to identify specific transition faults (missing, extra, wrong output, wrong target).
   • Repair: Constructs a new prompt explicitly listing the "wrong" transitions to remove and "missing" transitions to add.
   • Assumption: Requires an Oracle (unrealistic in practice but useful for benchmarking).

2. Approach 2: Distinguishing Sequence Repair (Oracle-Assisted)

   • Mechanism: Uses a distinguishing automaton to find input sequences that produce different outputs in the Oracle vs. the Generated FSM.
   • Repair: Prompts the LLM to correct the output for specific input sequences.
   • Limitation: The LLM struggled with the volume of information in these sequences, leading to lower success rates.

3. Approach 3: Checking Sequence Repair (Expert-Assisted)

   • Mechanism: Uses a single, long checking sequence (a trace that uniquely identifies the FSM).
   • Repair: An expert (or Oracle) provides the expected output for this sequence. The prompt is refined to enforce this specific trace.
   • Limitation: Computationally expensive (NP-complete) and the long sequences overwhelmed the LLM's attention mechanism, resulting in low repair success (40% in experiments).

4. Approach 4: Fault Model-Based Repair (Expert-Assisted)

   • Mechanism: Instead of asking the LLM to fix specific errors, this approach defines a Repair Domain using a Mutation Machine.
   • Process:
     1. Identify common LLM fault patterns (e.g., output errors, missing transitions).
     2. Generate a Mutation Machine containing all plausible "patches" (variations of the generated FSM).
     3. Use an expert to answer output queries for specific inputs.
     4. Use a SAT-based mining algorithm to filter the mutation domain and select the unique FSM that matches all expert answers.
   • Advantage: Does not rely on the LLM to "reason" about the fix; it relies on formal mining within a constrained space.

3. Key Contributions

• Simulated Dataset: Creation of a benchmark dataset of randomly generated DFSMs and their corresponding natural language descriptions to evaluate LLM capabilities.
• Prompt Engineering: Development of specific prompts to generate CSV-formatted FSMs from text.
• Four Repair Strategies: A comparative analysis of four distinct methods for repairing LLM-generated specifications, ranging from direct syntactic correction to formal mining via mutation machines.
• Empirical Evaluation: A rigorous statistical evaluation of GPT-4's accuracy and the efficacy of the repair methods.

4. Experimental Results

• Generation Accuracy:

  • GPT-4 performs reasonably well on small FSMs (5 states) but error rates increase significantly with complexity (10+ states).
  • Most Common Faults: Output faults (wrong output symbol) and Missing Transition faults.
  • Table 1 Data: For 10-state machines, the average number of faults per machine was 1.1, with a maximum of 11.

• Repair Effectiveness:

  • Syntactic Repair (Approach 1): 100% Success Rate. When the LLM is explicitly told which transitions are wrong/right, it can almost perfectly correct the FSM.
  • Distinguishing Sequence (Approach 2): 0% Success for 10-state machines. The LLM failed to process the complex input-output trace constraints.
  • Checking Sequence (Approach 3): 40% Success (5 states). The method is too computationally heavy and the long sequences confuse the LLM.
  • Fault Model/Mutation (Approach 4): 100% Success Rate. By constraining the search space to a mutation machine and using expert queries to filter candidates, the correct FSM was always found.

5. Significance and Conclusion

• LLM Limitations: The study highlights that while LLMs can generate initial FSM drafts, they lack the precision to handle complex semantic constraints (like long distinguishing sequences) or self-correct without explicit guidance. They struggle with "sharp analysis" of large information volumes.
• Hybrid Approach is Essential: The paper argues that LLMs should not be used in isolation for critical specification design. A hybrid approach is required where:
  1. LLMs generate the initial draft.
  2. Formal methods (mutation machines, checking sequences) define the repair space.
  3. Human experts (or oracles) provide validation queries.
  4. Algorithms mine the correct specification from the constrained domain.
• Future Work: The authors suggest applying this framework to industrial-scale systems, where domain-specific context might improve LLM performance, and further refining the fault models to reduce the number of expert queries needed.

In summary, the paper demonstrates that LLMs are viable for the initial generation of FSMs from text but require a robust, formal-methods-based repair layer to ensure correctness, with the Fault Model-based approach emerging as the most promising and reliable strategy.