Verifying software streaming systems

Ki Hyuk Nam, Jun Kil Park, Jin Young Choi, Jeong Joon Lee, Wan Choi

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

1 Citation (Scopus)

Abstract

Software streaming is an emerging technology that enables S/W applications to be executed on-demand without download and installation, so that the applications are available virtually everywhere in the network. In developing software streaming systems, the engine and protocols must be carefully designed since the performance and reliability of the streamed software are directly affected by that of streaming engine and network status. In this paper, we present the application of formal verification in the design and implementation of the software streaming systems to take precautions against any potential defects. To achieve this goal, we use the model checker SPIN to model and verify the base architecture and protocol of the system. The effects of the use of formal verification is much more satisfactory than we expected.

Original languageEnglish
Title of host publication8th International Conference Advanced Communication Technology, ICACT 2006 - Proceedings
Pages367-371
Number of pages5
Volume1
Publication statusPublished - 2006 Nov 17
Event8th International Conference Advanced Communication Technology, ICACT 2006 - Phoenix Park, Korea, Republic of
Duration: 2006 Feb 202006 Feb 22

Other

Other8th International Conference Advanced Communication Technology, ICACT 2006
CountryKorea, Republic of
CityPhoenix Park
Period06/2/2006/2/22

Fingerprint

Engines
Network protocols
Computer systems
Defects
Formal verification

Keywords

  • Feaver
  • Formal verification
  • Model checking
  • MODEX
  • Software streaming
  • SPIN

ASJC Scopus subject areas

  • Engineering(all)

Cite this

Nam, K. H., Park, J. K., Choi, J. Y., Lee, J. J., & Choi, W. (2006). Verifying software streaming systems. In 8th International Conference Advanced Communication Technology, ICACT 2006 - Proceedings (Vol. 1, pp. 367-371). [1625592]

Verifying software streaming systems. / Nam, Ki Hyuk; Park, Jun Kil; Choi, Jin Young; Lee, Jeong Joon; Choi, Wan.

8th International Conference Advanced Communication Technology, ICACT 2006 - Proceedings. Vol. 1 2006. p. 367-371 1625592.

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

Nam, KH, Park, JK, Choi, JY, Lee, JJ & Choi, W 2006, Verifying software streaming systems. in 8th International Conference Advanced Communication Technology, ICACT 2006 - Proceedings. vol. 1, 1625592, pp. 367-371, 8th International Conference Advanced Communication Technology, ICACT 2006, Phoenix Park, Korea, Republic of, 06/2/20.
Nam KH, Park JK, Choi JY, Lee JJ, Choi W. Verifying software streaming systems. In 8th International Conference Advanced Communication Technology, ICACT 2006 - Proceedings. Vol. 1. 2006. p. 367-371. 1625592
Nam, Ki Hyuk ; Park, Jun Kil ; Choi, Jin Young ; Lee, Jeong Joon ; Choi, Wan. / Verifying software streaming systems. 8th International Conference Advanced Communication Technology, ICACT 2006 - Proceedings. Vol. 1 2006. pp. 367-371
@inproceedings{fac5015cf5444defbc452849db1cbb54,
title = "Verifying software streaming systems",
abstract = "Software streaming is an emerging technology that enables S/W applications to be executed on-demand without download and installation, so that the applications are available virtually everywhere in the network. In developing software streaming systems, the engine and protocols must be carefully designed since the performance and reliability of the streamed software are directly affected by that of streaming engine and network status. In this paper, we present the application of formal verification in the design and implementation of the software streaming systems to take precautions against any potential defects. To achieve this goal, we use the model checker SPIN to model and verify the base architecture and protocol of the system. The effects of the use of formal verification is much more satisfactory than we expected.",
keywords = "Feaver, Formal verification, Model checking, MODEX, Software streaming, SPIN",
author = "Nam, {Ki Hyuk} and Park, {Jun Kil} and Choi, {Jin Young} and Lee, {Jeong Joon} and Wan Choi",
year = "2006",
month = "11",
day = "17",
language = "English",
isbn = "8955191294",
volume = "1",
pages = "367--371",
booktitle = "8th International Conference Advanced Communication Technology, ICACT 2006 - Proceedings",

}

TY - GEN

T1 - Verifying software streaming systems

AU - Nam, Ki Hyuk

AU - Park, Jun Kil

AU - Choi, Jin Young

AU - Lee, Jeong Joon

AU - Choi, Wan

PY - 2006/11/17

Y1 - 2006/11/17

N2 - Software streaming is an emerging technology that enables S/W applications to be executed on-demand without download and installation, so that the applications are available virtually everywhere in the network. In developing software streaming systems, the engine and protocols must be carefully designed since the performance and reliability of the streamed software are directly affected by that of streaming engine and network status. In this paper, we present the application of formal verification in the design and implementation of the software streaming systems to take precautions against any potential defects. To achieve this goal, we use the model checker SPIN to model and verify the base architecture and protocol of the system. The effects of the use of formal verification is much more satisfactory than we expected.

AB - Software streaming is an emerging technology that enables S/W applications to be executed on-demand without download and installation, so that the applications are available virtually everywhere in the network. In developing software streaming systems, the engine and protocols must be carefully designed since the performance and reliability of the streamed software are directly affected by that of streaming engine and network status. In this paper, we present the application of formal verification in the design and implementation of the software streaming systems to take precautions against any potential defects. To achieve this goal, we use the model checker SPIN to model and verify the base architecture and protocol of the system. The effects of the use of formal verification is much more satisfactory than we expected.

KW - Feaver

KW - Formal verification

KW - Model checking

KW - MODEX

KW - Software streaming

KW - SPIN

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

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

M3 - Conference contribution

AN - SCOPUS:33750938275

SN - 8955191294

SN - 9788955191295

VL - 1

SP - 367

EP - 371

BT - 8th International Conference Advanced Communication Technology, ICACT 2006 - Proceedings

ER -