Open AccessDeductive Verification of Telecommunication Systems Written in C
Author(s) -
I. S. Anureev
Publication year - 2015
Publication title -
modelirovanie i analiz informacionnyh sistem
Language(s) - English
Resource type - Journals
eISSN - 2313-5417
pISSN - 1818-1015
DOI - 10.18255/1818-1015-2012-6-34-44
Subject(s) - computer science , extension (predicate logic) , protocol (science) , programming language , reduction (mathematics) , functional verification , formal verification , mathematics , medicine , alternative medicine , geometry , pathology
A deductive approach to verification of telecommunication systems written in C is proposed. The approach is based on the extension of C by declarative statements and on reduction of verification of parallel communicating components of these systems to separate verification of components written in this extension. An example of verification of a data link protocol is considered.