Формальна верифікація

У Вікіпедії є статті про інші значення цього терміна: Верифікація (значення).

Форма́льна верифіка́ція — в інформаційних технологіях, доведення, або заперечення відповідності системи певній формальній специфікації або характеристиці, із використанням формальних методів математики[1].

Обґрунтування

Тестування програмного забезпечення не може довести, що система, алгоритм або програма не містить ніяких помилок і дефектів та задовольняє певним властивостям. Це може зробити формальна верифікація.

Сфери застосування

Формальна верифікація може використовуватися для перевірки таких систем, як програмне забезпечення, представлене у вигляді вихідних текстів, криптографічні протоколи, комбінаторні логічні схеми, цифрові схеми з внутрішньою пам'яттю.

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

Верифікація являє собою формальне доведення на абстрактній математичній моделі системи, в припущенні про те, що відповідність між математичною моделлю і природою системи вважається заданим. Наприклад, щодо побудованої моделі або математичного аналізу, доведення правильності алгоритмів і програм.

Прикладами математичних об'єктів, часто використовуваних для моделювання та формальної верифікації програм і систем, є:

Підходи до формальної верифікації

Існують такі підходи до формальної верифікації:

  • формальна семантика мов програмування
  • перевірка моделей (англ. model checking)
  • логічний висновок (англ. logical inference)
  • символьне виконання (англ. symbolic execution)
  • абстрактна інтерпретація
  • систематичний аналіз алгоритмів та програм
  • технології доказового програмування

Доказове програмування

Доказове програмування - використовувалось в 1980-х роках в академічних колах технології розробки програм для ЕОМ з доведеннями правильності - доведенням відсутності помилок у програмах (розуміючи, в рамках даної теорії, помилки як невідповідності між програмою і реалізованим нею алгоритмом).

Автоматична перевірка доведення

Доведення можна автоматизувати повністю лише для дуже невеликого кола простих теорій, тому зростає важливість його автоматичної перевірки і для цього зведення до належного вигляду.

Для підтримки строгості при перевірці доведення верифікатором слід перевірити ще й верифікатор, для чого потрібен ще один верифікатор і так далі. Отриманий нескінченний ланцюг верифікаторів можна було б згорнути, побудувавши самоверифіковний верифікатор, що володіє здатністю розвернутися до застосовного на практиці.

Див. також

Примітки

  1. ↑ Sanghavi, Alok (21 травня 2010). What is formal verification?. EE Times Asia.
  2. ↑ Introduction to Formal Verification, Berkeley University of California, Retrieved November 6, 2013


Інформаційні технології Це незавершена стаття про інформаційні технології.
Ви можете допомогти проєкту, виправивши або дописавши її.

Read other articles:

نصب تذكاري

  ميّز عن معلم تذكاري. نصب تذكاري النصب أو النصب التذكاري هو بناء أو موقع أو تمثال شيد لتخليد ذكرى شخص أو حادثة.[1][2] والنصب القومية هي أماكن لها أهمية تاريخية وعلمية، والمشاهد الخلابة التي تحافظ عليها الحكومة، باعتبارها ممتلكات شعبية. وتتضمّن هذه المباني القصو...

 

 

فريق الاستجابة للطوارئ المجتمعية

هذه المقالة يتيمة إذ تصل إليها مقالات أخرى قليلة جدًا. فضلًا، ساعد بإضافة وصلة إليها في مقالات متعلقة بها. (فبراير 2020) فريق الاستجابة للطوارئ المجتمعية تاريخ التأسيس 1993  الموقع الرسمي الموقع الرسمي  تعديل مصدري - تعديل   يمكن أن يشير فريق الاستجابة للطوارئ المجتمعية ...

 

 

ÖAF

This article includes a list of references, related reading, or external links, but its sources remain unclear because it lacks inline citations. Please help to improve this article by introducing more precise citations. (March 2021) (Learn how and when to remove this template message) Österreichische Automobil-FabrikCompany typeSubsidiary of MAN SEIndustryAutomotiveFounded1907HeadquartersFloridsdorf (Vienna), AustriaProductsvehiclesWebsiteOfficial Website ÖAF automobil ÖAF is an initialis...

Hotel Deluxe

Untuk hotel di Portland, Oregon, lihat Hotel deLuxe. Hotel DeluxeSutradaraVincent KokProduserRaymond WongSkenarioVincent KokAnselm ChanSteven FungPoon Jun LamPemeranRonald ChengSandra NgTeresa MoChapman ToRaymond WongFiona SitEric KotJim ChimLynn HungKarena NgMin Hun FungSinematograferCheung Man PoPenyuntingKwong Chi LeungPerusahaanproduksiPegasus Motion PicturesSil-Metropole OrganisationLe Vision PicturesHangzhou Tianma EntertainmentShanghai Hehe Entertainment InvestmentDistributorPegasus Mo...

 

 

2020 Arizona Democratic presidential primary

State election for the 2020 Democratic National Convention 2020 Arizona Democratic presidential primary ← 2016 March 17, 2020 2024 → ← MPFL →80 delegates (67 pledged, 13 unpledged)to the Democratic National ConventionThe number of pledged delegates won is determined by the popular vote   Candidate Joe Biden Bernie Sanders Home state Delaware Vermont Delegate count 38 29 Popular vote 268,029 200,456 Percentage 43.7% 32.7%   C...

 

 

The Man in the Glass Booth

The Man in the Glass BoothSampul DVDSutradaraArthur HillerProduserEly LandauDitulis olehEdward AnhaltRobert Shaw (novel & drama)PemeranMaximilian SchellLois NettletonLawrence PressmanSinematograferSam LeavittPenyuntingDavid BrethertonDistributorAmerican Film TheatreTanggal rilis 27 Januari 1975 (1975-01-27) Durasi117 menitNegaraAmerika SerikatBahasaInggris The Man in the Glass Booth adalah sebuah film drama Amerika 1975 garapan Arthur Hiller. Film tersebut diproduksi dan dirilis seba...

Wrestling at the 1924 Summer Olympics – Men's Greco-Roman light heavyweight

Wrestling at the Olympics Men's light heavyweight Greco-Roman wrestlingat the Games of the VIII OlympiadVenueVélodrome d'HiverDatesJuly 6–10Competitors22 from 15 nationsMedalists Carl Westergren  Sweden Rudolf Svensson  Sweden Onni Pellinen  Finland← 19201928 → Wrestling at the1924 Summer OlympicsGreco-RomanBantammenFeathermenLightmenMiddlemenLight heavymenHeavymenFreestyleBantammenFeathermenLightmenWeltermenMiddlemenLight heavymenHeavymenvte ...

 

 

Chufut-Kale

Historic settlement in Crimea CrimeaÇufut Qale Чуфут-КалеHistoric settlementChufut-Kale cave cityÇufut QaleLocation of Chufut-Kale in CrimeaCoordinates: 44°44′28″N 33°55′28″E / 44.74111°N 33.92444°E / 44.74111; 33.92444Region Crimea CrimeaRaionBakhchysarai RaionEstablished6th - 10th centuryTime zoneUTC+4 (MSK) Chufut-Kale (Crimean Tatar: Çufut Qale Tatar pronunciation: [tʃuˈfut qaˈle]; Russian and Ukrainian: Чуфут-Кале -...

 

 

Brock Pemberton

American theatrical producer and director For the baseball player of the same name, see Brock Pemberton (baseball). Brock PembertonBrock PembertonBornRalph Brock Pemberton(1885-12-14)December 14, 1885Leavenworth, Kansas, U.S.DiedMarch 11, 1950(1950-03-11) (aged 64)New York City, New York, U.S.EducationUniversity of KansasAlma materCollege of EmporiaOccupationsTheatre producertheatre directorstage actorjournalistKnown forFounding the Tony AwardsNotable workHarveySpouse Margaret ...

ソー (オー＝ド＝セーヌ県)

Sceaux 行政国 フランス地域圏 (Région) イル＝ド＝フランス地域圏県 (département) オー＝ド＝セーヌ県郡 (arrondissement) アントニー郡小郡 (canton) 小郡庁所在地INSEEコード 92071郵便番号 92330市長（任期） フィリップ・ローラン（2008年-2014年）自治体間連合 (fr) メトロポール・デュ・グラン・パリ人口動態人口 19,679人（2007年）人口密度 5466人/km2住民の呼称 Scéens地理座標 北緯48度4...

 

 

Niira Radia

Chairperson of Nayati Healthcare Niira RadiaBornNira Menon (1960-11-19) 19 November 1960 (age 63)[1]Nairobi, Kenya[2]Alma materHaberdashers' Aske's School for Girls, LondonUniversity of WarwickOccupation(s)Corporate lobbyist, Hospital owner and chairpersonOrganization(s)Nayati Healthcare Pvt. Ltd.Sudesh FoundationKnown forRadia tapes controversy Niira Radia (née Nira Menon; born on 19 November 1960) is a former corporate lobbyist whose taped telephone conv...

 

 

Concerto for Orchestra (Sessions)

Composition by Roger Sessions The Concerto for Orchestra is a composition for orchestra by the American composer Roger Sessions. The work was commissioned by the Boston Symphony Orchestra and premiered October 23, 1981, with conductor Seiji Ozawa leading the Boston Symphony Orchestra. The concerto was Sessions's last orchestral composition and won him the 1982 Pulitzer Prize for Music.[1] Sessions had previously won a special lifetime achievement Pulitzer Prize in 1974 for his life's ...

Pemilihan umum Gubernur Bali 2013

Pemilihan umum Gubernur Bali 20132008201815 Mei 2013Kandidat   Calon I Made Mangku Pastika A.A.G.N. Puspayoga Partai Demokrat PDI-P Pendamping I Ketut Sudikerta Dewa Nyoman Sukrawan Suara rakyat 1.063.734 1.062.738 Persentase 50,02% 49,98% Peta persebaran suara Peta lokasi Bali Gubernur dan Wakil Gubernur petahanaI Made Mangku Pastika dan Puspayoga PDI-P Gubernur dan Wakil Gubernur terpilih I Made Mangku Pastika dan Sudikerta Demokrat Pemilihan umum Gubernur Bali 2013 dilaksanakan ...

 

 

Cakram Blu-ray

Cakram Blu-rayLogo Cakram Blu-raySisi lainnya dari Blu-ray. Tidak seperti CD dan DVD, warnanya memiliki rona biru.Jenis mediacakram optik kepadatan tinggiPenyandianPengkodean data: CLV atau Zon lubang-and-lapisan CAV dengan kode koreksi kesalahan yang disisipkan Pengkodean video BDMV: H.262 / MPEG-2 Bagian 2 H.264 / MPEG- 4 AVC VC-1 H.265Kapasitas25 sampai 50 GB (satu lapis), 50 sampai 100 GB (dua lapis)Mekanisme baca195-405 nm laser dioda, 36 Mb/sPengembangSony Blu-ray Disc AssociationP...

 

 

Las vacaciones de Mr. Bean

Las vacaciones de Mr. BeanFicha técnicaDirección Steve BendelackProducción Peter Bennet-JonesGuion Rowan Atkinson Richard CurtisMúsica Howard GoodallFotografía Baz IrvineMontaje Tony CranstounVestuario Piérre Yves GayraudProtagonistas 23 personasRowan AtkinsonEmma de CaunesMax BaldryWillem DafoeKarel RodenJean RochefortAntoine de CaunesArsène MoscaCatherine HosmalinÉric NaggarGilles Gaston-DreyfusJulie FerrierNader BoussandelPhilippe CariouStéphane DebacSteve HarveyUrbain CancelierJu...

Cyberspace

Concept describing a widespread, interconnected digital technology For other uses, see Cyberspace (disambiguation). Not to be confused with Cyberchase. Part of a series onCyborgs Cyborgology Bionics Biomimicry Biomedical engineering Brain–computer interface Cybernetics Distributed cognition Genetic engineering Human ecosystem Human enhancement Intelligence amplification Whole brain emulation Theory Cyborg anthropology Centers Cyberpunk Cyberspace Politics Cognitive liberty Extropianism Morp...

 

 

Pyramid (image processing)

Type of multi-scale signal representation Feature detection Edge detection Canny Deriche Differential Sobel Prewitt Robinson Roberts cross Corner detection Harris operator Shi and Tomasi Level curve curvature Hessian feature strength measures SUSAN FAST Blob detection Laplacian of Gaussian (LoG) Difference of Gaussians (DoG) Determinant of Hessian (DoH) Maximally stable extremal regions PCBR Ridge detection Hough transform Hough transform Generalized Hough transform Structure tensor Structure...

 

 

Rafle de Dijon (1944)

Rafle de Dijon Type Rafle (Shoah en France) Pays France Localisation Dijon Organisateur  Reich allemand Date du 21 au 26 février 1944 Répression Arrestations 87 (hommes, femmes et enfants) modifier  La principale rafle de Dijon est une rafle antisémite perpétrée sous l'autorité du régime de Vichy qui se déroula du 21 au 26 février 1944 à Dijon (Côte-d'Or). 87 personnes, hommes, femmes et enfants, sont arrêtées et déportées de Drancy vers Auschwitz. Il n'y a qu'une se...

Passauer Neue Presse

This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: Passauer Neue Presse – news · newspapers · books · scholar · JSTOR (January 2013) (Learn how and when to remove this message) Passauer Neue PresseTypeDaily newspaperFounded1946Websitehttp://www.pnp.de Passauer Neue Presse is a German newspaper established in 19...

 

 

Claud Alexander

Claud Alexander1st BaronetIn office1886–1899Succeeded bySir Claud AlexanderMember of the British Parliamentfor South AyrshireIn office1874–1885 Personal detailsBorn15 January 1831Died23 May 1899Political partyConservativeSpouseEliza SpeirsAlma materChrist Church, OxfordMilitary serviceRankmajor-general[1]UnitGrenadier GuardsBattles/warsCrimean WarAwardsCrimean Medal and ClaspTurkish War MedalOrder of the Medjidie 5th Class Sir Claud Alexander, 1st Baronet (15 January 1831 –...