Model Checking: Verification or Debugging?

Theo C. Ruys; Ed Brinksma

Model Checking: Verification or Debugging?

Theo C. Ruys
, Ed Brinksma

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

93 Downloads (Pure)

Abstract

Model checking tools are increasingly being used for the validation of real-life systems in an industrial context. This paper discusses two validation approaches with respect to the application of model checkers. The verification approach tries to ascertain the correctness of a formal model of a system, whereas the debugging approach tries to find errors in the model. This paper discusses the differences between the two complementing approaches and shows for each approach its advantages and disadvantages.

Original language	English
Title of host publication	Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2000
Subtitle of host publication	Las Vegas, Nevada, USA, June 26-29, 2000
Editors	H.R. Arabnia
Publisher	CSREA Press
Pages	3009-3015
Number of pages	7
ISBN (Print)	1-892512-51-3
Publication status	Published - 2000
Event	International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2000 - Las Vegas, United States Duration: 26 Jun 2000 → 29 Jun 2000

Conference

Conference	International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2000
Abbreviated title	PDPTA 2000
Country/Territory	United States
City	Las Vegas
Period	26/06/00 → 29/06/00

Access to Document

Ruys2000modelFinal published version, 163 KB

Model Checking: Verification or Debugging?
Ruys, T. C. (Keynote speaker) & Brinksma, E. (Keynote speaker)
27 Jun 2000
Activity: Talk or presentation › Oral presentation

Cite this

@inproceedings{8b5b65698fa546ee9f252c61bcf5251c,

title = "Model Checking: Verification or Debugging?",

abstract = "Model checking tools are increasingly being used for the validation of real-life systems in an industrial context. This paper discusses two validation approaches with respect to the application of model checkers. The verification approach tries to ascertain the correctness of a formal model of a system, whereas the debugging approach tries to find errors in the model. This paper discusses the differences between the two complementing approaches and shows for each approach its advantages and disadvantages.",

author = "Ruys, \{Theo C.\} and Ed Brinksma",

year = "2000",

language = "English",

isbn = "1-892512-51-3",

pages = "3009--3015",

editor = "H.R. Arabnia",

booktitle = "Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2000",

publisher = "CSREA Press",

note = "International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2000, PDPTA 2000 ; Conference date: 26-06-2000 Through 29-06-2000",

}

Ruys, TC & Brinksma, E 2000, Model Checking: Verification or Debugging? in HR Arabnia (ed.), Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2000: Las Vegas, Nevada, USA, June 26-29, 2000. CSREA Press, pp. 3009-3015, International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2000, Las Vegas, Nevada, United States, 26/06/00.

Model Checking: Verification or Debugging? / Ruys, Theo C.; Brinksma, Ed.
Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2000: Las Vegas, Nevada, USA, June 26-29, 2000. ed. / H.R. Arabnia. CSREA Press, 2000. p. 3009-3015.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Model Checking

T2 - International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2000

AU - Ruys, Theo C.

AU - Brinksma, Ed

PY - 2000

Y1 - 2000

N2 - Model checking tools are increasingly being used for the validation of real-life systems in an industrial context. This paper discusses two validation approaches with respect to the application of model checkers. The verification approach tries to ascertain the correctness of a formal model of a system, whereas the debugging approach tries to find errors in the model. This paper discusses the differences between the two complementing approaches and shows for each approach its advantages and disadvantages.

AB - Model checking tools are increasingly being used for the validation of real-life systems in an industrial context. This paper discusses two validation approaches with respect to the application of model checkers. The verification approach tries to ascertain the correctness of a formal model of a system, whereas the debugging approach tries to find errors in the model. This paper discusses the differences between the two complementing approaches and shows for each approach its advantages and disadvantages.

M3 - Conference contribution

SN - 1-892512-51-3

SP - 3009

EP - 3015

BT - Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2000

A2 - Arabnia, H.R.

PB - CSREA Press

Y2 - 26 June 2000 through 29 June 2000

ER -

Model Checking: Verification or Debugging?

Abstract

Conference

Access to Document

Fingerprint

Activities

Model Checking: Verification or Debugging?

Cite this