BulDML at Institute of Mathematics and Informatics >
IMI Periodicals >
Serdica Journal of Computing >
2013 >
Volume 7 Number 1 >

Please use this identifier to cite or link to this item:

Title: Approximate Model Checking of Real-Time Systems for Linear Duration Invariants
Authors: Choe, Changil
O., Hyong-Chol
Han, Song
Keywords: Approximate Model Checking
Real-Time System
Linear Duration Invariant
Genetic Algorithm
Issue Date: 2013
Publisher: Institute of Mathematics and Informatics Bulgarian Academy of Sciences
Citation: Serdica Journal of Computing, Vol. 7, No 1, (2013), 1p-12p
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.
ISSN: 1312-6555
Appears in Collections:Volume 7 Number 1

Files in This Item:

File Description SizeFormat
sjc-vol7-num1-2013-p1-p12.pdf150.35 kBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.


Valid XHTML 1.0!   Creative Commons License