Verifying Embedded C Software with Timing Constraints Using an Untimed Bounded Model Checker
Resumo
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.
Referências
N. S. Bjørner A. Browne M. A. Colón B. Finkbeiner Z. Manna H. B. Sipma and T. E. Uribe "Verifying temporal properties of reactive systems: A STeP tutorial " Formal Methods in System Design vol. 16 pp. 227-270 June 2000.
J. R. Burch E. M. Clarke K. L. McMillan D. L. Dill and L. J. Hwang "Symbolic model checking: 1020 states and beyond " Information and Computation vol. 98 pp. 142-170 June 1992.
K. Y. Chun and D. V. Hung "Verifying real-time systems using untimed model checking tools " The United Nations University. Tech. Report UNU-IIST 302 June 2004.
E. Clarke O. Grumberg and D. Peled Model Checking. The MIT Press January 2000.
L. Cordeiro and B. Fischer "Verifying Multi-threaded Software using SMT-based Context-Bounded Model Checking " in International Conference on Software Engineering (ICSE'2011). ACM/IEEE May 21-28 2011 pp. 331-340.
L. Cordeiro B. Fischer H. Chen and J. Marques-Silva "Semiformal verification of embedded software in medical devices considering stringent hardware constraints " in Int. Conf. on Emb. Soft. and Systems (ICESS'09). pp. 396-403.
P. Ganty and R. Majumdar "Analyzing real-time event-driven programs " in Int. Conf. Formal Modeling and Analysis Timed Systems (FORMATS'09) 2009 pp. 164-178.
T. Henzinger P.-H. Ho and H. Wong-Toi "Hytech: A model checker for hybrid systems " Software Tools for Technology Transfer vol. 1 pp. 460-463 1997. (Pubitemid 127089004)
L. Lamport "Real-time model checking is really simple " in Correct Hardware Design and Verification Methods (CHARME'05) LNCS 3725 October 3-6 2005 pp. 162-175.
K. G. Larsen P. Pettersson and W. Yi "UPPAAL in a Nutshell " Int. Journal on Software Tools for Technology Transfer vol. 1 no. 1-2 pp. 134-152 Oct. 1997.
L. D. Moura and N. Bjrner "Z3: An efficient smt solver " Tools and Algorithms for the Construction and Analysis of Systems LNCS 4963 pp. 337-340 2008.
J. Ostroff and H. Ng "Verifying real-time systems with standard theories " in In AMAST Workshop on Real-Time Systems 2000.
G. Rote "Crossing the bridge at night " EATCS Bulletin vol. 78 pp. 241-246 October 2002.
B. Schlich and S. Kowalewski "Model checking C source code for embedded systems " Software Tools for Technology Transfer vol. 11 no. 3 pp. 187-202 June 2009.
J. Sifakis S. Tripakis and S. Yovine "Building models of real-time systems from application software " In Proceedings of the IEEE vol. 91 pp. 100-111 January 2003.
F. Wang G.-D. Huang and F. Yu "TCTL inevitability analysis of dense-time systems: From theory to engineering " IEEE Trans. Softw. Eng. vol. 32 pp. 510-526 July 2006. (Pubitemid 46405282)
R. Wilhelm et. al. "The worst-case execution-time problem: overview of methods and survey of tools " ACM Trans. Emb. Comp. Systems vol. 7 pp. 36:1-36:53 May 2008.
S. Yovine "Kronos: A Verification Tool for Real-Time Systems " International Journal on Software Tools for Technology Transfer vol. 1 pp. 123-133 1997
