SLEEC-PATCH

SLEEC-PATCH is a tool-supported methodology that automatically generates, formally verifies, and ranks resolution patches for well-formedness issues in SLEEC robot normative specifications. The framework combines formal reasoning with LLM-assisted semantic refinement to produce correct-by-construction candidate repairs.

Workflow

  • ✔ Detects conflicts, redundancies, concerns, purpose blocking, and situational conflicts using state-of-the-art tooling.
  • ✔ Selects appropriate repair operators based on the diagnosed issue.
  • ✔ Generates repairs using formal rule transformations.
  • ✔ Uses an LLM only for semantic refinements requiring new concepts or rules.
  • ✔ Formally verifies every candidate patch using state-of-the-art verification tooling.
  • ✔ Ranks verified patches according to criteria established with multidisciplinary stakeholders.