Verification of embedded system by a method for detecting defects in source codes using model checking

Yoshitaka Aoki, Saeko Matsuura

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

Abstract

We have proposed a method based on model checking for detecting hard-to-discover defects in enterprise systems. We apply our method to embedded system development to easily discover some defects caused by input/output data of the hardware which are influenced by the external environment before the software is integrated into the hardware. This paper discuss the effectiveness of our method using a case study to develop a line tracing robot.

Original languageEnglish
Title of host publicationISCI 2011 - 2011 IEEE Symposium on Computers and Informatics
Pages530-535
Number of pages6
DOIs
Publication statusPublished - 2011
Event2011 IEEE Symposium on Computers and Informatics, ISCI 2011 - Kuala Lumpur
Duration: 2011 Mar 202011 Mar 22

Other

Other2011 IEEE Symposium on Computers and Informatics, ISCI 2011
CityKuala Lumpur
Period11/3/2011/3/22

Fingerprint

Model checking
Embedded systems
Hardware
Defects
Robots
Industry

Keywords

  • Model checking
  • Process Modeling
  • Software debugging
  • Software tools
  • system verification

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Information Systems

Cite this

Aoki, Y., & Matsuura, S. (2011). Verification of embedded system by a method for detecting defects in source codes using model checking. In ISCI 2011 - 2011 IEEE Symposium on Computers and Informatics (pp. 530-535). [5958972] https://doi.org/10.1109/ISCI.2011.5958972

Verification of embedded system by a method for detecting defects in source codes using model checking. / Aoki, Yoshitaka; Matsuura, Saeko.

ISCI 2011 - 2011 IEEE Symposium on Computers and Informatics. 2011. p. 530-535 5958972.

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

Aoki, Y & Matsuura, S 2011, Verification of embedded system by a method for detecting defects in source codes using model checking. in ISCI 2011 - 2011 IEEE Symposium on Computers and Informatics., 5958972, pp. 530-535, 2011 IEEE Symposium on Computers and Informatics, ISCI 2011, Kuala Lumpur, 11/3/20. https://doi.org/10.1109/ISCI.2011.5958972
Aoki, Yoshitaka ; Matsuura, Saeko. / Verification of embedded system by a method for detecting defects in source codes using model checking. ISCI 2011 - 2011 IEEE Symposium on Computers and Informatics. 2011. pp. 530-535
@inproceedings{98fb1b514ec5445f8002c72834429b48,
title = "Verification of embedded system by a method for detecting defects in source codes using model checking",
abstract = "We have proposed a method based on model checking for detecting hard-to-discover defects in enterprise systems. We apply our method to embedded system development to easily discover some defects caused by input/output data of the hardware which are influenced by the external environment before the software is integrated into the hardware. This paper discuss the effectiveness of our method using a case study to develop a line tracing robot.",
keywords = "Model checking, Process Modeling, Software debugging, Software tools, system verification",
author = "Yoshitaka Aoki and Saeko Matsuura",
year = "2011",
doi = "10.1109/ISCI.2011.5958972",
language = "English",
isbn = "9781612846903",
pages = "530--535",
booktitle = "ISCI 2011 - 2011 IEEE Symposium on Computers and Informatics",

}

TY - GEN

T1 - Verification of embedded system by a method for detecting defects in source codes using model checking

AU - Aoki, Yoshitaka

AU - Matsuura, Saeko

PY - 2011

Y1 - 2011

N2 - We have proposed a method based on model checking for detecting hard-to-discover defects in enterprise systems. We apply our method to embedded system development to easily discover some defects caused by input/output data of the hardware which are influenced by the external environment before the software is integrated into the hardware. This paper discuss the effectiveness of our method using a case study to develop a line tracing robot.

AB - We have proposed a method based on model checking for detecting hard-to-discover defects in enterprise systems. We apply our method to embedded system development to easily discover some defects caused by input/output data of the hardware which are influenced by the external environment before the software is integrated into the hardware. This paper discuss the effectiveness of our method using a case study to develop a line tracing robot.

KW - Model checking

KW - Process Modeling

KW - Software debugging

KW - Software tools

KW - system verification

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

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

U2 - 10.1109/ISCI.2011.5958972

DO - 10.1109/ISCI.2011.5958972

M3 - Conference contribution

AN - SCOPUS:80052125542

SN - 9781612846903

SP - 530

EP - 535

BT - ISCI 2011 - 2011 IEEE Symposium on Computers and Informatics

ER -