Naslov
A technique for checking the adequacy of formal model

Autori
Shkarupylo, Vadym ; Alsayaydeh, Jamil Abedalrahim Jamil ; Tomicic, Igor ; Chemeris, Alexander ; Dusheba, Valentyna

Izvornik
ARPN Journal of Engineering and Applied Sciences (1819-6608) 16 (2021), 16; 1707-1719

Vrsta, podvrsta i kategorija rada
Radovi u časopisima, članak, znanstveni

Ključne riječi
adequacy ; correctness ; formal specification ; model checking ; TLA ; TLC

Sažetak
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.

Izvorni jezik
Engleski

Znanstvena područja
Računarstvo

POVEZANOST RADA