DefinePK

Abstract

In this paper, the question on the expediency of checking the model, the model checking method is applied to, is discussed. To this end, corresponding technique has been proposed. Named technique is based on differentiation between the concepts of analytical plane of model perception and the concepts of corresponding implementation plane. The technique is grounded on the following constituents: Kripke structure - for analytical interpretation of formal specification; Temporal Logic of Actions and corresponding formalism - as the instruments for shifting from the analytical plane to the implementation one; TLC model checker - to examine the correctness of formal specification – with respect to the concepts of implementation plane. To prove the proposed technique, the case study has been conducted. To this end, the algorithms from the spacecraft domain have been considered. To verify the resulting specifications, two alternative implementations of TLC model checker have been applied.