Temporal HAL-API Dependencies as a Gateway to Formal Embedded Software Development

TL;DR

Temporal HAL-API Dependencies (THADs) offer a practical approach to specify and verify correctness properties in embedded software, bridging the gap between simple static analysis and comprehensive formal methods.

Contribution

This paper introduces THADs as a new formalism that balances specification effort and verification automation for embedded software correctness.

Findings

THADs can be specified with moderate effort via annotations.

Verification of THADs is automatable using model checking.

THADs serve as a practical gateway to formal methods in industry.

Abstract

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.