Symbolic model checking of process networks using interval diagram techniques

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Symbolic model checking of process networks using interval diagram techniques

Full text

Pdf (772 KB)

Source

International Conference on Computer Aided Design archive
Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design table of contents

San Jose, California, United States

Pages: 686 - 692

Year of Publication: 1998

ISBN:1-58113-008-2

Authors

Karsten Strehl	Computer Engineering and Networks Lab (TIK), Swiss Federal Institute of Technology (ETH), Gloriastrasse 35, 8092 Zurich, Switzerland
Lothar Thiele	Computer Engineering and Networks Lab (TIK), Swiss Federal Institute of Technology (ETH), Gloriastrasse 35, 8092 Zurich, Switzerland

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CS : Computer Society
IEEE-EDS : Electronic Devices Society
IEEE-CAS : Circuits & Systems

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 8, Downloads (12 Months): 20, Citation Count: 6

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/288548.289117 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis. Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons, 1995.
	2	Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
	3	J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4), 1994.
	4	J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
	5	Patrice Godefroid , David E. Long, Symbolic Protocol Verification with Queue BDDs, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.198, July 27-30, 1996
	6	Alan J. Hu , David L. Dill, Efficient Verification with BDDs using Implicitly Conjoined Invariants, Proceedings of the 5th International Conference on Computer Aided Verification, p.3-14, June 28-July 01, 1993
	7	G. Kahn. The semantics of a simple language for parallel programming. In Proceedings of the IFIP Congress information Processing, 1974.
	8	G. Kahn and D. B. MacQueen. Coroutines and networks of parallel processes. In Proceedings of the IFIP Congress Information Processing, 1977.
	9	R. M. Karp and R. E. Miller. Properties of a model for parallel computations: Determinacy, termination, and queueing. SIAM Journal on Applied Mathematics, 14(6):1390-1411, 1966.
	10	Edward Ashford Lee , David G. Messerschmitt, Static scheduling of synchronous data flow programs for digital signal processing, IEEE Transactions on Computers, v.36 n.1, p.24-35, Jan. 1987 [doi>10.1109/TC.1987.5009446]
	11	E.A. Lee and T. M. Parks. Dataflow process networks. Proceedings of the IEEE, 83(5):773-799, 1995.
	12	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	13	Thomas Martyn Parks, Bounded scheduling of process networks, University of California at Berkeley, Berkeley, CA, 1996
	14	A. Srinivasan, T. Kam, S. Malik, and R. K. Brayton. Algorithms for discrete function manipulation. In Proceedings of the IEEE International Conference on Computer Aided Design, 1990.
	15	K. Strehl and L. Thiele. Symbolic model checking using interval diagram techniques. Technical Report 40, Computer Engineering and Networks Lab (TIK), Swiss Federal Institute of Technology (ETH) Zurich, Gloriastrasse 35, CH-8092 Zurich, February 1998.

CITED BY 6

	L. Thiele , K. Strehl , D. Ziegenbein , R. Ernst , J. Teich, FunState—an internal design representation for codesign, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.558-565, November 07-11, 1999, San Jose, California, United States
	Luis Alejandro Cortés , Petru Eles , Zebo Peng, Verification of embedded systems using a petri net based representation, Proceedings of the 13th international symposium on System synthesis, September 20-22, 2000, Madrid, Spain
	Karsten Strehl , Lothar Thiele , Dirk Ziegenbein , Rolf Ernst , Jürgen Teich, Scheduling hardware/software systems using symbolic techniques, Proceedings of the seventh international workshop on Hardware/software codesign, p.173-177, March 1999, Rome, Italy
	Kim G. Larsen , Justin Pearson , Carsten Weise , Wang Yi, Clock difference diagrams, Nordic Journal of Computing, v.6 n.3, p.271-298, Fall 1999
	Tobias Amnell , Gerd Behrmann , Johan Bengtsson , Pedro R. D'Argenio , Alexandre David , Ansgar Fehnker , Thomas Hune , Bertrand Jeannet , Kim G. Larsen , M. Oliver Möller , Paul Pettersson , Carsten Weise , Wang Yi, UPPAAL: now, next, and future, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
	Karsten Strehl , Lothar Thiele, Interval diagram techniques for symbolic model checking of Petri nets, Proceedings of the conference on Design, automation and test in Europe, p.14-es, January 1999, Munich, Germany

INDEX TERMS

Primary Classification:
C. Computer Systems Organization

Additional Classification:
J. Computer Applications

General Terms:
Design, Experimentation, Measurement, Performance, Theory, Verification

Collaborative Colleagues:

Karsten Strehl: colleagues

Lothar Thiele: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player