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. |
Year | DOI | Venue |
---|---|---|
2004 | 10.1007/978-3-540-30476-0_35 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
modeling,analog signal,phase lock loop,hybrid system,petri net,program analysis,analog circuit,oscillations,phase locked loop,digital signal,discrete system,state space,embedded system | Petri net,Computer science,Digital signal,Automaton,Algorithm,Analog signal,Computer engineering,State space,Hybrid system,Discrete system,Hybrid automaton,Distributed computing | Conference |
Volume | ISSN | Citations |
3299 | 0302-9743 | 12 |
PageRank | References | Authors |
0.71 | 22 | 5 |
Name | Order | Citations | PageRank |
---|---|---|---|
Scott Little | 1 | 132 | 9.42 |
David Walter | 2 | 98 | 5.38 |
Nicholas Seegmiller | 3 | 59 | 3.35 |
Chris J. Myers | 4 | 607 | 75.73 |
Tomohiro Yoneda | 5 | 353 | 41.62 |