Automating Component-Based Embedded Software Construction via Formal Synthesis and LLMs
摘要
In embedded software, reactive synthesis can automatically generate control automata from Generalized Reactivity of rank 1 (GR(1)) specifications. However, this approach requires handcrafted specifications, and reactive synthesis only provides the automata as the control logic, while the rest of the program must be implemented manually. To address these issues, we propose an automated method for building component-based embedded software through formal synthesis and Large Language Models (LLMs), comprising the following parts: first, we design a component-based embedded software architecture to support our software synthesis method; then, we develop an approach to translate tasks expressed in natural language (NL) into GR(1) specifications based on LLMs, producing the control automaton for our software architecture. We combine the intelligence and simplicity of LLMs with the correctness and safety of formal synthesis.