Open AccessFormal Verification of Real-Time Systems with Data Processing
Author(s) -
Tamás Tóth,
István Majzik
Publication year - 2017
Publication title -
periodica polytechnica. electrical engineering and computer science
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.158
H-Index - 13
eISSN - 2064-5279
pISSN - 2064-5260
DOI - 10.3311/ppee.9766
Subject(s) - computer science , correctness , model checking , automaton , formal verification , data flow analysis , formalism (music) , formal methods , data flow diagram , abstract interpretation , software , programming language , theoretical computer science , real time computing , database , art , musical , visual arts
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.