2011/06/12 by Raimundo Barreto, Barreto, Raimundo, Lucas C. Cordeiro +3 · 1 citation
Computer Science · #Embedded Systems Design Techniques #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Real-Time Systems Scheduling
paper · pdf · doi:10.48550/arxiv.1106.2320
openalex publication_date 2011/06/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Embedded systems are everywhere, from home appliances to critical systems\nsuch as medical devices. They usually have associated timing constraints that\nneed to be verified for the implementation. Here, we use an untimed bounded\nmodel checker to verify timing properties of embedded C programs. We propose an\napproach to specify discrete time timing constraints using code annotations.\nThe annotated code is then automatically translated to code that manipulates\nauxiliary timer variables and is thus suitable as input to conventional,\nuntimed software model checker such as ESBMC. Thus, we can check timing\nconstraints in the same way and at the same time as untimed system\nrequirements, and even allow for interaction between them. We applied the\nproposed method in a case study, and verified timing constraints of a pulse\noximeter, a noninvasive medical device that measures the oxygen saturation of\narterial blood.\n