On-the-Fly Model Checking of Program Runs for Automated Debugging

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by M. Frey Articles by B.-H. Schlingloff

24 th. EUROMICRO Conference Volume 1 (EUROMICRO'98)

Västerås, Sweden

August 25-August 27

ISBN: 0-8186-8646-4

	ASCII Text	x
	M. Frey, B.-H. Schlingloff, "On-the-Fly Model Checking of Program Runs for Automated Debugging," EUROMICRO Conference, vol. 1, pp. 10426, 24 th. EUROMICRO Conference Volume 1 (EUROMICRO'98), 1998.

	BibTex	x
	@article{ 10.1109/EURMIC.1998.711836, author = {M. Frey and B.-H. Schlingloff}, title = {On-the-Fly Model Checking of Program Runs for Automated Debugging}, journal ={EUROMICRO Conference}, volume = {1}, year = {1998}, issn = {1089-6503}, pages = {10426}, doi = {http://doi.ieeecomputersociety.org/10.1109/EURMIC.1998.711836}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - EUROMICRO Conference TI - On-the-Fly Model Checking of Program Runs for Automated Debugging SN - 1089-6503 SP EP A1 - M. Frey, A1 - B.-H. Schlingloff, PY - 1998 KW - null VL - 1 JA - EUROMICRO Conference ER -

M. Frey, Technische Universität München

B.-H. Schlingloff, Universität Bremen

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/EURMIC.1998.711836

In this paper, an on-the-fly algorithm is developed for model checking of temporal logic safety properties on partially ordered occurrence net structures. This algorithm is used for the automated debugging of parallel programs. During the monitoring of a program run, a state action net is constructed from the program trace. Temporal specifications are evaluated on-the-fly with respect to this net. The specifications can express e.g. that an error has occurred, or that certain control locations have been reached. When the specified condition can occur, the execution is halted. Since we use a partial order logic, specification violations can be detected even if they did not actually occur in the particular interleaving of the program run.

Citation:

M. Frey, B.-H. Schlingloff, "On-the-Fly Model Checking of Program Runs for Automated Debugging," euromicro, vol. 1, pp.10426, 24 th. EUROMICRO Conference Volume 1 (EUROMICRO'98), 1998

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.