Temporal HAL-API Dependencies as a Gateway to Formal Embedded Software Development
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911318652485632 |
|---|---|
| author | Bentele, Manuel Podelski, Andreas Sikora, Axel Westphal, Bernd |
| author_facet | Bentele, Manuel Podelski, Andreas Sikora, Axel Westphal, Bernd |
| contents | Temporal HAL-API Dependencies (THADs) can be useful to capture an interesting class of correctness properties in embedded software development. They demand a moderate effort for specification (which can be done via program annotations) and verification (which can be done automatically via software model checking). In this sense, they have the potential to form an interesting sweet spot between generic properties (that demand virtually no specification effort, and that are typically addressed by static analysis) and application-specific properties as addressed by full-fledged formal methods. Thus, they may form a gateway to wider and more economic use of formal methods in industrial embedded software development. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_12788 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Temporal HAL-API Dependencies as a Gateway to Formal Embedded Software Development Bentele, Manuel Podelski, Andreas Sikora, Axel Westphal, Bernd Software Engineering Temporal HAL-API Dependencies (THADs) can be useful to capture an interesting class of correctness properties in embedded software development. They demand a moderate effort for specification (which can be done via program annotations) and verification (which can be done automatically via software model checking). In this sense, they have the potential to form an interesting sweet spot between generic properties (that demand virtually no specification effort, and that are typically addressed by static analysis) and application-specific properties as addressed by full-fledged formal methods. Thus, they may form a gateway to wider and more economic use of formal methods in industrial embedded software development. |
| title | Temporal HAL-API Dependencies as a Gateway to Formal Embedded Software Development |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2512.12788 |