SPECENG: Specification Engineering for Temporal Logical Specifications

In specification-driven software engineering, formal specifications are crucial for guiding the development process by acting as a bridge between informal requirements and machine-understandable implementations. These specifications ensure correctness at every stage, from identifying inconsistencies during requirements analysis to generating test cases, verifying system properties, and even synthesizing correct implementations. However, creating valid specifications remains a major challenge and is often considered a bottleneck in achieving higher-quality, reliable software systems. In this project SPECENG, we envision a systematic process to develop linear temporal logical specifications that are valid and match the engineers' intention. Furthermore, we aim to improve the quality of the specifications in terms of their comprehensibility by engineers and in terms of their efficiency for downstream software engineering tasks, such as program synthesis and verification. Thus, we envision a process of specification engineering with the following contributions: (1) for validity, we will create a novel two-way interactive process from natural language to LTL formulas and back, via interactive use of LLMs and positive and negative traces (2) for quality, we will develop novel refactorings that address anti-patterns and result in specifications that are readable by engineers and efficient for use by verifiers and synthesizers.