Formal Verification of Real-Time Systems with Data Processing

Authors

  • Tamás Tóth
    Affiliation
    Budapest University of Technology and Economics, Department of Measurement and Information Systems, Fault Tolerant Systems Research Group
  • István Majzik
    Affiliation
    Budapest University of Technology and Economics, Department of Measurement and Information Systems, Fault Tolerant Systems Research Group
https://doi.org/10.3311/PPee.9766

Abstract

The behavior of practical safety critical systems often combines real-time behavior with structured data flow. To ensure correctness of such systems, both aspects have to be modeled and formally verified. Time related behavior can be efficiently modeled and analyzed in terms of timed automata. At the same time, program verification techniques like abstract interpretation and software model checking can efficiently handle data flow. In this paper, we describe a simple formalism that represents both aspects of such systems in a uniform and explicit way, thus enables the combination of formal analysis methods for real-time systems and software using standard techniques.

Keywords:

model checking, abstract interpretation, abstraction refinement, timed automata, control flow automata

Citation data from Crossref and Scopus

Published Online

2017-05-23

How to Cite

Tóth, T., Majzik, I. “Formal Verification of Real-Time Systems with Data Processing”, Periodica Polytechnica Electrical Engineering and Computer Science, 61(2), pp. 166–174, 2017. https://doi.org/10.3311/PPee.9766

Issue

Section

Articles