Behavior verification of hybrid real-time requirements by qualitative formalism

Jang Soo Lee, Sungdeok Cha

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

2 Citations (Scopus)

Abstract

Although modern control theories have been successfully applied to solve a variety of problems, they are often mathematically and physically too specific to describe and analyze the qualitative properties of hybrid real-time systems. In this paper, we propose the use of qualitative formal methods, Compositional Modeling Language (CML) and Causal Functional Representation Language (CFRL) in particular, to specify continuous plant dynamics and the required behavior respectively. The system behavior has been simulated by a qualitative simulator known as the Device Modeling Environment (DME), and verified against the required behavior. Using the Electrical Power System (EPS) as an example, we demonstrate the effectiveness of our approach by illustrating how a simple SCR-style specification can be transformed and analyzed.

Original languageEnglish
Title of host publicationProceedings of the International Workshop on Real-Time Computing Systems and Applications/RTCSA
Editors Anon
Place of PublicationPiscataway, NJ, United States
PublisherIEEE
Pages127-134
Number of pages8
Publication statusPublished - 1997 Dec 1
Externally publishedYes
EventProceedings of the 1997 4th International Workshop on Real-Time Computing Systems and Applications, RTCSA - Taipei, Taiwan
Duration: 1997 Oct 271997 Oct 29

Other

OtherProceedings of the 1997 4th International Workshop on Real-Time Computing Systems and Applications, RTCSA
CityTaipei, Taiwan
Period97/10/2797/10/29

Fingerprint

Formal methods
Real time systems
Thyristors
Control theory
Simulators
Specifications
Modeling languages

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

Lee, J. S., & Cha, S. (1997). Behavior verification of hybrid real-time requirements by qualitative formalism. In Anon (Ed.), Proceedings of the International Workshop on Real-Time Computing Systems and Applications/RTCSA (pp. 127-134). Piscataway, NJ, United States: IEEE.

Behavior verification of hybrid real-time requirements by qualitative formalism. / Lee, Jang Soo; Cha, Sungdeok.

Proceedings of the International Workshop on Real-Time Computing Systems and Applications/RTCSA. ed. / Anon. Piscataway, NJ, United States : IEEE, 1997. p. 127-134.

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

Lee, JS & Cha, S 1997, Behavior verification of hybrid real-time requirements by qualitative formalism. in Anon (ed.), Proceedings of the International Workshop on Real-Time Computing Systems and Applications/RTCSA. IEEE, Piscataway, NJ, United States, pp. 127-134, Proceedings of the 1997 4th International Workshop on Real-Time Computing Systems and Applications, RTCSA, Taipei, Taiwan, 97/10/27.
Lee JS, Cha S. Behavior verification of hybrid real-time requirements by qualitative formalism. In Anon, editor, Proceedings of the International Workshop on Real-Time Computing Systems and Applications/RTCSA. Piscataway, NJ, United States: IEEE. 1997. p. 127-134
Lee, Jang Soo ; Cha, Sungdeok. / Behavior verification of hybrid real-time requirements by qualitative formalism. Proceedings of the International Workshop on Real-Time Computing Systems and Applications/RTCSA. editor / Anon. Piscataway, NJ, United States : IEEE, 1997. pp. 127-134
@inproceedings{464b79cff55c4a078262d73c02c5d685,
title = "Behavior verification of hybrid real-time requirements by qualitative formalism",
abstract = "Although modern control theories have been successfully applied to solve a variety of problems, they are often mathematically and physically too specific to describe and analyze the qualitative properties of hybrid real-time systems. In this paper, we propose the use of qualitative formal methods, Compositional Modeling Language (CML) and Causal Functional Representation Language (CFRL) in particular, to specify continuous plant dynamics and the required behavior respectively. The system behavior has been simulated by a qualitative simulator known as the Device Modeling Environment (DME), and verified against the required behavior. Using the Electrical Power System (EPS) as an example, we demonstrate the effectiveness of our approach by illustrating how a simple SCR-style specification can be transformed and analyzed.",
author = "Lee, {Jang Soo} and Sungdeok Cha",
year = "1997",
month = "12",
day = "1",
language = "English",
pages = "127--134",
editor = "Anon",
booktitle = "Proceedings of the International Workshop on Real-Time Computing Systems and Applications/RTCSA",
publisher = "IEEE",

}

TY - GEN

T1 - Behavior verification of hybrid real-time requirements by qualitative formalism

AU - Lee, Jang Soo

AU - Cha, Sungdeok

PY - 1997/12/1

Y1 - 1997/12/1

N2 - Although modern control theories have been successfully applied to solve a variety of problems, they are often mathematically and physically too specific to describe and analyze the qualitative properties of hybrid real-time systems. In this paper, we propose the use of qualitative formal methods, Compositional Modeling Language (CML) and Causal Functional Representation Language (CFRL) in particular, to specify continuous plant dynamics and the required behavior respectively. The system behavior has been simulated by a qualitative simulator known as the Device Modeling Environment (DME), and verified against the required behavior. Using the Electrical Power System (EPS) as an example, we demonstrate the effectiveness of our approach by illustrating how a simple SCR-style specification can be transformed and analyzed.

AB - Although modern control theories have been successfully applied to solve a variety of problems, they are often mathematically and physically too specific to describe and analyze the qualitative properties of hybrid real-time systems. In this paper, we propose the use of qualitative formal methods, Compositional Modeling Language (CML) and Causal Functional Representation Language (CFRL) in particular, to specify continuous plant dynamics and the required behavior respectively. The system behavior has been simulated by a qualitative simulator known as the Device Modeling Environment (DME), and verified against the required behavior. Using the Electrical Power System (EPS) as an example, we demonstrate the effectiveness of our approach by illustrating how a simple SCR-style specification can be transformed and analyzed.

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

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

M3 - Conference contribution

AN - SCOPUS:0031359054

SP - 127

EP - 134

BT - Proceedings of the International Workshop on Real-Time Computing Systems and Applications/RTCSA

A2 - Anon, null

PB - IEEE

CY - Piscataway, NJ, United States

ER -