Invariants in symbolic modeling and verification of requirements

Author

Letichevsky, Alexander ; Godlevsky, Alexander ; Guba, Anton ; Kolchin, Alexander ; Letychevskyi, Oleksandr ; Peschanenko, Vladimir

Author_Institution

V.M. Glushkov Inst. of Cybern., Kiev, Ukraine

fYear

2013

fDate

23-27 Sept. 2013

Firstpage

1

Lastpage

6

Abstract

The paper presents the usage of invariants technique for symbolic modeling and verification of requirements for reactive systems. It includes checking of the safety, completeness, liveness, and consistency properties, deadlocks and livelocks detection. The paper describes the iterative method of double approximation and the method of undetermined coefficients for invariants generation. Benefits, disadvantages and comparison of this technique with existing methods are considered. The paper is illustrated by examples of invariants technique usage for symbolic verification.

Keywords

approximation theory; iterative methods; program verification; system recovery; completeness properties; consistency properties; deadlock detection; double approximation; invariant generation; iterative method; livelock detection; liveness properties; reactive system requirements; reactive systems; safety properties; symbolic modeling; symbolic verification; Abstracts; Approximation methods; Computational modeling; Cybernetics; Iterative methods; Polynomials; Protocols; Invariants; basic protocols; lower and upper approximation; requirements; symbolic modeling; verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Science and Information Technologies (CSIT), 2013

Conference_Location

Yerevan

Print_ISBN

978-1-4799-2460-8

Type

conf

DOI

10.1109/CSITechnol.2013.6710332

Filename

6710332