Specification and Validation of Dynamic Systems Using Temporal Logic

A specification and validation technique for dynamic systems is proposed. In particular, a new temporal logic called HDTL, is presented and the tableau method revised for automatic analysis. Using a freeze quantifier, HDTL with the revised tableau method makes it possible to specify the correctness requirements of dynamic systems and validate them. The proposed logic is rather generic, i.e. it has only a few assumptions on operational language. The authors introduce a simple dynamic modelling language and illustrate its experiment. The experiment shows that HDTL is suitable for specifying dynamic properties and the analysis technique is promising
Publisher
Institution of Engineering and Technology
Issue Date
2001-08
Keywords

Dynamic systems; temporal logic

Citation

IEE Proceedings - Software, Vol.148, No.4, pp.135-140

ISSN
1462-5970
DOI
10.1049/ip-sen:20010558
URI
http://hdl.handle.net/10203/18431
Appears in Collection
CS-Journal Papers(저널논문)
  • Hit : 211
  • Download : 71
  • Cited 0 times in thomson ci

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0