IEICE TRANSACTIONS on Information
Model Checking of Embedded Assembly Program Based on Simulation
Summary :
Embedded systems have been widely used. In addition, embedded systems have been gradually complicated. It is important to ensure the safety for embedded software by software model checking. We have developed a verification system for verifying embedded assembly programs. It generates exact Kripke structure by exhaustively and dynamically simulating assembly programs, and simultaneously verify it by model checking. In addition, we have introduced undefined values to reduce the number of states in order to avoid the state space explosion.
- Publication
- IEICE TRANSACTIONS on Information Vol.E100-D No.8 pp.1819-1826
- Publication Date
- 2017/08/01
- Publicized
- 2017/05/12
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.2016EDP7452
- Type of Manuscript
- PAPER
- Category
- Software Engineering
Authors
Satoshi YAMANE
Kanazawa University
Ryosuke KONOSHITA
Kanazawa University
Tomonori KATO
Kanazawa University
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Satoshi YAMANE, Ryosuke KONOSHITA, Tomonori KATO, "Model Checking of Embedded Assembly Program Based on Simulation" in IEICE TRANSACTIONS on Information,
vol. E100-D, no. 8, pp. 1819-1826, August 2017, doi: 10.1587/transinf.2016EDP7452.
Abstract: Embedded systems have been widely used. In addition, embedded systems have been gradually complicated. It is important to ensure the safety for embedded software by software model checking. We have developed a verification system for verifying embedded assembly programs. It generates exact Kripke structure by exhaustively and dynamically simulating assembly programs, and simultaneously verify it by model checking. In addition, we have introduced undefined values to reduce the number of states in order to avoid the state space explosion.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2016EDP7452/_p
Copy
@ARTICLE{e100-d_8_1819,
author={Satoshi YAMANE, Ryosuke KONOSHITA, Tomonori KATO, },
journal={IEICE TRANSACTIONS on Information},
title={Model Checking of Embedded Assembly Program Based on Simulation},
year={2017},
volume={E100-D},
number={8},
pages={1819-1826},
abstract={Embedded systems have been widely used. In addition, embedded systems have been gradually complicated. It is important to ensure the safety for embedded software by software model checking. We have developed a verification system for verifying embedded assembly programs. It generates exact Kripke structure by exhaustively and dynamically simulating assembly programs, and simultaneously verify it by model checking. In addition, we have introduced undefined values to reduce the number of states in order to avoid the state space explosion.},
keywords={},
doi={10.1587/transinf.2016EDP7452},
ISSN={1745-1361},
month={August},}
Copy
TY - JOUR
TI - Model Checking of Embedded Assembly Program Based on Simulation
T2 - IEICE TRANSACTIONS on Information
SP - 1819
EP - 1826
AU - Satoshi YAMANE
AU - Ryosuke KONOSHITA
AU - Tomonori KATO
PY - 2017
DO - 10.1587/transinf.2016EDP7452
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E100-D
IS - 8
JA - IEICE TRANSACTIONS on Information
Y1 - August 2017
AB - Embedded systems have been widely used. In addition, embedded systems have been gradually complicated. It is important to ensure the safety for embedded software by software model checking. We have developed a verification system for verifying embedded assembly programs. It generates exact Kripke structure by exhaustively and dynamically simulating assembly programs, and simultaneously verify it by model checking. In addition, we have introduced undefined values to reduce the number of states in order to avoid the state space explosion.
ER -
English
