TS-U: Temporal-spatial methodology for application checking of the systems in the ubiquitous environment

Fran Jarnjak, Jinhyung Kim, Yixin Jing, Hoh In, Dongwon Jeong, Doo Kwon Baik

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

Abstract

In the paper a novel methodology, TS-U, is proposed based on existing model checking techniques that were extended to successfully model the systems in a ubiquitous environment by introducing time and space constraints relevant in modeling of some ubiquitous system for its validation. Method proposed requires only slight modification of the existing model checking tools by introducing the notion of a Transition Checking Matrix (TCM) which holds time and space constraints for model's transitions. By applying TS-U methodology, regular CTL formulae can be used without modifications to successfully check the system's model as in the traditional model checking based on the Kripke structure.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages161-170
Number of pages10
Volume3823 LNCS
DOIs
Publication statusPublished - 2005 Dec 1
EventEUC 2005 Workshops: UISW, NCUS, SecUbiq, USN, and TAUES - Nagasaki, Japan
Duration: 2005 Dec 62005 Dec 9

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3823 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

OtherEUC 2005 Workshops: UISW, NCUS, SecUbiq, USN, and TAUES
CountryJapan
CityNagasaki
Period05/12/605/12/9

Fingerprint

Model checking
Model Checking
Space Simulation
Methodology
Transition Model
Modeling
Model

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Jarnjak, F., Kim, J., Jing, Y., In, H., Jeong, D., & Baik, D. K. (2005). TS-U: Temporal-spatial methodology for application checking of the systems in the ubiquitous environment. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3823 LNCS, pp. 161-170). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3823 LNCS). https://doi.org/10.1007/11596042_17

TS-U : Temporal-spatial methodology for application checking of the systems in the ubiquitous environment. / Jarnjak, Fran; Kim, Jinhyung; Jing, Yixin; In, Hoh; Jeong, Dongwon; Baik, Doo Kwon.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 3823 LNCS 2005. p. 161-170 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3823 LNCS).

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

Jarnjak, F, Kim, J, Jing, Y, In, H, Jeong, D & Baik, DK 2005, TS-U: Temporal-spatial methodology for application checking of the systems in the ubiquitous environment. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 3823 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3823 LNCS, pp. 161-170, EUC 2005 Workshops: UISW, NCUS, SecUbiq, USN, and TAUES, Nagasaki, Japan, 05/12/6. https://doi.org/10.1007/11596042_17
Jarnjak F, Kim J, Jing Y, In H, Jeong D, Baik DK. TS-U: Temporal-spatial methodology for application checking of the systems in the ubiquitous environment. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 3823 LNCS. 2005. p. 161-170. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/11596042_17
Jarnjak, Fran ; Kim, Jinhyung ; Jing, Yixin ; In, Hoh ; Jeong, Dongwon ; Baik, Doo Kwon. / TS-U : Temporal-spatial methodology for application checking of the systems in the ubiquitous environment. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 3823 LNCS 2005. pp. 161-170 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{f8220c47c89245d5821d36b1bd593074,
title = "TS-U: Temporal-spatial methodology for application checking of the systems in the ubiquitous environment",
abstract = "In the paper a novel methodology, TS-U, is proposed based on existing model checking techniques that were extended to successfully model the systems in a ubiquitous environment by introducing time and space constraints relevant in modeling of some ubiquitous system for its validation. Method proposed requires only slight modification of the existing model checking tools by introducing the notion of a Transition Checking Matrix (TCM) which holds time and space constraints for model's transitions. By applying TS-U methodology, regular CTL formulae can be used without modifications to successfully check the system's model as in the traditional model checking based on the Kripke structure.",
author = "Fran Jarnjak and Jinhyung Kim and Yixin Jing and Hoh In and Dongwon Jeong and Baik, {Doo Kwon}",
year = "2005",
month = "12",
day = "1",
doi = "10.1007/11596042_17",
language = "English",
isbn = "3540308032",
volume = "3823 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "161--170",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - TS-U

T2 - Temporal-spatial methodology for application checking of the systems in the ubiquitous environment

AU - Jarnjak, Fran

AU - Kim, Jinhyung

AU - Jing, Yixin

AU - In, Hoh

AU - Jeong, Dongwon

AU - Baik, Doo Kwon

PY - 2005/12/1

Y1 - 2005/12/1

N2 - In the paper a novel methodology, TS-U, is proposed based on existing model checking techniques that were extended to successfully model the systems in a ubiquitous environment by introducing time and space constraints relevant in modeling of some ubiquitous system for its validation. Method proposed requires only slight modification of the existing model checking tools by introducing the notion of a Transition Checking Matrix (TCM) which holds time and space constraints for model's transitions. By applying TS-U methodology, regular CTL formulae can be used without modifications to successfully check the system's model as in the traditional model checking based on the Kripke structure.

AB - In the paper a novel methodology, TS-U, is proposed based on existing model checking techniques that were extended to successfully model the systems in a ubiquitous environment by introducing time and space constraints relevant in modeling of some ubiquitous system for its validation. Method proposed requires only slight modification of the existing model checking tools by introducing the notion of a Transition Checking Matrix (TCM) which holds time and space constraints for model's transitions. By applying TS-U methodology, regular CTL formulae can be used without modifications to successfully check the system's model as in the traditional model checking based on the Kripke structure.

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

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

U2 - 10.1007/11596042_17

DO - 10.1007/11596042_17

M3 - Conference contribution

AN - SCOPUS:33744899348

SN - 3540308032

SN - 9783540308034

VL - 3823 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 161

EP - 170

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -