|
Authors: | Karsten Strehl, Lothar Thiele |
Group: | Computer Engineering |
Type: | Inproceedings |
Title: | Symbolic Model Checking of Process Networks Using Interval Diagram Techniques |
Year: | 1998 |
Month: | November |
Pub-Key: | St98b |
Book Titel: | Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD-98) |
Pages: | 686-692 |
Keywords: | SMC IDD |
Abstract: | Process network models – consisting in general of concurrent processes communicating through unidirectional FIFO queues – are commonly used for specification and synthesis
of distributed systems. An example are Kahn process networks which form the basis for implementation methods such as real-time scheduling and allocation. While many simple dataflow models –
for instance, synchronous dataflow and computation graphs – are sufficiently analyzable by balance equation methods, these fail for more powerful descriptions as general process networks
due to their complex internal state.
Typical questions to be answered by formal verification of process networks are about the absence of deadlocks, the boundedness of the required memory, or proving certain properties of the specification. Especially memory boundedness is important as process networks in general may not be scheduled statically. Thus, dynamic schedulers have to be deployed which cannot always guarantee to comply with memory limitations. Formal verification may assist during development of scheduling strategies by confirming the compliance with explicit resource limitations or by determining inherent bounds. During the last years, a promising approach named symbolic model checking was applied to many areas of system verification in computer engineering and related research fields and even has been able to enter the area of industrial applications. It makes use of binary decision diagrams (BDDs) which are an efficient representation of Boolean functions and allow for their very fast manipulation. But when applying this technique to process networks or related models of computation, several difficulties occur that question its usefulness in this area. The major limiting factor of symbolic model checking is the state explosion problem caused by the queues of potentially unlimited length. To overcome several limitations of conventional symbolic model checking of process networks, we present an approach that uses interval decision diagrams (IDDs) combined with interval mapping diagrams (IMDs) – especially their restricted form predicate action diagrams (PADs) – and thus is able to remedy described lacks of traditional approaches. Fundamentally, it is based on a more reasonable way of describing the mentioned form of transition relations. Major enhancements of symbolic model checking with IDDs and IMDs are:
|
Remarks: | Proceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD-98), San Jose, California, pages 686-692, November 8-12, 1998 |
Location: | San Jose, California |
Resources: | [BibTeX] [Paper as PDF] |