Официалната проверка е

Официалната проверкае официално доказателство за съответствие или несъответствие на официалния обект на проверка с неговото официално описание. Предметът е алгоритми, програми и други доказателства.

Поради рутинния характер дори на простата формална проверка и теоретичната възможност за пълната им автоматизация, формалната проверка обикновено означава автоматична проверка с помощта на програма.

Съдържание

Обосновка

Софтуерното тестване не може да докаже, че дадена система, алгоритъм или програма не съдържа никакви грешки и дефекти и отговаря на определено свойство. Това може да стане чрезофициалнапроверка.

Области на използване

Официалната проверка може да се използва за проверка на системи като софтуер с изходен код, криптографски протоколи, комбинаторни логически схеми, цифрови схеми с вътрешна памет.

Теоретична основа

Верификацията е формално доказателство върху абстрактен математически модел на системата, при допускането, че съответствието между математическия модел и природата на системата се счита за първоначално дадено. Например за изграждане на модел или математически анализ и доказателство за коректността на алгоритми и програми.

Примери за математически обекти, често използвани за моделиране и формална проверка на програми и системи са:

формална семантика на езиците за програмиране, например операционна семантика, денотационна семантика, аксиоматична семантика (логиката на Хоаре), [математическа семантика на програмите].
държавна машина
етикетирано състояние и модел на преход
нетоПетри
машина на времето
хибриден автоматик
процесно смятане
структурирани алгоритми
структурирани програми

Подходи за формална проверка

Съществуват следните подходи за официална проверка:

формална семантика на езиците за програмиране
проверка на модела
логически извод
символично изпълнение
абстрактно тълкуване
систематичен анализ на алгоритми и програми
технологии за програмиране, базирани на доказателства

Програмиране, основано на доказателства

Програмирането, основано на доказателства, е технология, използвана в академичните среди през 80-те години на миналия век за разработване на програми за компютри с доказателства за коректност - доказателства за липсата на грешки в програмите (разбирайки, в рамките на тази теория, грешките като несъответствия между програмата и алгоритъма, който изпълнява).

Автоматична проверка на доказателство

Доказателството може да бъде напълно автоматизирано само за много малък кръг от прости теории, така че автоматичната му проверка и за това превръщането в проверима форма стават важни.

За да се запази строгостта при проверка на доказателство от верификатор, трябва да се провери и верификаторът, за което е необходим още един верификатор и т.н. Получената безкрайна верига от верификатори може да бъде свита чрез изграждане на самопроверяващ се верификатор, който има способността да се разгръща до практически такъв.

Литература

П. Грогоно, Програмиране на Паскал, М.: Мир, 1982, стр.295, (Тестване и проверка).

Фондация Уикимедия. 2010 г.

Вижте какво е "официална проверка" в други речници:

Проверка - Позитивизъм ... Уикипедия

проверка и одит - (Преход на ITIL услуга) Дейностите, отговорни за гарантиране, че информацията в системата за управление на конфигурацията е точна и че всички елементи на конфигурацията са дефинирани и записани. Проверката включва регламентирани ... ... Наръчник за технически преводач

Официална спецификация — В компютърните науки формалната спецификация е математическо описание на софтуерна или хардуерна система, която може да бъде внедрена съгласно това описание. Той определя какво трябва да прави системата, но не и как трябва да го прави ... ... Wikipedia

Подлежащи на проверка — Проверката може да означава малко по-различни неща в различните области на човешката дейност. Например: Верификацията (от латински verus true, facere да се направи) е потвърждение на съответствието на крайния продукт с предварително дефинирана препратка ... ... Wikipedia

Доказуемост - Проверката може да означава малко по-различни неща в различните области на човешката дейност. Например: Верификацията (от латински verus true, facere да се направи) е потвърждение на съответствието на крайния продукт с предварително дефинирана препратка ... ... Wikipedia

Проверяемост - Проверката може да означава малко по-различни неща в различните области на човешката дейност. Например: Верификацията (от латински verus true, facere да се направи) е потвърждение на съответствието на крайния продукт с предварително дефинирана препратка ... ... Wikipedia

Cadence Design Systems - Тип ... Wikipedia

Статичният анализ на кода е софтуерен анализ, извършен безреално изпълнение на изследваните програми (анализът, извършен с изпълнението на програмите, се нарича динамичен анализ на кода). В повечето случаи анализ ... ... Wikipedia

Логика на Хоар — (англ. Hoare logic, също Floyd Hoare logic, или Hoare rules) формална система с набор от логически правила, предназначени да докажат правилността на компютърните програми. Предложено е през 1969 г. от английски учен в ... ... Wikipedia

Софтуерно инженерство в чиста стая - Разработка на софтуер Процес на разработка на софтуер Анализ на стъпки на процеса • Дизайн • Програмиране • Документиране ... Wikipedia