In: Farn Wang (Ed.): Lecture Notes in Computer Science, Vol. 3299: Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004, pages 426-440. Springer-Verlag, 2004.
Abstract: Embedded systems are composed of a heterogeneous collection of digital, analog, and mixed-signal hardware components. This paper presents a method for the verification of systems composed of such a variety of components. This method utilizes a new model, timed hybrid Petri nets (THPN), to model these circuits. In particular, this paper describes an efficient, approximate algorithm to find the reachable states of a THPN model. Using this state space, desired properties specified in ACTL are verified. To demonstrate these methodologies, a few hybrid automata benchmarks, a tunnel diode oscillator, and a phase-locked loop are modeled and analyzed using THPNs.