Specification and validation of dynamic systems using temporal logic

S. M. Cho, H. H. Kim, Sungdeok Cha, D. H. Bae

Research output: Contribution to journalArticle

9 Citations (Scopus)

Abstract

A specification and validation technique for dynamic systems is proposed. In particular, a new temporal logic, called HDTL, is presented and the tableau method revised for automatic analysis. Using a freeze quantifier, HDTL with the revised tableau method makes it possible to specify the correctness requirements of dynamic systems and validate them. The proposed logic is rather generic, i.e. it has only a few assumptions on operational language. The authors introduce a simple dynamic modelling language and illustrate its experiment. The experiment shows that HDTL is suitable for specifying dynamic properties and the analysis technique is promising.

Original languageEnglish
Pages (from-to)135-140
Number of pages6
JournalIEE Proceedings: Software
Volume148
Issue number4
DOIs
Publication statusPublished - 2001 Aug 1
Externally publishedYes

Fingerprint

Temporal logic
Dynamical systems
Specifications
Experiments
Modeling languages

ASJC Scopus subject areas

  • Computer Graphics and Computer-Aided Design
  • Software

Cite this

Specification and validation of dynamic systems using temporal logic. / Cho, S. M.; Kim, H. H.; Cha, Sungdeok; Bae, D. H.

In: IEE Proceedings: Software, Vol. 148, No. 4, 01.08.2001, p. 135-140.

Research output: Contribution to journalArticle

Cho, S. M. ; Kim, H. H. ; Cha, Sungdeok ; Bae, D. H. / Specification and validation of dynamic systems using temporal logic. In: IEE Proceedings: Software. 2001 ; Vol. 148, No. 4. pp. 135-140.
@article{0e9d3a1c64894cd587f6b2a5833b42e2,
title = "Specification and validation of dynamic systems using temporal logic",
abstract = "A specification and validation technique for dynamic systems is proposed. In particular, a new temporal logic, called HDTL, is presented and the tableau method revised for automatic analysis. Using a freeze quantifier, HDTL with the revised tableau method makes it possible to specify the correctness requirements of dynamic systems and validate them. The proposed logic is rather generic, i.e. it has only a few assumptions on operational language. The authors introduce a simple dynamic modelling language and illustrate its experiment. The experiment shows that HDTL is suitable for specifying dynamic properties and the analysis technique is promising.",
author = "Cho, {S. M.} and Kim, {H. H.} and Sungdeok Cha and Bae, {D. H.}",
year = "2001",
month = "8",
day = "1",
doi = "10.1049/ip-sen:20010558",
language = "English",
volume = "148",
pages = "135--140",
journal = "IET Software",
issn = "1751-8806",
publisher = "Institution of Engineering and Technology",
number = "4",

}

TY - JOUR

T1 - Specification and validation of dynamic systems using temporal logic

AU - Cho, S. M.

AU - Kim, H. H.

AU - Cha, Sungdeok

AU - Bae, D. H.

PY - 2001/8/1

Y1 - 2001/8/1

N2 - A specification and validation technique for dynamic systems is proposed. In particular, a new temporal logic, called HDTL, is presented and the tableau method revised for automatic analysis. Using a freeze quantifier, HDTL with the revised tableau method makes it possible to specify the correctness requirements of dynamic systems and validate them. The proposed logic is rather generic, i.e. it has only a few assumptions on operational language. The authors introduce a simple dynamic modelling language and illustrate its experiment. The experiment shows that HDTL is suitable for specifying dynamic properties and the analysis technique is promising.

AB - A specification and validation technique for dynamic systems is proposed. In particular, a new temporal logic, called HDTL, is presented and the tableau method revised for automatic analysis. Using a freeze quantifier, HDTL with the revised tableau method makes it possible to specify the correctness requirements of dynamic systems and validate them. The proposed logic is rather generic, i.e. it has only a few assumptions on operational language. The authors introduce a simple dynamic modelling language and illustrate its experiment. The experiment shows that HDTL is suitable for specifying dynamic properties and the analysis technique is promising.

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

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

U2 - 10.1049/ip-sen:20010558

DO - 10.1049/ip-sen:20010558

M3 - Article

VL - 148

SP - 135

EP - 140

JO - IET Software

JF - IET Software

SN - 1751-8806

IS - 4

ER -