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

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

2011-06-12

arxiv.org/abs/1106.2320v1

Computer Science

Logic in Computer Science

16 pages

Scientific paper

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 for the implementation. Here, we use an untimed bounded model checker to verify timing properties of embedded C programs. We propose 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 checker such as ESBMC. Thus, 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.

Affiliated with

Also associated with

No associations

Rating

Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-712562