Changil Choe

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Trends

Author Order

Document Type

Co-Authors

Hyejong Hong

Yonsei University

Kukhwan Kim

O Hyong-Chol

Dang Van Hung

Vietnam National University, Hanoi

Song Han

Shanghai University of Engineering Science

Kim Kukhwan

Kim Munchol

Cooperative Institutions

Vietnam National University, Hanoi

Le Quy Don Technical University

VNU University of Science

University of Engineering and Technology Lahore

PRG S&Tech (South Korea)

Hanoi University

United Nations University Institute on Globalization, Culture and Mobility

Software (Spain)

Nation University

Institute of Software

Author Statistics

Papers

Citation

H-Index

i-10 index

Research Field

Verification of N-M Switching Control System Using LTL Model Checking

ASME Press eBooks (2013)

Changil Choe Kim Kukhwan Kim Munchol

Production factories in which stable voltage is critical, e.g., electro-plating factory, require constantly stable voltage to minimize loss by adjusting incoming voltage in real time, even if low-quality electricity is supplied from outside. To solve such problem often being raised from the factories located in the area with unstable electricity supply, we designed N-M switching control system and verified its correctness using LTL model checking technique.

Factory (object-oriented programming)

10.1115/1.860182_ch16

Cite

Citations (0)

On Verification of Linear Occurrence Properties of Real-Time Systems

Electronic Notes in Theoretical Computer Science (2008)

Changil Choe Dang Van Hung

Duration Calculus of Weakly Monotonic Time (WDC) is an extension of DC to allow description of discrete processes where several steps of computation can occur at the same time point. In this paper, we introduce Linear Occurrence Invariants (LOI) using WDC and give an algorithm to check real-time automata for LOI by solving integer programming problems. LOI can be used effectively to specify system requirements in some cases including when the system is considered under the true synchrony assumption. We also extend WDC probabilistically to express dependability requirements of real-time systems and develop a technique to check deterministic probabilistic real-time automata for a class of probabilistic WDC formulas.

Probabilistic automaton

10.1016/j.entcs.2008.03.088

Cite

Citations (2)

Formal Design and Verification of N-M Switching Control System

arXiv (Cornell University) (2012)

Changil Choe Hyejong Hong Kukhwan Kim

10.48550/arxiv.1212.2789

Cite

Citations (0)

Approximate Model Checking of Real-Time Systems for Linear Duration Invariants

Serdica Journal of Computing (2013)

Changil Choe O Hyong-Chol Song Han

Real-time systems are usually modelled with timed automata and real-time requirements relating to the state durations of the system are often specifiable using Linear Duration Invariants, which is a decidable subclass of Duration Calculus formulas. Various algorithms have been developed to check timed automata or real-time automata for linear duration invariants, but each needs complicated preprocessing and exponential calculation. To the best of our knowledge, these algorithms have not been implemented. In this paper, we present an approximate model checking technique based on a genetic algorithm to check real-time automata for linear durration invariants in reasonable times. Genetic algorithm is a good optimization method when a problem needs massive computation and it works particularly well in our case because the fitness function which is derived from the linear duration invariant is linear. ACM Computing Classification System (1998): D.2.4, C.3.

10.55630/sjc.2013.7.1-12

Cite

Citations (0)

VERIFICATION OF N-M SWITCHING CONTROL SYSTEM: A CASE STUDY IN TEMPORAL LOGIC MODEL CHECKING

Changil Choe Hyejong Hong Kukhwan Kim

Production factories in which stable voltage is critical, e.g., electro-plating factory, require constantly stable voltage to minimize loss by adjusting incoming voltage in real time even if low-quality electricity is supplied from outside. To solve such problem often being raised from the factories located in the area with unstable electricity supply, we designed N-M switching control system and verified its correctness using LTL model checking. Mathematics Subject Classification 2010 : 03B44, 68Q60

Factory (object-oriented programming)

Control logic

Source

Cite

Citations (0)