Svenska ElektronikForumet

Även om koden gör precis som tänkt under alla omständigheter, kan det ju vara så att "tänket" var fel från början. Denna aspekt tycker jag att det fokuseras alldeles för lite på. Spelar ju ingen roll ifall koden passerar alla tester (med hjälp av testmjukvara för miljontals kronor) om detta är fallet.

Men det är ju en så jobbig tanke så den vill ju de flesta undvika.

Ja, väldigt mycket utveckling sker idag utan en riktig förståelse av
den miljö och de processer där det hela ska användas. Ett fenomen
som ökar med konsulter i fel roller och tillfälliga utvecklare från
firmor runt halv jordklotet.

Ett exempel på hur det kan gå. Känner en del som jobbar/jobbade där...
https://computersweden.idg.se/2.2683/1. ... rojekt-nbg

lillahuset skrev:Det som förbryllar mig mest är att det finns en massa (nåja ett gäng iallafall) folk här i forumet som verkar ha väldigt svårt för konceptet att det är i stort sett omöjligt att BEVISA att ett program är FELFRITT.

Vad jag menar är att du gör en modell i något strikt deklarativt modelleringsspråk och sedan bevisar matematiskt att din modell är fullständigt korrekt. Då finns det inga undantag eller "oj jag tänkte inte på det". Används för t.ex. telefonväxlar, mobilnät och kritiska saker i bilar som bromssystem.

Buggar kan naturligtvis uppstå senare i implementationen men blir lättare att hitta eftersom du har en garanterat korrekt modell att jämföra med.

Prolog och logikprogrammering fanns väl redan när farbror var student? Se det som en utvecklig på det spåret.

Vad är det som är så speciellt med en modell som gör att den kan "garanteras"?

Det finns säkert vissa typer av modeller/strukturer som man kan bevisa vissa egenskaper hos. Dock kan det ju faktiskt vara så att man väljer en sådan typ av modell just av den anledningen trots att den kanske beskriver det verkliga problemet sämre än en annan modell som inte går att visa matematiskt. Har man då vunnit någon säkerhet?

Ska se om jag kan få fram någon kod att visa vad jag försöker beskriva.

bearing skrev:Vad är det som är så speciellt med en modell som gör att den kan "garanteras"?

Du gör en matematiskt/logiskt baserad modell som sedan kan bevisas med samma metoder som matematiska bevis.

Fungerar inte på allt men kan du logiskt specificera t.ex. en elektronisk krets eller paketkärnan i dit mobilnät då kan du även verifiera och bevisa att modellen alltid kommer att fungera korrekt.

Swesysmgr, men problemet kvarstår fortfarande om modellen representerar verkligheten/problemställningen tillräckligt bra?
Gör den inte det kan man visserligen klappa sig på axeln och säga att modellen garanterat uppför på ett predikterbart sätt, men kanske inte som behövs för att lösa problemet.

Det finns ett obegränsat antal icke simulerbara händelser i alla system, vilka kan få systemet att uppträda helt oberäkneligt.

För att verifiera ett system ska man i grunden simulera alla möjliga inputs till det.

Det riktigt svåra är att man sedan ska VETA hur systemet ska reagera för ett givet input!

Att ett system fungerar korrekt enl. specifikationerna MÅSTE betyda att specifikationerna ska vara alltomfattande!

Har man kört "skarp" programmering - alltså på viktiga funktioner - bör man ha insett att det svåra är inte att få en sekvens till att köra, det svära är att fånga felen (in-värden utanför spec.) och få systemet till att reagera lämpligt.

Ett enkelt exempel: farthållare till fordon.
Att fixa en hastighetshållning är inte så svårt, det svåra är alla ting som sker och vad som ska hända då.
* Krock.
* Dålig hastighetssensor (t.ex. ABS-ringen som börjar bli dålig)
* Över/undervarv.
* Växel blir ryckt ur.
osv.

swesysmgr skrev:

bearing skrev:Vad är det som är så speciellt med en modell som gör att den kan "garanteras"?

Du gör en matematiskt/logiskt baserad modell som sedan kan bevisas med samma metoder som matematiska bevis.

Fungerar inte på allt men kan du logiskt specificera t.ex. en elektronisk krets eller paketkärnan i dit mobilnät då kan du även verifiera och bevisa att modellen alltid kommer att fungera korrekt.

Jag är lite insatt, och har förstått att modellbaserad utveckling ses som något "fantastiskt", och lösningen på "alla" problem i säkerhetskritiska applikationer. Men min erfarenhet är att ju säkrare modellen ska vara, ju mindre beståndsdelar måste den byggas upp av, för att kunna att garantera att varje beståndsdel är felfri. I slutändan hamnar man i ett grafiskt programmeringsspråk, som måste programmeras på liknande sett som ett vanligt textbaserat språk. Det kommer ner på nivån att varje typomvandling måste finnas med. I mina ögon är den enda fördelen med detta grafiska programmeringsspråk att det har väldigt hårda kontroller av "koden" innan kompilering, ungefär som de verktyg som finns för att följa MISRA. Det är helt omöjligt att skriva till oönskade adresser i RAM och så vidare. Men bortsett från sådana saker, kan man göra misstag i modellen, precis som i ett vanligt handskrivet program.

Misstagen kommer säkert upptäckas av de matematiska metoder du beskriver. Men jag tror att det bara är en väldigt liten del av ett stort program som kan verifieras på det sättet.

Andax skrev:Swesysmgr, men problemet kvarstår fortfarande om modellen representerar verkligheten/problemställningen tillräckligt bra?
Gör den inte det kan man visserligen klappa sig på axeln och säga att modellen garanterat uppför på ett predikterbart sätt, men kanske inte som behövs för att lösa problemet.

Jo så är det och det är därför det kan bli dyrt med formell validering när du behöver göra mycket mer omfattande kravfångst och specifikation samt kanske köpa dyra verktyg. Är nog därför det främst används för kritiska system som ligger långt från användaren

TomasL skrev:Det finns ett obegränsat antal icke simulerbara händelser i alla system, vilka kan få systemet att uppträda helt oberäkneligt.

Nej varför det? Du har begränsat med input och du vet exakt hur ditt system kommer att bete sig. Skall din krets som du verifierat bestrålas i rymden eller köras utanför specat temperaturområde då går det nog inte.

bearing skrev:

swesysmgr skrev:

bearing skrev:Vad är det som är så speciellt med en modell som gör att den kan "garanteras"?

Du gör en matematiskt/logiskt baserad modell som sedan kan bevisas med samma metoder som matematiska bevis.

Fungerar inte på allt men kan du logiskt specificera t.ex. en elektronisk krets eller paketkärnan i dit mobilnät då kan du även verifiera och bevisa att modellen alltid kommer att fungera korrekt.

Jag är lite insatt, och har förstått att modellbaserad utveckling ses som något "fantastiskt", och lösningen på "alla" problem i säkerhetskritiska applikationer. Men min erfarenhet är att ju säkrare modellen ska vara, ju mindre beståndsdelar måste den byggas upp av, för att kunna att garantera att varje beståndsdel är felfri. I slutändan hamnar man i ett grafiskt programmeringsspråk, som måste programmeras på liknande sett som ett vanligt textbaserat språk. Det kommer ner på nivån att varje typomvandling måste finnas med. I mina ögon är den enda fördelen med detta grafiska programmeringsspråk att det har väldigt hårda kontroller av "koden" innan kompilering, ungefär som de verktyg som finns för att följa MISRA. Det är helt omöjligt att skriva till oönskade adresser i RAM och så vidare. Men bortsett från sådana saker, kan man göra misstag i modellen, precis som i ett vanligt handskrivet program.

Misstagen kommer säkert upptäckas av de matematiska metoder du beskriver. Men jag tror att det bara är en väldigt liten del av ett stort program som kan verifieras på det sättet.

Du kan specificera med hjälp av kod i ett språk gjort för det, finns inget krav på att köra dra-och-släpp programmering varken för verifiering eller implementation så den invändningen förstår jag inte.