Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913581894729728 |
|---|---|
| author | Patil, Minal Suresh Ung, Gustav Nyberg, Mattias |
| author_facet | Patil, Minal Suresh Ung, Gustav Nyberg, Mattias |
| contents | The paper studies how code generation by LLMs can be combined with formal verification to produce critical embedded software. The first contribution is a general framework, spec2code, in which LLMs are combined with different types of critics that produce feedback for iterative backprompting and fine-tuning. The second contribution presents a first feasibility study, where a minimalistic instantiation of spec2code, without iterative backprompting and fine-tuning, is empirically evaluated using three industrial case studies from the heavy vehicle manufacturer Scania. The goal is to automatically generate industrial-quality code from specifications only. Different combinations of formal ACSL specifications and natural language specifications are explored. The results indicate that formally correct code can be generated even without the application of iterative backprompting and fine-tuning. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_13269 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software Patil, Minal Suresh Ung, Gustav Nyberg, Mattias Software Engineering Artificial Intelligence The paper studies how code generation by LLMs can be combined with formal verification to produce critical embedded software. The first contribution is a general framework, spec2code, in which LLMs are combined with different types of critics that produce feedback for iterative backprompting and fine-tuning. The second contribution presents a first feasibility study, where a minimalistic instantiation of spec2code, without iterative backprompting and fine-tuning, is empirically evaluated using three industrial case studies from the heavy vehicle manufacturer Scania. The goal is to automatically generate industrial-quality code from specifications only. Different combinations of formal ACSL specifications and natural language specifications are explored. The results indicate that formally correct code can be generated even without the application of iterative backprompting and fine-tuning. |
| title | Towards Specification-Driven LLM-Based Generation of Embedded Automotive Software |
| topic | Software Engineering Artificial Intelligence |
| url | https://arxiv.org/abs/2411.13269 |