 |
|
|||
| Authors: | Karsten Strehl, Lothar Thiele |
| Group: | Computer Engineering |
| Type: | Article |
| Title: | Interval Diagrams for Efficient Symbolic Verification of Process Networks |
| Year: | 2000 |
| Month: | August |
| Pub-Key: | ST00 |
| Journal: | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems |
| Volume: | 19 |
| Number: | 8 |
| Pages: | 939-956 |
| Keywords: | ESD |
| Abstract: | In this paper, a representation of multi-valued functions called interval decision diagrams (IDDs) is introduced. It is related to similar representations such as binary decision
diagrams. Compared to other functional representations with regard to symbolic formal verification approaches, IDDs show some important properties that enable us to verify process networks and
related models of computation more adequately than with conventional approaches. Therefore, a new form of transition relation representation called interval mapping diagram (IMD) is
introduced.
A novel approach to symbolic model checking of process networks is presented. Several drawbacks of traditional strategies are avoided using IDDs and IMDs. The resulting transition relation IMD is very compact, enabling fast image computations. Furthermore, no artificial limitations concerning buffer capacities or equivalent have to be introduced. Additionally, applications concerning scheduling of process networks are feasible. IDDs and IMDs are defined, their properties are described, and computation methods and techniques are given. |
| Remarks: | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 19(8), August 2000 |
| Resources: | [BibTeX] [Paper as PDF] |
