A technique for checking the adequacy of formal model (CROSBI ID 299569)
Prilog u časopisu | izvorni znanstveni rad | međunarodna recenzija
Podaci o odgovornosti
Shkarupylo, Vadym ; Alsayaydeh, Jamil Abedalrahim Jamil ; Tomicic, Igor ; Chemeris, Alexander ; Dusheba, Valentyna
engleski
A technique for checking the adequacy of formal model
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.
adequacy ; correctness ; formal specification ; model checking ; TLA ; TLC
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o izdanju
16 (16)
2021.
1707-1719
objavljeno
1819-6608
1819-6608