Automated generation and formal validation of resolution patches for well-formedness issues in normative requirements.