Applying Model Checking to Concurrent Object-Oriented Software

Seung Mo Cho; Doo Hwan Bae; Sung Deok Cha; Young Gon Kim; Byung Kyu Yoo; Sang Taek Kim

doi:10.1109/ISADS.1999.838464

Applying Model Checking to Concurrent Object-Oriented Software

Seung Mo Cho
, Doo Hwan Bae
, Sung Deok Cha
, Young Gon Kim
, Byung Kyu Yoo
, Sang Taek Kim

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

7 Citations (Scopus)

Abstract

Model checking is a formal verification technique which checks the consistency between a requirement specification and a behavior model of the system by explorating the state space of the model. We apply model checking to formal verification of concurrent object-oriented systems, using an existing model checker SPIN which has been successful in verifying parallel systems. First, we propose an Actor-based modeling language, called APromela, by extending a modeling language Promela which is a modeling language supported in SPIN. APromela supports not only all the primitives of Promela, but additional primitives needed to model concurrent object-oriented systems, such as class definition, object instantiation, message send, and synchronization. Second, we provide translation rules for mapping APromela's such modeling primitives to Promela's. By giving an example of specification, translation, and verification, we also demonstrate the applicability of our proposed approach, and discuss the limitations and further research issues.

Original language	English
Title of host publication	Proceedings - 4th International Symposium on Autonomous Decentralized Systems
Subtitle of host publication	Integration of Heterogeneous Systems, ISADS 1999
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	380-383
Number of pages	4
ISBN (Electronic)	0769501370, 9780769501376
DOIs	https://doi.org/10.1109/ISADS.1999.838464
Publication status	Published - 1999
Externally published	Yes
Event	4th International Symposium on Autonomous Decentralized Systems, ISADS 1999 - Tokyo, Japan Duration: 1999 Mar 21 → 1999 Mar 23

Publication series

Name	Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999

Conference

Conference	4th International Symposium on Autonomous Decentralized Systems, ISADS 1999
Country/Territory	Japan
City	Tokyo
Period	99/3/21 → 99/3/23

Bibliographical note

Publisher Copyright:
© 1999 Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999. All rights reserved.

ASJC Scopus subject areas

Computer Networks and Communications
Information Systems

Access to Document

10.1109/ISADS.1999.838464

Cite this

Cho, S. M., Bae, D. H., Cha, S. D., Kim, Y. G., Yoo, B. K., & Kim, S. T. (1999). Applying Model Checking to Concurrent Object-Oriented Software. In Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999 (pp. 380-383). (Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ISADS.1999.838464

Applying Model Checking to Concurrent Object-Oriented Software. / Cho, Seung Mo; Bae, Doo Hwan; Cha, Sung Deok et al.
Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999. Institute of Electrical and Electronics Engineers Inc., 1999. p. 380-383 (Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999).

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

Cho, SM, Bae, DH, Cha, SD, Kim, YG, Yoo, BK & Kim, ST 1999, Applying Model Checking to Concurrent Object-Oriented Software. in Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999. Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999, Institute of Electrical and Electronics Engineers Inc., pp. 380-383, 4th International Symposium on Autonomous Decentralized Systems, ISADS 1999, Tokyo, Japan, 99/3/21. https://doi.org/10.1109/ISADS.1999.838464

Cho SM, Bae DH, Cha SD, Kim YG, Yoo BK, Kim ST. Applying Model Checking to Concurrent Object-Oriented Software. In Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999. Institute of Electrical and Electronics Engineers Inc. 1999. p. 380-383. (Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999). doi: 10.1109/ISADS.1999.838464

Cho, Seung Mo ; Bae, Doo Hwan ; Cha, Sung Deok et al. / Applying Model Checking to Concurrent Object-Oriented Software. Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999. Institute of Electrical and Electronics Engineers Inc., 1999. pp. 380-383 (Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999).

@inproceedings{2b72da03b3b84d64b7ea7ad3395851e1,

title = "Applying Model Checking to Concurrent Object-Oriented Software",

abstract = "Model checking is a formal verification technique which checks the consistency between a requirement specification and a behavior model of the system by explorating the state space of the model. We apply model checking to formal verification of concurrent object-oriented systems, using an existing model checker SPIN which has been successful in verifying parallel systems. First, we propose an Actor-based modeling language, called APromela, by extending a modeling language Promela which is a modeling language supported in SPIN. APromela supports not only all the primitives of Promela, but additional primitives needed to model concurrent object-oriented systems, such as class definition, object instantiation, message send, and synchronization. Second, we provide translation rules for mapping APromela's such modeling primitives to Promela's. By giving an example of specification, translation, and verification, we also demonstrate the applicability of our proposed approach, and discuss the limitations and further research issues.",

author = "Cho, \{Seung Mo\} and Bae, \{Doo Hwan\} and Cha, \{Sung Deok\} and Kim, \{Young Gon\} and Yoo, \{Byung Kyu\} and Kim, \{Sang Taek\}",

note = "Publisher Copyright: {\textcopyright} 1999 Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999. All rights reserved.; 4th International Symposium on Autonomous Decentralized Systems, ISADS 1999 ; Conference date: 21-03-1999 Through 23-03-1999",

year = "1999",

doi = "10.1109/ISADS.1999.838464",

language = "English",

series = "Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999",

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

pages = "380--383",

booktitle = "Proceedings - 4th International Symposium on Autonomous Decentralized Systems",

}

TY - GEN

T1 - Applying Model Checking to Concurrent Object-Oriented Software

AU - Cho, Seung Mo

AU - Bae, Doo Hwan

AU - Cha, Sung Deok

AU - Kim, Young Gon

AU - Yoo, Byung Kyu

AU - Kim, Sang Taek

PY - 1999

Y1 - 1999

N2 - Model checking is a formal verification technique which checks the consistency between a requirement specification and a behavior model of the system by explorating the state space of the model. We apply model checking to formal verification of concurrent object-oriented systems, using an existing model checker SPIN which has been successful in verifying parallel systems. First, we propose an Actor-based modeling language, called APromela, by extending a modeling language Promela which is a modeling language supported in SPIN. APromela supports not only all the primitives of Promela, but additional primitives needed to model concurrent object-oriented systems, such as class definition, object instantiation, message send, and synchronization. Second, we provide translation rules for mapping APromela's such modeling primitives to Promela's. By giving an example of specification, translation, and verification, we also demonstrate the applicability of our proposed approach, and discuss the limitations and further research issues.

AB - Model checking is a formal verification technique which checks the consistency between a requirement specification and a behavior model of the system by explorating the state space of the model. We apply model checking to formal verification of concurrent object-oriented systems, using an existing model checker SPIN which has been successful in verifying parallel systems. First, we propose an Actor-based modeling language, called APromela, by extending a modeling language Promela which is a modeling language supported in SPIN. APromela supports not only all the primitives of Promela, but additional primitives needed to model concurrent object-oriented systems, such as class definition, object instantiation, message send, and synchronization. Second, we provide translation rules for mapping APromela's such modeling primitives to Promela's. By giving an example of specification, translation, and verification, we also demonstrate the applicability of our proposed approach, and discuss the limitations and further research issues.

UR - https://www.scopus.com/pages/publications/10444251440

U2 - 10.1109/ISADS.1999.838464

DO - 10.1109/ISADS.1999.838464

M3 - Conference contribution

AN - SCOPUS:10444251440

T3 - Proceedings - 4th International Symposium on Autonomous Decentralized Systems: Integration of Heterogeneous Systems, ISADS 1999

SP - 380

EP - 383

BT - Proceedings - 4th International Symposium on Autonomous Decentralized Systems

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 4th International Symposium on Autonomous Decentralized Systems, ISADS 1999

Y2 - 21 March 1999 through 23 March 1999

ER -

Applying Model Checking to Concurrent Object-Oriented Software

Abstract

Publication series

Conference

Bibliographical note

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this