אימות תוכנה

הנדסת תוכנה
ערך זה שייך לקטגוריית הנדסת תוכנה
פעילויות ושלבים
דרישותניתוחאפיוןארכיטקטורהעיצובתכנותניפוי שגיאותבדיקהאימותבנייהפריסהתפעולתחזוקה
מתודולוגיות
זריזותמפל המיםתכנת ותקןCrystal ClearScrumUnified ProcessExtreme Programmingאינטגרציה רציפהDevOps
תחומים תומכים
ניהול פרויקטיםניהול תצורהתיעודהבטחת איכותProfiling
כלים
מהדרמקשרמפרשIDEניהול גרסאותאוטומציית בנייה

אימות תוכנה הוא תחום במדעי המחשב העוסק בהוכחה שתוכנה מסוימת נכונה (כלומר מבצעת בדיוק את מה שהוגדר במפרט שלה) או בעלת תכונות מסוימות.

מרבית העוסקים בפיתוח תוכנה בודקים את התוכנה ולא מאמתים אותה. הבדיקה נעשית באמצעות בחירת מקרים ספציפיים ובדיקה שהתוכנה מתנהגת כנדרש במקרים אלו. שיטה זו כרוכה בעבודה רבה ורמת האמינות של תוכנה הנבדקת כך נמוכה יחסית, משום שאין ביטחון כיצד תתנהג התוכנה במקרים שלא נבדקו. לעומת זאת, כאשר מוכיחים את אמינות התוכנה, ידוע מכך שהיא תתנהג נכון בכל המקרים.

שיטות

ישנן שתי שיטות עיקריות לאימות תוכנה.

הראשונה היא שיטת בדיקות מודל - תהליך האימות מתבצע על מודל מתמטי המתאר את מערכת התוכנה, תוך הוכחת נכונות של תכונות הנדרשות על בסיס המודל הזה, תוך ניתוח המצבים והמעברים ביניהם. על מנת להצליח בשיטה הזאת, המודל חייב להיות סופי (בעל מספר סופי של מצבים). השיטה הזאת מאוד מוגבלת מהבחינה המעשית, בגלל בעיית התפוצצות מצבים שמאפיינת מערכות מעשיות רבות.

השיטה השנייה היא שיטת ההוכחה - בשיטה הזאת מתארים תכונות מסוימות של התכונה בתחשיב פסוקים לוגי (בעזרת לוגיקה טמפורלית, כדוגמת *CTL), ומוכיחים שהתוכנה (יותר נכון המודל שלה) מספקת את התכונות הנדרשות, בעזרת כלים מתמטיים אוטומטיים או אוטומטיים למחצה (Theorem Provers). גם השיטה הזאת מוגבלת בגלל בעיית התפוצצות מצבים, זאת למרות שניתן לבטא בעזרת תחשיב לוגי גם תכונות עבור מודלים אינסופיים.

שיטות של אימות תוכנה משמשות גם לאימות מעגלים לוגיים הכלולים ברכיבי חומרה, שם בעיית התפוצצות המצבים חריפה פחות. כל מעגל לוגי כזה הוא למעשה סוג של תוכנית מחשב שכן הוא מקבל קלט ומוציא פלט בהתאם.

מגבלות

ישנן שתי בעיות עיקריות באימות תוכנה. המעשית שבהן היא שאימות תוכנה דורש מיומנות רבה ורקע מתמטי ברמה גבוהה מהמקובל. הבעיה החמורה יותר היא שלא ניתן להוכיח קיום או שלילה של תכונה כלשהי על כל תוכנית שרירותית. דוגמה לכך היא ההוכחה כי אי אפשר לפתח תוכנית שיכולה לוודא האם תוכנית כלשהי תעצור כאשר תקבל קלט מסוים (בעיה זו ידועה כבעיית העצירה). משפט רייס מוכיח כי לא ניתן לכתוב תוכנית שתוכל להכריע לגבי כל תוכנית שהיא האם היא מקיימת תכונה לא טריוויאלית (תכונה שלא כל תוכנית בהכרח מקיימת) כלשהי.

למרות שמגבלה תאורטית זו נראית חמורה עדיין אימות תוכנה תורם רבות מבחינה מעשית. למשל, לגבי תכונות מסוימות ניתן לבצע בדיקה שאומנם עשויה לעיתים לטעות ולומר על תוכנית תקינה שהיא אינה תקינה, אך לעולם אינה אומרת על תוכנית שאינה תקינה שהיא תקינה. גישה כזאת נקראת "שמרנית", ודוגמה אליה היא מערכות טיפוסים של שפות תכנות, המוכיחות היעדר שגיאות טיפוסים.

אמיר פנואלי ממכון ויצמן למדע היה למומחה ברמה בינלאומית בתחום זה ואף זכה על מחקריו בתחום בפרס טיורינג, הפרס החשוב ביותר במדעי המחשב, על מחקרו ופיתוחיו בתחום הלוגיקה הטמפורלית.

ראו גם

Read other articles:

Radio station in St. Charles, MinnesotaKDCZSt. Charles, MinnesotaBroadcast areaRochester, MinnesotaFrequency107.7 MHzBrandingSasquatch 107.7ProgrammingFormatClassic rockAffiliationsCompass Media NetworksOwnershipOwnerTownsquare Media(Townsquare License, LLC)Sister stationsKDOC-FM, KFIL, KFIL-FM, KOLM, KROC, KROC-FM, KWWK, KYBAHistoryFirst air dateApril 18, 1998 (1998-04-18) (as KLCX)Former call signsKANP (1996–1997)KLCX (1997–2008)KDZZ (2008–2017)Technical informationFac...

 

العلاقات الزيمبابوية الفنزويلية زيمبابوي فنزويلا   زيمبابوي   فنزويلا تعديل مصدري - تعديل   العلاقات الزيمبابوية الفنزويلية هي العلاقات الثنائية التي تجمع بين زيمبابوي وفنزويلا.[1][2][3][4][5] مقارنة بين البلدين هذه مقارنة عامة ومرجعية للدول�...

 

Arkansas's gun law Location of Arkansas in the United States Gun laws in Arkansas regulate the sale, possession, and use of firearms and ammunition in the state of Arkansas in the United States. Summary table Subject / law Long guns Handguns Relevant statutes Notes State permit required to purchase? No No Firearm registration? No No Assault weapon law? No No Magazine capacity restriction? No No Owner license required? No No Permit required for concealed carry? N/A No AR Code § 5-73-120A...

Catholic Clergy journal Homiletic and Pastoral ReviewCover of the January 2011 issueEditorJohn P. CushCategoriesCatholicismFounderJoseph F. WagnerFounded1900CompanyIgnatius PressCountryUnited StatesLanguageEnglishWebsitewww.hprweb.comISSN0018-4268 Homiletic and Pastoral Review (HPR) is a religious journal, the first Catholic Clergy magazine to appear in the United States and has been the leading journal of its kind for over a century. The current editor-in-chief is the Reverend John Cush, pro...

 

Rotating chair Further information: Office chair A swivel chair with a pump to raise and lower the seat A swivel, swivelling, spinny, or revolving chair is a chair with a single central leg that allows the seat to rotate 360 degrees to the left or right. A concept of a rotating chair with swivel castors was illustrated by the Nuremberg patrician Martin Löffelholz von Kolberg in his 1505 technological illuminated manuscript, the so-called Codex Löffelholz, on folio 10r.[1] It is purp...

 

Ferruccio Benzoni Ferruccio Benzoni (Cesenatico, 18 febbraio 1949 – Cesena, 16 giugno 1997) è stato un poeta italiano. Indice 1 Biografia 2 Opere (parziale) 2.1 Poesia 2.2 Saggi e interviste 2.3 Poesie e raccolte tradotte 2.4 Carteggi 3 Premi 4 Note 5 Bibliografia 6 Altri progetti 7 Collegamenti esterni Biografia Ferruccio Benzoni nasce a Cesenatico il 18 febbraio 1949. Frequenta il liceo classico a Cesena e si dimostra subito un lettore vorace cominciando a scrivere poesie sin da giovanis...

Piala EFL 2019–20202019–20 EFL CupNegara Inggris WalesTanggal penyelenggaraan6 Agustus 2019 s.d. 1 Maret 2020Jumlah peserta92Juara bertahanManchester CityJuaraManchester City(gelar ke-7)Tempat keduaAston VillaJumlah pertandingan92Pencetak gol terbanyakLiam Boyce(5 gol)← 2018–2019 2020–2021 → Seluruh statistik akurat per 29 Januari 2020. Piala EFL 2019–2020 (dikenal sebagai Piala Carabao untuk alasan sponsor) adalah edisi ke-60 penyelenggaraan Piala EFL, sebuah kompetis...

 

Pieter Feith Sekretariat Jenderal Dewan Uni Eropa Deputi Bidang Politik MiliterMasa jabatan2001–2010 Informasi pribadiLahir9 Februari 1945 (umur 79)[1]Rotterdam, the Netherlands[1]Kebangsaan BelandaAlma materUniversity of Lausanne, SwitzerlandSunting kotak info • L • B Pieter Cornelis Feith (lahir 9 Februari 1945) adalah seorang diplomat Belanda yang sekarang menjabat sebagai Perwakilan Khusus Uni Eropa di Kosovo. Pieter pernah menjabat sebagai ketua ...

 

Wachusett Meadow Wildlife SanctuaryTypeWildlife sanctuary, nature centerLocation113 Goodnow RoadPrinceton, Massachusetts, USACoordinates42°27′21″N 71°54′20″W / 42.4557°N 71.9055°W / 42.4557; -71.9055Area1,135 acres (459 ha)Operated byMassachusetts Audubon SocietyHiking trails12 milesWebsiteWachusett Meadow Wildlife Sanctuary Wachusett Meadow Wildlife Sanctuary is a 1,135 acres (459 ha) wildlife sanctuary located in Princeton, Massachusetts, o...

Government ministry in India 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: Ministry of Science and Technology India – news · newspapers · books · scholar · JSTOR (December 2022) (Learn how and when to remove this message) Ministry of Science and TechnologyBranch of Government of IndiaMinistry of Scien...

 

Species of carnivore Rusty-spotted genet Conservation status Least Concern  (IUCN 3.1)[1] Scientific classification Domain: Eukaryota Kingdom: Animalia Phylum: Chordata Class: Mammalia Order: Carnivora Suborder: Feliformia Family: Viverridae Genus: Genetta Species: G. maculata Binomial name Genetta maculata(Gray, 1830) Rusty-spotted genet range The rusty-spotted genet (Genetta maculata),[2] also called panther genet and large-spotted genet, is a genet that is widely ...

 

Fictional Star Trek species FerengiStar Trek raceThree Ferengi in the Star Trek: The Next Generation episode The Price.Created byGene RoddenberryHerbert WrightIn-universe informationQuadrantAlphaHome worldFerenginar The Ferengi (/fəˈrɛŋɡi/) are a fictional extraterrestrial species in the American science fiction franchise Star Trek. They were devised in 1987 for the series Star Trek: The Next Generation, played a prominent role in the following series Star Trek: Deep Space Nine, and have...

Сельское поселение России (МО 2-го уровня)Новотитаровское сельское поселение Флаг[d] Герб 45°14′09″ с. ш. 38°58′16″ в. д.HGЯO Страна  Россия Субъект РФ Краснодарский край Район Динской Включает 4 населённых пункта Адм. центр Новотитаровская Глава сельского пос�...

 

Белая мечеть 54°57′58″ с. ш. 49°03′40″ в. д.HGЯO Тип мечеть Страна  Россия Местоположение Болгар, Спасский район, Татарстан и Приво́лжский федера́льный о́круг Основатель Минтимер Шарипович Шаймиев Дата основания 2010  Медиафайлы на Викискладе Бéлая мечé...

 

{{{name}}} تعديل مصدري - تعديل   كنيسة القديسة حنة الكاثوليكية في بوخارا. الكنيسة الكاثوليكية النيباليَّة هي جزء من الكنيسة الكاثوليكية العالمية في ظل القيادة الروحية للبابا في روما؛ واعتباراً من عام 2011 ضمت البلاد أكثر من 10,000 كاثوليكي.[1] نشرت الكاثوليكية لأول مرة في نيب�...

بيتشكرافت T-6 تكسان الثانيةمعلومات عامةالنوع طائرة تدريببلد الأصل الولايات المتحدةالمهام تدريب طيران التطوير والتصنيعالصانع هوكر بيتش كرافتسنة الصنع 2000الكمية المصنوعة 636سيرة الطائرةدخول الخدمة 2001أول طيران 2000الخدمةالمستخدم الأساسي القوات الجوية الأمريكيةمستخدمون آخر�...

 

The OutsidersPoster rilis teatrikalSutradaraFrancis Ford CoppolaProduserGray FredericksonFred RoosSkenarioKathleen RowellBerdasarkanThe Outsidersoleh S.E. HintonPemeran C. Thomas Howell Matt Dillon Ralph Macchio Patrick Swayze Rob Lowe Diane Lane Emilio Estevez Tom Cruise Leif Garrett Penata musikCarmine CoppolaSinematograferStephen H. BurumPenyuntingAnne GoursaudPerusahaanproduksiZoetrope StudiosDistributorWarner Bros.Tanggal rilis 25 Maret 1983 (1983-03-25) Durasi90 menit (versi ...

 

European folklore beings associated with water For other uses, see Undine (disambiguation). Not to be confused with Undyne. UndineUndineGroupingLegendary creatureFirst attestedIn folkloreRegionEurope Undine A novella Undines (/ˈʌndiːnz, ənˈdiːnz/; also ondines) are a category of elemental beings associated with water, stemming from the alchemical writings of Paracelsus. Later writers developed the undine into a water nymph in its own right, and it continues to live in modern literature ...

Several types of leg coverings A woman wearing black leggings Leggings are several types of leg attire that have varied through the years. Modern usage from the 1960s onwards has come to refer to elastic close-fitting high-rise garments worn over the legs typically by women, such as leg warmers or tights. Usage from the 18th century refers to men's wear usually made of cloth or leather that is wrapped around the leg down to the ankle.[1] In the 19th century, leggings usually referred ...

 

Wonderful LifeSutradaraSidney J. FurieProduserKenneth HarperDitulis olehPeter MyersRonald CassTanggal rilis1964Durasi83 menitNegara Britania RayaBahasaInggris Wonderful Life adalah sebuah film drama-musikal Britania Raya tahun 1964, dibuat sebagai kendaraan untuk bintang pop Cliff Richard dan adalah ketiga dalam serial yang termasuk The Young Ones dan Summer Holiday. Koreografi oleh Gillian Lynne, disutradarai oleh Sidney J. Furie dengan naskah tulisan Peter Myers dan Ronald Cass. Film ini di...