Символдық верификация


Бұл жүйе үшін барлық мүмкін болатын өткелдер өткелдің төрт жағдайымен анықталады



бет7/9
Дата01.08.2020
өлшемі20.24 Kb.
1   2   3   4   5   6   7   8   9

Бұл жүйе үшін барлық мүмкін болатын өткелдер өткелдің төрт жағдайымен анықталады:

Бұл жүйе үшін барлық мүмкін болатын өткелдер өткелдің төрт жағдайымен анықталады:

1. Немесе фермердің өзі бір жағалаудан екінші жағалауға өтуі мүмкін. Немесе фермер бір жағалаудан екінші жағалауға тасымалдануы мүмкін:

2. тек қасқыр;

немесе

3. тек ешкі;

немесе

4. тек қырыққабат.

CTL үшін Model Checking символдық алгоритмы

CTL үшін model checking әдісімен верификациялау міндеті келесіден тұрады: Крипке М құрылымы және тармақталған уақыт логикасының (CTL) темпоралдық формуласы берілген. Ф орындалатын Крипке М құрылымының көптеген жағдайларын табу . Егер бастапқы жағдай S0 болса , онда Ф М үшін орындалады .



Достарыңызбен бөлісу:
1   2   3   4   5   6   7   8   9




©engime.org 2020
әкімшілігінің қараңыз

    Басты бет