A. , M. And-lamport, and L. , An old-fashioned recipe for real time, ACM Transactions on Programming Languages and Systems (TOPLAS), vol.16, issue.5, pp.1543-1571, 1994.

A. , R. And, and D. L. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.

B. , T. And, and A. Sowmya, Automatically transforming and relating Uppaal models of embedded systems, Proceedings of the 8th ACM Int. Conference on Embedded Software (EMSOFT'08, pp.59-68, 2008.

H. , T. A. Nicollin, X. Sifakis, J. And-yovine, and S. , Symbolic model checking for real-time systems, Information and Computation, vol.111, issue.2, pp.192-244, 1994.

I. Corporation, MCS ® 51 microcontroller family user's manual, 1994.

J. , H. E. Larsen, K. G. And-skou, and A. , Scaling up Uppaal: Automatic verification of real-time systems using compositionality and abstraction, Proceedings of the 6th Int. Symposium on Formal Techniques for Real-Time and Fault-Tolerance, pp.19-30, 2000.

K. , D. K. Lynch, N. Segala, R. And-vaandrager, and F. , The Theory of Timed I/O Automata. Synthesis Lectures on Computer Science, 2006.

L. , K. G. Pettersson, P. And-wang, and Y. , Uppaal in a nutshell, Int. Journal of Software Tools for Technology Transfer, vol.1, pp.1-2, 1997.

L. , N. And, and F. Vaandrager, Forward and backward simulations. Part II: Timing-based systems, Information and Computation, vol.128, issue.1, pp.1-25, 1996.

S. Corporation, GP2D02: Compact, high sensitive distance measuring sensor, 1997.

V. , F. And, and A. De-groot, Analysis of a biphase mark protocol with Uppaal and PVS. Formal Aspects of Computing 18, pp.433-458, 2006.