Verifying Embedded C Software with Timing Constraints using an Untimed Bounded Model Checker

Raimundo Barreto, Lucas Cordeiro, Bernd Fischer

Research output: Contribution to journalArticlepeer-review

Abstract

Embedded systems are everywhere, from home appliances to critical systems such as medical devices. They usually have associated timing constraints that need to be verified. Here, we use an untimed bounded model checker to verify timing properties of embedded C programs. We describe an approach to specify discrete-time timing constraints using code annotations. The annotated code is then automatically translated to code that manipulates auxiliary timer variables and is thus suitable as input to conventional, untimed software model checkers such as ESBMC. Moreover, we can check timing constraints in the same way and at the same time as untimed system requirements, and even allow for interaction between them. We applied the proposed method in a case study, and verified timing constraints of a pulse oximeter, a noninvasive medical device that measures the oxygen saturation of arterial blood.
Original languageEnglish
Pages (from-to)46-52
Number of pages7
JournalBrazilian Symposium on Computing System Engineering : proceedings
Publication statusPublished - 2011

Keywords

  • Bounded model checker
  • timing constraints
  • code verification

Fingerprint

Dive into the research topics of 'Verifying Embedded C Software with Timing Constraints using an Untimed Bounded Model Checker'. Together they form a unique fingerprint.

Cite this