Model checking software requirement specifications using domain reduction abstraction

Yunja Choi; Mats Heimdahl

doi:10.1109/ASE.2003.1240328

Model checking software requirement specifications using domain reduction abstraction

Yunja Choi, Mats Heimdahl

University of Minnesota Twin Cities

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

11 Scopus citations

Abstract

As an automated verification and validation tool, model checking can be quite effective in practice. Nevertheless, model checking has been quite inefficient when dealing with systems with data variables over a large (or infinite) domain, which is a serious limiting factor for its applicability in practice. To address this issue, we have investigated a static abstraction technique, domain reduction abstraction, based on data equivalence and trajectory reduction, and implemented it as a prototype extension of the symbolic model checker NuSMV. Unlike on-the-fly dynamic abstraction techniques, domain reduction abstraction statically analyzes specifications and automatically produces an abstract model which can be reused over time-a feature suitable for regression verification.

Original language	English
Title of host publication	Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	314-317
Number of pages	4
ISBN (Electronic)	0769520359, 9780769520353
DOIs	https://doi.org/10.1109/ASE.2003.1240328
State	Published - 2003
Event	18th IEEE International Conference on Automated Software Engineering, ASE 2003 - Montreal, Canada Duration: 6 Oct 2003 → 10 Oct 2003

Publication series

Name	Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003

Conference

Conference	18th IEEE International Conference on Automated Software Engineering, ASE 2003
Country/Territory	Canada
City	Montreal
Period	6/10/03 → 10/10/03

Access to Document

10.1109/ASE.2003.1240328

Cite this

Choi, Y., & Heimdahl, M. (2003). Model checking software requirement specifications using domain reduction abstraction. In Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003 (pp. 314-317). (Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ASE.2003.1240328

Choi, Yunja ; Heimdahl, Mats. / Model checking software requirement specifications using domain reduction abstraction. Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003. Institute of Electrical and Electronics Engineers Inc., 2003. pp. 314-317 (Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003).

@inproceedings{1c642456e54e4a63870c7c312b1e63b0,

title = "Model checking software requirement specifications using domain reduction abstraction",

abstract = "As an automated verification and validation tool, model checking can be quite effective in practice. Nevertheless, model checking has been quite inefficient when dealing with systems with data variables over a large (or infinite) domain, which is a serious limiting factor for its applicability in practice. To address this issue, we have investigated a static abstraction technique, domain reduction abstraction, based on data equivalence and trajectory reduction, and implemented it as a prototype extension of the symbolic model checker NuSMV. Unlike on-the-fly dynamic abstraction techniques, domain reduction abstraction statically analyzes specifications and automatically produces an abstract model which can be reused over time-a feature suitable for regression verification.",

author = "Yunja Choi and Mats Heimdahl",

note = "Publisher Copyright: {\textcopyright} 2003 IEEE; 18th IEEE International Conference on Automated Software Engineering, ASE 2003 ; Conference date: 06-10-2003 Through 10-10-2003",

year = "2003",

doi = "10.1109/ASE.2003.1240328",

language = "English",

series = "Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "314--317",

booktitle = "Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003",

address = "United States",

}

Choi, Y & Heimdahl, M 2003, Model checking software requirement specifications using domain reduction abstraction. in Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003. Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003, Institute of Electrical and Electronics Engineers Inc., pp. 314-317, 18th IEEE International Conference on Automated Software Engineering, ASE 2003, Montreal, Canada, 6/10/03. https://doi.org/10.1109/ASE.2003.1240328

Model checking software requirement specifications using domain reduction abstraction. / Choi, Yunja; Heimdahl, Mats.
Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003. Institute of Electrical and Electronics Engineers Inc., 2003. p. 314-317 (Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003).

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

TY - GEN

T1 - Model checking software requirement specifications using domain reduction abstraction

AU - Choi, Yunja

AU - Heimdahl, Mats

PY - 2003

Y1 - 2003

N2 - As an automated verification and validation tool, model checking can be quite effective in practice. Nevertheless, model checking has been quite inefficient when dealing with systems with data variables over a large (or infinite) domain, which is a serious limiting factor for its applicability in practice. To address this issue, we have investigated a static abstraction technique, domain reduction abstraction, based on data equivalence and trajectory reduction, and implemented it as a prototype extension of the symbolic model checker NuSMV. Unlike on-the-fly dynamic abstraction techniques, domain reduction abstraction statically analyzes specifications and automatically produces an abstract model which can be reused over time-a feature suitable for regression verification.

AB - As an automated verification and validation tool, model checking can be quite effective in practice. Nevertheless, model checking has been quite inefficient when dealing with systems with data variables over a large (or infinite) domain, which is a serious limiting factor for its applicability in practice. To address this issue, we have investigated a static abstraction technique, domain reduction abstraction, based on data equivalence and trajectory reduction, and implemented it as a prototype extension of the symbolic model checker NuSMV. Unlike on-the-fly dynamic abstraction techniques, domain reduction abstraction statically analyzes specifications and automatically produces an abstract model which can be reused over time-a feature suitable for regression verification.

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

U2 - 10.1109/ASE.2003.1240328

DO - 10.1109/ASE.2003.1240328

M3 - Conference contribution

AN - SCOPUS:84908342880

T3 - Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003

SP - 314

EP - 317

BT - Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 18th IEEE International Conference on Automated Software Engineering, ASE 2003

Y2 - 6 October 2003 through 10 October 2003

ER -

Choi Y, Heimdahl M. Model checking software requirement specifications using domain reduction abstraction. In Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003. Institute of Electrical and Electronics Engineers Inc. 2003. p. 314-317. (Proceedings - 18th IEEE International Conference on Automated Software Engineering, ASE 2003). doi: 10.1109/ASE.2003.1240328

Model checking software requirement specifications using domain reduction abstraction

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this