scholarly journals Usage of Invariants for Symbolic Verification of Requirements

10.29007/2nr2 ◽  
2018 ◽  
Author(s):  
Alexander Letichevsky ◽  
Alexander Godlevsky ◽  
Anton Guba ◽  
Alexander Kolchin ◽  
Oleksandr Letychevskyi ◽  
...  
Keyword(s):  
Iterative Method ◽  
Reactive Systems ◽  
Consistency Properties ◽  
Double Approximation ◽  
Symbolic Verification

The paper presents the usage of invariants for symbolic verification of requirements for reactive systems. It includes checking of safety, incompleteness, liveness, consistency properties, and livelock 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.

Quality Improvement of X-ray CT Images by Estimation of the Mechanical Misalignment in a Projection Image Using an Iterative Method

2017 ◽  
Vol 137 (3) ◽  
pp. 213-219
Author(s):  
Kenji Noguchi ◽  
Satoshi Takahashi ◽  
Daisuke Suzuki ◽  
Atsushi Teramoto
Keyword(s):  
Quality Improvement ◽  
Iterative Method ◽  
Ct Images ◽  
X Ray ◽  
Projection Image

THE REALIZATION OF THE ITERATIVE METHOD OF THE LEAST SQUARES FOR THE ESTIMATION OF STATIC OBJECT PARAMETERS IN MATLAB ENVIRONMENT

2017 ◽  
pp. 28-36
Author(s):  
Galina Vasil’evna Troshina ◽  
Alexander Aleksandrovich Voevoda
Keyword(s):  
Parameter Estimation ◽  
Iterative Method ◽  
Least Squares ◽  
Input Signal ◽  
Layer Structure ◽  
Estimation Procedure ◽  
Parameter Estimation Procedure ◽  
Noise Simulation ◽  
Static Object ◽  
Object Parameters

It was suggested to use the system model working in real time for an iterative method of the parameter estimation. It gives the chance to select a suitable input signal, and also to carry out the setup of the object parameters. The object modeling for a case when the system isn't affected by the measurement noises, and also for a case when an object is under the gaussian noise was executed in the MatLab environment. The superposition of two meanders with different periods and single amplitude is used as an input signal. The model represents the three-layer structure in the MatLab environment. On the most upper layer there are units corresponding to the simulation of an input signal, directly the object, the unit of the noise simulation and the unit for the parameter estimation. The second and the third layers correspond to the simulation of the iterative method of the least squares. The diagrams of the input and the output signals in the absence of noise and in the presence of noise are shown. The results of parameter estimation of a static object are given. According to the results of modeling, the algorithm works well even in the presence of significant measurement noise. To verify the correctness of the work of an algorithm the auxiliary computations have been performed and the diagrams of the gain behavior amount which is used in the parameter estimation procedure have been constructed. The entry conditions which are necessary for the work of an iterative method of the least squares are specified. The understanding of this algorithm functioning principles is a basis for its subsequent use for the parameter estimation of the multi-channel dynamic objects.

An adaptive chebyshev iterative method

2018 ◽  
Vol 30 (10) ◽  
pp. 67-85
Author(s):  
V. Zhukov ◽  
◽  
O. Feodoritova ◽  
N. Novikova ◽  
◽  
...  
Keyword(s):  
Iterative Method

An Iterative Method for Restoring Noisy Blurred Images.

1984 ◽  
Author(s):  
A. K. Katsaggelos ◽  
J. Biemond ◽  
R. M. Mersereau ◽  
R. W. Schafer
Keyword(s):  
Iterative Method ◽  
Blurred Images
Sign in / Sign up

Export Citation Format

Share Document