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

Choe, Changil; O., Hyong-Chol; Han, Song

Serdica Journal of Computing (2013)

- Volume: 7, Issue: 1, page 1-12
- ISSN: 1312-6555

## Access Full Article

top## Abstract

top## How to cite

topChoe, Changil, O., Hyong-Chol, and Han, Song. "Approximate Model Checking of Real-Time Systems for Linear Duration Invariants." Serdica Journal of Computing 7.1 (2013): 1-12. <http://eudml.org/doc/252267>.

@article{Choe2013,

abstract = {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.},

author = {Choe, Changil, O., Hyong-Chol, Han, Song},

journal = {Serdica Journal of Computing},

keywords = {Approximate Model Checking; Verification; Real-Time System; Linear Duration Invariant; Genetic Algorithm; approximate model checking; verification; real-time system; linear duration invariant; genetic algorithm},

language = {eng},

number = {1},

pages = {1-12},

publisher = {Institute of Mathematics and Informatics Bulgarian Academy of Sciences},

title = {Approximate Model Checking of Real-Time Systems for Linear Duration Invariants},

url = {http://eudml.org/doc/252267},

volume = {7},

year = {2013},

}

TY - JOUR

AU - Choe, Changil

AU - O., Hyong-Chol

AU - Han, Song

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

JO - Serdica Journal of Computing

PY - 2013

PB - Institute of Mathematics and Informatics Bulgarian Academy of Sciences

VL - 7

IS - 1

SP - 1

EP - 12

AB - 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.

LA - eng

KW - Approximate Model Checking; Verification; Real-Time System; Linear Duration Invariant; Genetic Algorithm; approximate model checking; verification; real-time system; linear duration invariant; genetic algorithm

UR - http://eudml.org/doc/252267

ER -

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.