Correctness debugging of message passing programs using model verification techniques

Robert Lovas, P. Kacsuk

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

Abstract

During the correctness debugging of non-deterministic message-passing programs the software engineers must face the probe effect, the irreproducibility, the completeness problem, and also the large state-space to be discovered. This work attempts to over-come the limitation of existing debugging solutions, and combines the traditional debugging methods with automated modeling and formal verification of parallel programs. The presented debugging framework provides user-friendly facilities for active control and highly automated observation mechanism for message passing programs based on formal methods; Petri-net modeling, partial ordering of state space, and temporal logic assertions.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages335-343
Number of pages9
Volume4757 LNCS
Publication statusPublished - 2007
Event14th European PVM/MPI Users' Group Meeting on Parallel Virtual Machine and Message Passing Interface - Paris, France
Duration: Sep 30 2007Oct 3 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4757 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other14th European PVM/MPI Users' Group Meeting on Parallel Virtual Machine and Message Passing Interface
CountryFrance
CityParis
Period9/30/0710/3/07

Fingerprint

Model Verification
Program Verification
Message passing
Debugging
Message Passing
Correctness
Facility Regulation and Control
Temporal logic
Formal methods
Petri nets
State Space
Software
Observation
Engineers
Partial ordering
Parallel Programs
Active Control
Formal Verification
Formal Methods
Temporal Logic

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Lovas, R., & Kacsuk, P. (2007). Correctness debugging of message passing programs using model verification techniques. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4757 LNCS, pp. 335-343). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4757 LNCS).

Correctness debugging of message passing programs using model verification techniques. / Lovas, Robert; Kacsuk, P.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4757 LNCS 2007. p. 335-343 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4757 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Lovas, R & Kacsuk, P 2007, Correctness debugging of message passing programs using model verification techniques. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 4757 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4757 LNCS, pp. 335-343, 14th European PVM/MPI Users' Group Meeting on Parallel Virtual Machine and Message Passing Interface, Paris, France, 9/30/07.
Lovas R, Kacsuk P. Correctness debugging of message passing programs using model verification techniques. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4757 LNCS. 2007. p. 335-343. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Lovas, Robert ; Kacsuk, P. / Correctness debugging of message passing programs using model verification techniques. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 4757 LNCS 2007. pp. 335-343 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{b4248bd373934415bf6f0c4473ac6a43,
title = "Correctness debugging of message passing programs using model verification techniques",
abstract = "During the correctness debugging of non-deterministic message-passing programs the software engineers must face the probe effect, the irreproducibility, the completeness problem, and also the large state-space to be discovered. This work attempts to over-come the limitation of existing debugging solutions, and combines the traditional debugging methods with automated modeling and formal verification of parallel programs. The presented debugging framework provides user-friendly facilities for active control and highly automated observation mechanism for message passing programs based on formal methods; Petri-net modeling, partial ordering of state space, and temporal logic assertions.",
author = "Robert Lovas and P. Kacsuk",
year = "2007",
language = "English",
isbn = "9783540754152",
volume = "4757 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "335--343",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Correctness debugging of message passing programs using model verification techniques

AU - Lovas, Robert

AU - Kacsuk, P.

PY - 2007

Y1 - 2007

N2 - During the correctness debugging of non-deterministic message-passing programs the software engineers must face the probe effect, the irreproducibility, the completeness problem, and also the large state-space to be discovered. This work attempts to over-come the limitation of existing debugging solutions, and combines the traditional debugging methods with automated modeling and formal verification of parallel programs. The presented debugging framework provides user-friendly facilities for active control and highly automated observation mechanism for message passing programs based on formal methods; Petri-net modeling, partial ordering of state space, and temporal logic assertions.

AB - During the correctness debugging of non-deterministic message-passing programs the software engineers must face the probe effect, the irreproducibility, the completeness problem, and also the large state-space to be discovered. This work attempts to over-come the limitation of existing debugging solutions, and combines the traditional debugging methods with automated modeling and formal verification of parallel programs. The presented debugging framework provides user-friendly facilities for active control and highly automated observation mechanism for message passing programs based on formal methods; Petri-net modeling, partial ordering of state space, and temporal logic assertions.

UR - http://www.scopus.com/inward/record.url?scp=38449090939&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=38449090939&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:38449090939

SN - 9783540754152

VL - 4757 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 335

EP - 343

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -