Formal Specification Based Automatic Test Generation for Embedded Network Systems

Embedded systems have become increasingly connected and communicate with each other, forming large-scaled and complicated network systems. To make their design and testing more reliable and robust, this paper proposes a formal specification language called SENS and a SENS-based automatic test genera...

Full description

Saved in:
Bibliographic Details
Main Authors: Eun Hye Choi, Hideaki Nishihara, Takahiro Ando, Nguyen Van Tang, Masahiro Aoki, Keiichi Yoshisaka, Osamu Mizuno, Hitoshi Ohsaki
Format: Article
Language:English
Published: Wiley 2014-01-01
Series:Journal of Applied Mathematics
Online Access:http://dx.doi.org/10.1155/2014/909762
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1849306122252451840
author Eun Hye Choi
Hideaki Nishihara
Takahiro Ando
Nguyen Van Tang
Masahiro Aoki
Keiichi Yoshisaka
Osamu Mizuno
Hitoshi Ohsaki
author_facet Eun Hye Choi
Hideaki Nishihara
Takahiro Ando
Nguyen Van Tang
Masahiro Aoki
Keiichi Yoshisaka
Osamu Mizuno
Hitoshi Ohsaki
author_sort Eun Hye Choi
collection DOAJ
description Embedded systems have become increasingly connected and communicate with each other, forming large-scaled and complicated network systems. To make their design and testing more reliable and robust, this paper proposes a formal specification language called SENS and a SENS-based automatic test generation tool called TGSENS. Our approach is summarized as follows: (1) A user describes requirements of target embedded network systems by logical property-based constraints using SENS. (2) Given SENS specifications, test cases are automatically generated using a SAT-based solver. Filtering mechanisms to select efficient test cases are also available in our tool. (3) In addition, given a testing goal by the user, test sequences are automatically extracted from exhaustive test cases. We’ve implemented our approach and conducted several experiments on practical case studies. Through the experiments, we confirmed the efficiency of our approach in design and test generation of real embedded air-conditioning network systems.
format Article
id doaj-art-3958d2b4d4e5439081b3fe5f0e017f1b
institution Kabale University
issn 1110-757X
1687-0042
language English
publishDate 2014-01-01
publisher Wiley
record_format Article
series Journal of Applied Mathematics
spelling doaj-art-3958d2b4d4e5439081b3fe5f0e017f1b2025-08-20T03:55:11ZengWileyJournal of Applied Mathematics1110-757X1687-00422014-01-01201410.1155/2014/909762909762Formal Specification Based Automatic Test Generation for Embedded Network SystemsEun Hye Choi0Hideaki Nishihara1Takahiro Ando2Nguyen Van Tang3Masahiro Aoki4Keiichi Yoshisaka5Osamu Mizuno6Hitoshi Ohsaki7National Institute of Advanced Industrial Science and Technology, JapanNational Institute of Advanced Industrial Science and Technology, JapanKyushu University, JapanHanoi University of Industry, VietnamDaikin Industries, Ltd., JapanDaikin Industries, Ltd., JapanKyoto Institute of Technology, JapanNational Institute of Advanced Industrial Science and Technology, JapanEmbedded systems have become increasingly connected and communicate with each other, forming large-scaled and complicated network systems. To make their design and testing more reliable and robust, this paper proposes a formal specification language called SENS and a SENS-based automatic test generation tool called TGSENS. Our approach is summarized as follows: (1) A user describes requirements of target embedded network systems by logical property-based constraints using SENS. (2) Given SENS specifications, test cases are automatically generated using a SAT-based solver. Filtering mechanisms to select efficient test cases are also available in our tool. (3) In addition, given a testing goal by the user, test sequences are automatically extracted from exhaustive test cases. We’ve implemented our approach and conducted several experiments on practical case studies. Through the experiments, we confirmed the efficiency of our approach in design and test generation of real embedded air-conditioning network systems.http://dx.doi.org/10.1155/2014/909762
spellingShingle Eun Hye Choi
Hideaki Nishihara
Takahiro Ando
Nguyen Van Tang
Masahiro Aoki
Keiichi Yoshisaka
Osamu Mizuno
Hitoshi Ohsaki
Formal Specification Based Automatic Test Generation for Embedded Network Systems
Journal of Applied Mathematics
title Formal Specification Based Automatic Test Generation for Embedded Network Systems
title_full Formal Specification Based Automatic Test Generation for Embedded Network Systems
title_fullStr Formal Specification Based Automatic Test Generation for Embedded Network Systems
title_full_unstemmed Formal Specification Based Automatic Test Generation for Embedded Network Systems
title_short Formal Specification Based Automatic Test Generation for Embedded Network Systems
title_sort formal specification based automatic test generation for embedded network systems
url http://dx.doi.org/10.1155/2014/909762
work_keys_str_mv AT eunhyechoi formalspecificationbasedautomatictestgenerationforembeddednetworksystems
AT hideakinishihara formalspecificationbasedautomatictestgenerationforembeddednetworksystems
AT takahiroando formalspecificationbasedautomatictestgenerationforembeddednetworksystems
AT nguyenvantang formalspecificationbasedautomatictestgenerationforembeddednetworksystems
AT masahiroaoki formalspecificationbasedautomatictestgenerationforembeddednetworksystems
AT keiichiyoshisaka formalspecificationbasedautomatictestgenerationforembeddednetworksystems
AT osamumizuno formalspecificationbasedautomatictestgenerationforembeddednetworksystems
AT hitoshiohsaki formalspecificationbasedautomatictestgenerationforembeddednetworksystems