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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Automating Component-Based Embedded Software Construction via Formal Synthesis and LLMs

  • Sirui Liu,
  • Wei Dong,
  • Tiecheng Ma,
  • Yanqi Dong,
  • Dong Yang

摘要

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.