Title :
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
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;
Conference_Titel :
Computer Science and Information Technologies (CSIT), 2013
Conference_Location :
Yerevan
Print_ISBN :
978-1-4799-2460-8
DOI :
10.1109/CSITechnol.2013.6710332
