Deductive Verification of Telecommunication Systems Written in C

Abstract

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.

Keywords

• verification
• specification
• operational semantics
• axiomatic semantics
• transformational semantics
• telecommunication systems
• telecommunication protocols