Temporal HAL-API Dependencies as a Gateway to Formal Embedded Software Development
By: Manuel Bentele , Andreas Podelski , Axel Sikora and more
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.
Similar Papers
Towards the Coordination and Verification of Heterogeneous Systems with Data and Time
Software Engineering
Checks if complex systems work together correctly.
Automated Hardware Trojan Insertion in Industrial-Scale Designs
Cryptography and Security
Creates fake computer bugs to test security.
Bridging Threat Models and Detections: Formal Verification via CADP
Cryptography and Security
Checks if security rules catch real threats.