Geodesic
Approximate Model Checking of Real-Time Systems for Linear Duration Invariants
Serdica Journal of Computing, Tome 7 (2013) no. 1, pp. 1-12.

Voir la notice de l'article provenant de la source Bulgarian Digital Mathematics Library

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.
Keywords: Approximate Model Checking, Verification, Real-Time System, Linear Duration Invariant, Genetic Algorithm 
@article{SJC_2013_7_1_a0,
     author = {Choe, Changil and O., Hyong-Chol and Han, Song},
     title = {Approximate {Model} {Checking} of {Real-Time} {Systems} for {Linear} {Duration} {Invariants}},
     journal = {Serdica Journal of Computing},
     pages = {1--12},
     publisher = {mathdoc},
     volume = {7},
     number = {1},
     year = {2013},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/SJC_2013_7_1_a0/}
}
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
SP  - 1
EP  - 12
VL  - 7
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/SJC_2013_7_1_a0/
LA  - en
ID  - SJC_2013_7_1_a0
ER  - 
%0 Journal Article
%A Choe, Changil
%A O., Hyong-Chol
%A Han, Song
%T Approximate Model Checking of Real-Time Systems for Linear Duration Invariants
%J Serdica Journal of Computing
%D 2013
%P 1-12
%V 7
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/SJC_2013_7_1_a0/
%G en
%F SJC_2013_7_1_a0
Choe, Changil; O., Hyong-Chol; Han, Song. Approximate Model Checking of Real-Time Systems for Linear Duration Invariants. Serdica Journal of Computing, Tome 7 (2013) no. 1, pp. 1-12. http://geodesic.mathdoc.fr/item/SJC_2013_7_1_a0/