Dansk center vil skabe værktøjer til fejlfri programmering

Illustration: Beebright/Bigstock
Programmers sikkerhed kan blive bedre, hvis man kan bevise, at udførelsen er korrekt. Det er visionen for et nyt center på Aarhus Universitet, som også vil skabe open source-værktøjer, der kan hjælpe til.

Aarhus Universitet har fået 35 millioner kroner fra en pengetank til oprettelse af et nyt center, der skal forske i udvikling af metoder og værktøjer, der kan bevise, at et givent program ikke indeholder fejl.

Det er især anvendeligt til kryptografi og sikkerhed, hvor en enkelt lille fejl kan have store konsekvenser.

I spidsen for der nye center står professor Lars Birkedal. Han begrunder eksistensen således:

»Vi vil udvikle de fundamentale matematiske modeller og logikker, som kan bruges til at lave matematisk ræsonnering om korrekthed og sikkerhed. På sigt kan det lede til bedre værktøjer, som kan hjælpe programmører med at lave bedre software.«

Aarhus Universitets nye Center for Grundforskning i Program-verifikation kan skabe forskning, der på længere sigt blandt andet kan gøre kryptografiske algoritmer fejlfri, håber dets leder, professor Lars Birkedal. Illustration: Morten Koldby

Når man analyserer software, har man behov for modeller på forskellige abstraktionsniveauer, fortæller Lars Birkedal. Mange fejl i software stammer fra subtile problemer i implementationen af software.

»Så vi kigger på meget detaljerede modeller af programmerne – 'semantiske' modeller. Det er dem, vi interesserer os for.«

Læs også: Sådan finder og retter Facebook kodefejl med kunstig intelligens

Sikkerhedsbrister i software giver udfordringer for samfundet

Målet for det nye Center for Grundforskning i Program-verifikation er at udvikle bedre teknikker til at sikre softwaresystemer, som i dag er en stor del af vores samfundsstruktur.

Hvis der er fejl eller sikkerhedsbrister, giver det enorme udfordringer for samfundet, lyder synspunktet.

Baggrunden for projektet er Lars Birkedals tidligere topforsker-bevilling, hvor der blev udviklet teknikker, som kan bruges til at ræsonnere om avancerede programmeringssprog. Lars Birkedal peger selv på, at et gennembrud i den forbindelse var en ‘state of the art-programlogik,’ med navnet Iris.

»Det er det, vi vil bygge videre på, så vi kan ræsonnere om en større klasse af realistiske software-systemer og korrektheds-sikkerhedsegenskaber. Jeg har fået midler til at ansatte en række ph.d-studerende og postdocs, som skal samarbejde med mig, og derudover er der også en række forskere her på stedet, som vil komplementere med deres projekter,« siger han og tilføjer uddybende om sit gennembrud med Iris:

»Det har indbyggede faciliteter, som gør det muligt at ræsonnere matematisk om avancerede programmer. Det er dem, der har samtidige tråde, der afvikles, er højordens-programmer og er imperative.«

Imperative sprog er dem, der er flest af, som Java og C++, hvor programudførslen består af en række fortløbende skridt, ligesom en bageopskrift.

Avancerede programmer er svære at analysere

Det er faciliteter, som er vigtige for at skrive større programmer og det er velkendt, at de er svære at ræsonnere om og analysere.

Logikken gør det muligt at skrive ned hvad et programmodul skal gøre og bevise, at en modul gør det, det skal gøre.

»Vi har et prototype-værktøj – en bevis-assistent. Så kan man sikre sig, at alt fungerer korrekt. Det er det eneste verifikations-værktøj, der har alle disse faciliteter. Det er et framework, der kan instantieres til forskellige programmeringssprog. Vi har brugt et ML-lignende sprog med tråde, der afvikles samtidigt. Vores samarbejdspartnere på Max Planck-instituttet i Tyskland benytter det til at analysere programmer skrevet i Rust.«

Læs også: Rust: Sådan vil Mozilla genstarte Firefox med sikker og hurtig kode

Det er også implementeret i mere akademiske programmeringssprog, såsom en variant af Haskell.

Det er ikke hele sprog, der behandles, men man tager de væsentlige dele ud, og kigger nærmere på dem.

Fejlfri kryptografiske protokoller

For ikke så mange år siden var det kun trivielle programmer, man kunne bevise korrektheden af. Og det er heller ikke fordi Lars Birkedal regner med, at al software kan bevises korrekt i morgen.

Men nu kan man specificere og verificere ret avancerede programmer. Det er for eksempel de samtidige algoritmer, der findes inde i maven på operativsystemer, som man kan specificere og ræsonnere om.

»Der findes noget, der hedder låse-fri datastrukturer, som er lavet for at undgå at bruge låse i trådede programmer, for at få mest mulig effektivitet. Det er ekstremt kompliceret at vise, at de er korrekte.«

Det er stadig forskning, men man er dog nået så langt, at specialestuderende kan udføre projekter med teknikken.

»Distribuerede systemer er en af de ting vi mangler. Vi har taget de første spæde skridt, og det vil vi gerne kigge mere på. Et andet punkt er implementering af kryptografiske protokoller.«

Blandt kryptografer er modellerne mere abstrakte. Centerets modeller er mere konkrete og detaljerede og de to slags modeller komplementerer hinanden.

»Det kræver blandt andet, at sandsynlighedsmæssige egenskaber skal kunne håndteres. Det kan vi ikke endnu.«

Sikkerhed svært at løse med test

For 20 år siden var programtest ikke så højt oppe på udviklernes dagsorden. I mellemtiden har automatiserede tests og metoder som continuous integration i høj grad løst problemerne med ustabile programmer.

Men det løser ikke problemerne med sikkerhed.

»Tests kan kun afsløre, at der er en fejl - det kan ikke garantere, at der ikke er fejl. Selv en lille fejl kan give hackere muligheder.«

Og det er som tidligere nævnt også stadig meget svært at teste flertrådede programmer.

»Det kan man nærmest ikke. Det er også derfor, at det er et af de områder vi fokuserer på.«

Facebook er blandt dem, der er interesseret i teknologien. Medievirksomheden har selv forskerhold, der kigger på tilsvarende problematikker.

»Vi lavede et automatiseret værktøj til at analysere flertrådet software. Facebook var interesseret i, om teknikken kunne skaleres op til større programmer.«

Resultatet af forskningen bliver videnskabelige artikler. Men tanken er også at lave prototype-værktøjer, som er open source, siger Lars Birkedal. De vil kunne findes på Iris-projektets hjemmeside.

Tips og korrekturforslag til denne historie sendes til tip@version2.dk
Følg forløbet
Kommentarer (61)
sortSortér kommentarer
  • Ældste først
  • Nyeste først
  • Bedste først
Jens Madsen

Det er muligt at gøre kode meget sikker ved hjælp af tests.

Fremgangsmetoden er typisk, at der først laves specifikation, en prototype af softwaren, tests, mv. Herefter laves et antal "kloner" af softwaren, af uafhængige hold af programmører. Disse får ingen kendskab til hinandens kode, eller til prototypens kode. Alle holds kode skal fungere ens på den specificerede grænseflade. Samtlige hold, fungerer som ansvarlig reviewer på specifikationen. Det betyder at hvis der er fejl i specifikationen, så er stor sandsynlighed for, at en eller flere af holdene opdager fejlene, når de skal reproducere koden.

Når koden udføres, køres flere holds kode simultant - og er der en som svarer anderledes på grænsefladen kobles den ud, og eventuelt reetableres. På den måde undgås menneskelige fejl, og også mange fejl i specifikationen. Da koden skal skrives alene efter specifikationen, og at den skal være simpel og ikke må indeholde kode, og at samtlige uafhængige hold tager ansvar for specifikationens korrekthed, og ellers indberetter dem, så vil normalt både specifikation, og kode blive korrekt. Er der fejl i koden, så opdages den normalt under test med tests. Udover der haves tests fra prototypen, så laver hver hold uafhængige tests, og samtlige tests bliver afprøvet for alle programmer. Testene skal naturligvis leve op til reglerne for tests, så det sikres at man har været igennem hele programmet i alle ender og kanter.

Fordelen ved ovenstående er, at hvis der er tilstrækkeligt mange hold, så vil en softwarefejl - eller bagdør - intet betyde. De andres kode udfører ikke bagdøren. Og den pågældende kode kobles fra.

Dertil kommer, at man normalt har et system, så man har et fingeraftryk på enhver bit i koden, og dermed kan finde den ansvarlige programmør, samt har tidspunkt, video osv. og kan bevise at programmøren har indkodet fejlen. Normalt logger man også, hvis der bruges cut/paste, så f.eks. kopiering af koden afsløres.

Til sidst er der to muligheder: At man vælger at softwaren skal køre i sikker tilstand, hvor man kobler fejl ud - altså hvis nogen svarer forkert i forhold til de andre. Eller, man kan vælge at køre i public tilstand, hvor at man vælger den kode som svarer forkert. Det bruges normalt for at afsløre hackere, der har indlagt kode, og undersøge deres hensigter. Samtidigt, så ved man at det er tale om hacking, da der bevidst vælges hackerens kode at udføre når det er public. Fordelen er, at man bevidst får alle til at tro koden er fejlbarlig, at den kan hackes, og man får afsløret hackernes kendskab, identitet, og hensigter.

  • 1
  • 2
Jens Ole Stilling

. Det er et stort komplekst problem og uden indlysende strategier , i hvert tilfælde ingen generelle. At forvente at en god løsning består i kun at analysere strukturen af programmerne er for let sluppet.
Man må som målsætning have at en kontrol udføres løbende både at software og hardware.
Personligt ville jeg lægge tracere ind i program modulerne og lade et program udregne de forventede værdier for at løbende verificere at programmet blev udført korrekt . For at hacke programmet uden det opdages kræves der en udregning som er meget vanskelig. Som for sikkerheds relevante programmer bør man løbende kontrollere at hårdvaren fungerer korrekt. Programmoduler kan også testes som hardware .

PS hvor er det dog irriterende at håndtere dette indput felt, prøv lige selv at gøre det med en Lenovo tablet, hårdt arbejde

  • 1
  • 0
Jens Madsen

Den metode som jeg beskrev er meget sikker - men den kræver flere uafhængige programmører, og medfører derfor at softwareomkostningerne øges væsentligt. Til gengæld, så vil mange fejl blive opdaget, når programmerne udsættes for hinandens tests og sammenlignes med hinanden, og med prototypen. Det er også væsentligt, at programmørerne er indforstået med, at de ikke må stjæle kode fra nettet, eller bruge kode der på nogen måder kan komme fra samme kilde. Her findes flere metoder - blandt andet udviklet til undervisningssammenhæng for at sikre eleverne ikke snyder - der kan undersøge uafhængigheden af progammørernes kode.

Det viser sig, at der kun er to metoder som fungerer ordentligt, når der skal undgås fejl. Den bedste er semantiske modeller, da det er billigst. Men, der er mange typer fejl som den ikke kan fange. Det kan man kun ved at have flere hold uafhængige programmører. Med denne metode, fanger man alt fra tanketorsk til computerfejl hvis der er nok uafhængige hold. Den eneste fælleskilde er specifikationen, og dermed eneste kilde til fejl - men den tjekkes af flere uafhængige hold, der ikke kun har det som opgave at læse den som roman, men faktisk skal lave et uafhængigt fungerende program på grundlag af specifikationen, og den skal svare til de andre holds kode på grænsefladerne.
Og, når der er fejl, så kan man direkte pege på hvor uoverensstemmelsen opstår mellem programmerne der udføres samtidigt, og undersøge om der er fejl i koden, eller i hardware. Omtrent samme metode bruges når der tjekkes om der er fejl i hardwaren, bortset fra, at der så bruges samme kode, og ikke kode lavet af uafhængige programmører efter samme specifikation. Ved HW er det meget almindeligt at tjekke om samme kode, evt. oversat af forskellige kompilere, giver fejl på grænsefladen til f.eks. I/O kommunikationen. Typisk køres et task fra I/O indstruktion til I/O indstruktion, og det tjekkes så, at de svarer ens. En I/O indstruktion laver derfor samtidigt et tast skift. Et tvungen taskskift er normalt den nemmeste måde at gøre det. Generalt er kravet, at man har et programmeringssprog der er deterministisk (altså, der ikke kan opstå tilfældige svar på nogen måder), samt at specifikationen laves, således man kan tjekke at resultaterne altid er ens på grænsefladen. Er specifikationen ikke i orden - så bliver det hurtigt opdaget - for så kan ingen programmører lave kode der fungerer ens. Man kan også bruge metoden, så man anvender flere hold end nødvendigt, og sortere dem fra, der ikke bliver færdig hurtig nok. Eller, der kan laves forskellige kvalitetstests på softwaren, f.eks. hastighed, så der svares når tilstrækkeligt mange har svaret korrekt, og at dem der er sent, eller aldrig kommer med svar kobles fra som en fejl.

Den dårligste metode er normalt code-review. Den fungerer stort set ikke, og der er ingen garanti for kvaliteten. En rettelse kan både være korrekt, og forkert, og er ofte forkert. De fleste hackere har jobs som reviewer. Koden kan misforstås af revieweren. Og man ser også eksempel på, at revieweren lader sig påvirke af dokumentationen, til at tro koden er korrekt og fungerer, fordi der er overbevisende dokumentation og forklaringer. På et eller andet tidspunkt, giver revieweren ofte efter, og reviewer for hurtigt, således at ikke alle detaljer tjekkes. Review tager normalt mindst ligeså lang tid som at skrive softwaren forfra, og ellers skyldes det at der er noget som ikke er tjekket ordentligt.

Mange programmeringssprog anvender sig ikke til korrekt programmering, fordi at de er udviklet til at ikke fungere ens. Determinisme er minimumskravet, uanset om det er sekventielt eller parallel kode. Der må ikke være nogen tilfældighedsfunktioner, da det gør sammenligning umuligt, og umliggør enhver form for bevis, herunder rekonstruktion af fejl.

Det er muligt at lægge hacking bagdøre ind hvis alle hold samarbejder om det - men, så er det ikke længere tale om softwarefejl, men organiseret kriminalitet. Det holder de flest sig derfor fra. Og ellers, så er der love og domstole der tager sig af den slags.

  • 1
  • 0
Jens Ole Stilling

Meget vel men , 1) har du beregnet hvad sandsynligheden er med den metode for fejl. 2) omkostningerne og 3) virkningen af den yderlige kompleksitet?

Desuden henviser jeg til de udemærkede internationale standarder som dækker området " safety relevant software" de er udmærkede. Ingen særlig grund til at opfinde hjulet igen.

  • 2
  • 0
Tobias Tobiasen

Det er selvfølgelig altid velkommen hvis man automatisk kan finde fejl. Men fejlfri er meget optimistisk.
Der kan jo være fejl både i verifikationen og implementationen. Der kan jo være hele klasser af fejl man slet ikke er opmærksom på. F.eks. hvis en hash er hurtige for nogle type input så kan en angriber bruge det til at udlede noget information. Den angrebsvektor skal jo være en del af verifikationen før man kan være sikker på at den fejlfri.

Så ja til færre fejl på kendte angrebs vektorer. Men fejlfri med hensyn til ukendte angrebs vektorer? Det tror jeg ikke på.

  • 2
  • 0
Jens Madsen

Hvad hvis der er en sikkerheds fejl i den kode der vælger mellem de konkurende implementeringer?
Eller skal den kode også koden kunne kobles ud?


Det er et meget relevant spørgsmål - men det er uafhængigt af applikationen. Og det er dermed også uafhængig af applikatonens formål og kompleksitet. Vi kan i princippet flytte problemet til hardwaren, og spørge hvordan vi så har sikret os, at der ikke er fejl i hardwaren. Du spørger, om koden så også skal kunne kobles ud - ja, man kan godt f.eks. dupplere den pågældende hardware, og sikre at de kobler samme kode ud (eller evt. CPU ud).

Det er altid vigtigt, at man reducerer sikkerhedsproblematikken til så lidt kode, eller hardware som muligt, og ikke mindst sikre, at det er uafhængigt af applikationen. Dem, der sikrer sig, at sikkerheden er i orden, må ikke have kendskab til applikationen.

For at være sikker, så skal man have ca. 5 kloner af softwaren, og dermed koster det ca. 5 gange så meget at udvikle. Dog, så kan det i nogle tilfælde, være nemmere at finde fejlene, da de til en vis grad dukker op af sig selv, når testvektorer, eller tesprogrammerne udføres.

  • 1
  • 0
Jens Madsen

Det er selvfølgelig altid velkommen hvis man automatisk kan finde fejl. Men fejlfri er meget optimistisk.
Der kan jo være fejl både i verifikationen og implementationen. Der kan jo være hele klasser af fejl man slet ikke er opmærksom på. F.eks. hvis en hash er hurtige for nogle type input så kan en angriber bruge det til at udlede noget information. Den angrebsvektor skal jo være en del af verifikationen før man kan være sikker på at den fejlfri.

Så ja til færre fejl på kendte angrebs vektorer. Men fejlfri med hensyn til ukendte angrebs vektorer? Det tror jeg ikke på.


Det som du kan sikre dig ved at have flere hold, der skal lave samme kode, er at de overholder specifikationen. Der kan i specifikationen godt være timing problemer, som afslører data, og det er så et problem med specifikationen.

I nogle tilfælde, gør man det at man tidsstempler alt - det betyder, at der besluttes hvor lang tid at det tager, og det er beslutningen som der tages efter, og ikke en tilfældig beregnings hastighed. Derved får computerens hastighed ingen betydning.

  • 1
  • 0
Troels Henriksen

For mig lyder din metode ubekendt. Er der nogen som har brugt den på et større projekt?

Det lyder som om den metode der blev brugt til at udvikle rumfærgens kontrolsystem. Her var der to helt separat udviklede systemer, der brugte både forskelligt maskinel og programmel (og maskinellet var derudover yderligere redundant). Det er naturligvis en uhyre kostbar affære, men det virkede da - ingen af rumfærgeulykkerne kan tilskrives programfejl. Jeg er ikke på stående fod klar over om den teknik er blevet brugt til mere komplicerede programmer.

Den type programmer, som Lars Birkedal ifølge artiklen vil undersøge, er derudover nondeterministiske i deres natur. Her er empirisk afprøvning kun en ringe hjælp: Det kan kun påvise eksistensen af fejl, ikke deres fravær, og det er sandsynligt at disse programmer vil køre størrelsesordener længere i produktion end i test (ved f.eks. rumfærgen var det omvendt).

  • 3
  • 0
Jens Madsen

Den type programmer, som Lars Birkedal ifølge artiklen vil undersøge, er derudover nondeterministiske i deres natur. Her er empirisk afprøvning kun en ringe hjælp: Det kan kun påvise eksistensen af fejl, ikke deres fravær, og det er sandsynligt at disse programmer vil køre størrelsesordener længere i produktion end i test (ved f.eks. rumfærgen var det omvendt).


Programmer skal altid være deterministiske - ellers er det noget helt galt med den underlæggende teori. Såvel almindeligt kodet sekventielt software, som parallelt software, skal altid være deterministisk i dets natur. Ellers, så er det en fejl i sig selv.

Et program, kan derimod godt få et tilfældigt input, som gør at den tilsyneladende fungerer tilfældigt. Dette tilfældige input laves af en tilfældighedsgenerator. Dog, er vigtigt, at forstå at koden stadigt er deterministisk. Det er tilfældighedsgeneratoren, som leverer et tilfældigt input. En tilfældighedsgenerator kan ikke skrives i kode. Hvis den kan, så er det noget galt i programmeringssproget.

  • 1
  • 1
Troels Henriksen

Programmer skal altid være deterministiske - ellers er det noget helt galt med den underlæggende teori.

Klart, men programmets adfærd kan være nondeterministisk hvis det afhænger af ekstern adfærd. Et distribueret system er et klassisk eksempel på dette, da forsinkelser i netværkstrafikken lynhurtigt medfører nondeterministiske kommunikationsmønstre, og behov for synkronisering (som dertil ikke må være for langsom).

  • 4
  • 0
Jens Madsen

Klart, men programmets adfærd kan være nondeterministisk hvis det afhænger af ekstern adfærd. Et distribueret system er et klassisk eksempel på dette, da forsinkelser i netværkstrafikken lynhurtigt medfører nondeterministiske kommunikationsmønstre, og behov for synkronisering (som dertil ikke må være for langsom).


Og derfor, er det netop et krav, at forsinkelser ikke må kunne detekteres i koden. Som eksempel, så må du ikke kunne detektere om der er data i en input kø, da dette afhænger af forsinkelser til køen. Du skal altid vente på, at data kommer. I et parallelt system, må du så til gengæld gerne opprioritere det, at få data i køen, så der svares hurtigt. Der findes mange tilfælde, hvor det er nødvendigt, at vælge efter hvilke data der kommer først. Det har vi ikke lov til, da det ender i samme problematik. Det, som man kan i disse tilfælde, er at tidsstemple data hvor de sendes ind i systemet, f.eks. fra tastatur / terminal, således det bliver deterministisk og uafhængigt af bus og netværkshastigheder. Der må heller ikke forefindes delay instruktioner i software, da de ikke har relevans. Hvis man har delays, så har man dem ved at tidsstemple inputs og outputs. Tid findes ikke i software. Tid findes, når software møder den rigtige fysiske verden.

  • 1
  • 2
Baldur Norddahl

Det som du kan sikre dig ved at have flere hold, der skal lave samme kode, er at de overholder specifikationen. Der kan i specifikationen godt være timing problemer, som afslører data, og det er så et problem med specifikationen.

Når du fører matematisk bevis for kode, så sker det at det viser sig umuligt at bevise. Og ved nærmere undersøgelse, så finder man måske ud af at det skyldes at det du forsøger at bevise, simpelthen er forkert. Måske fordi at specifikationen er forkert.

Den type fejl finder du ikke nødvendigvis ved at have flere hold der implementere den samme fejlramte specifikation eller ved test.

  • 1
  • 0
Kjeld Flarup Christensen

Den metode som jeg beskrev er meget sikker - men den kræver flere uafhængige programmører, og medfører derfor at softwareomkostningerne øges væsentligt.


Til det er der så det at sige, at fejlrettelser også er en del af software omkostningerne. Det er en typisk fejl der begås igen og igen, at man sætter for få ressourcer af til test.

Som regel estimerer jeg med at tager det en uge at lave en funktionalitet, så tager det yderligere to at teste og rette den.

Det disse metoder gør er at man laver det samme program mindst to gange. Reelt er det det samme man gør når man laver en unit test at man koder funktionaliteten en gang til.

  • 1
  • 0
Kristian Mandrup

Typisk, konventionel programmering i dag er stadig meget lig med hvordan man i "gamle dage" selv lodded kredsløb sammen manuelt med dertil hørende fejl.

I dag køber man oftest færdige chips der er gennemtestet og knytter så de enkelte komponenter sammen til en færdig løsning.

Samme fremgangsmåde bør man benytte til software. Undgå så vidt muligt boilerplate kodning. En kilde til fejl uanset hvad!

Alternativt, lav et høj-niveau sprog i stil med f.eks Eve eller AppML, hvor man beskriver sin domeæne model og workflows og så har en underliggende engine der genererer al koden med dertilhørende tests (full test coverage) direkte fra den abstrakte model. Dertil kan føres lidt ekstra custom kode om nødvendigt (max 5%).

Hvis man endelig vil gøre det på lav kode niveau, så brug et sprog med indbygget statisk type og flow analyse som f.eks OCaml, ML og lignende (moderne variante f.eks F#, ReasonML, ELM osv).

For disse sprog er der normalt, at hvis programmet compiler er det også fejlfrit. No runtime errors. Undgå sprog med null pointer (aka Billion Dollar mistake). Benyt typestærke sprog uden null pointer.

Undgå at bruge statements (imperativ programmering) og kod det hele med expressions.

Case solved.

  • 0
  • 0
Jens Madsen

Når du fører matematisk bevis for kode, så sker det at det viser sig umuligt at bevise. Og ved nærmere undersøgelse, så finder man måske ud af at det skyldes at det du forsøger at bevise, simpelthen er forkert. Måske fordi at specifikationen er forkert.

Den type fejl finder du ikke nødvendigvis ved at have flere hold der implementere den samme fejlramte specifikation eller ved test.


Det er korrekt. Derfor, er også vigtigt, at de enkelte hold tager et ansvar for specifikationen. Det, som du opnår i forhold til normal review, er at de ikke kun læser specifikationen, men også skal lave en fungerende kode ud fra den. I nogle tilfælde, er det med til at fange flere fejl - specielt i tilfælde, hvor specifikationen ikke er tilstrækkeligt ordentligt defineret.

Metoden kan ikke stå alene. Skal den fungere godt, så er vigtigt, at alle programmerne er stort set fejlfri - eller bedre helt fejlfri. Desto længere, at du kan få fejlraten ned, desto bedre er det. Så det er stadigt vigtigt, at bruge andre metoder, for at reducere fejlraten mest muligt. Dens fordel er, at den opdager fejl i såvel hardware som software. Og det er forholdsvis nemt at logge data på grænsefladen, når at fejl opstår. Hacking kode, eller anden ulovlig kode, implementeret af en enkelt programmør er umuligt, da det vil kræve at flere hold implementere samme kode, og det kan kun lade sig gøre koordineret mellem holdene. Det betyder at det kun er muligt at hacke koordineret, indlægge samme fejl, og så er det orgainiseret kriminalitet. Det betyder større straffe.

Jeg syntes, at det er rigtigt godt at udvikle bedre metoder til software udvikling. Men, det er ikke alle metoder, som fanger alle typer fejl. Derfor, er nødvendigt med flere metoder, til at supplere hinanden. I nogle tilfælde kan bedre metoder endog medføre at det bliver hurtigere og nemmere at kode. Mange fejltyper, skyldes at de programmeringssprog som vi oftest bruger, direkte er udviklet til at fejle - det har jeg i hvertfald hørt historier om. Laver vi en liste over problemer, som et programmeringssprog absolut ikke må have, så viser det sig, at vi kan sætte kryds på listen for alle punkter, for langt de fleste programmeringssprog. Og det skal forstås sådan, at problemet findes i programmeringssproget - ikke, at det er fri for dem. Programmeringssprogene vi normalt bruger, er lavet til at gøre kodning meget besværligt.

  • 0
  • 0
Jens Madsen

Bedre metoder
Typisk, konventionel programmering i dag er stadig meget lig med hvordan man i "gamle dage" selv lodded kredsløb sammen manuelt med dertil hørende fejl.

I dag køber man oftest færdige chips der er gennemtestet og knytter så de enkelte komponenter sammen til en færdig løsning.

Samme fremgangsmåde bør man benytte til software. Undgå så vidt muligt boilerplate kodning. En kilde til fejl uanset hvad!

Alternativt, lav et høj-niveau sprog i stil med f.eks Eve eller AppML, hvor man beskriver sin domeæne model og workflows og så har en underliggende engine der genererer al koden med dertilhørende tests (full test coverage) direkte fra den abstrakte model. Dertil kan føres lidt ekstra custom kode om nødvendigt (max 5%).

Hvis man endelig vil gøre det på lav kode niveau, så brug et sprog med indbygget statisk type og flow analyse som f.eks OCaml, ML og lignende (moderne variante f.eks F#, ReasonML, ELM osv).

For disse sprog er der normalt, at hvis programmet compiler er det også fejlfrit. No runtime errors. Undgå sprog med null pointer (aka Billion Dollar mistake). Benyt typestærke sprog uden null pointer.

Undgå at bruge statements (imperativ programmering) og kod det hele med expressions.

Case solved.


Og hvordan sikrer du så mod menneskelige tanketorsk?

Skal du sikre mod bevidste fejl, bagdøre, tanketorsk, og lign. problemer, så kan det ikke gøres uden uafhængige mennesker til at lave og teste koden. En enkelt person, kan aldrig gøre noget beviseligt fejlfrit.

  • 0
  • 0
Jens Madsen

I dag køber man oftest færdige chips der er gennemtestet og knytter så de enkelte komponenter sammen til en færdig løsning.

Samme fremgangsmåde bør man benytte til software. Undgå så vidt muligt boilerplate kodning. En kilde til fejl uanset hvad!


Det er faktisk en rigtig god metode, fordi at hvis der bruges samme komponenter til alt, så vil de automatisk blive testet godt.
Som regel er vi dog ikke tilfreds med det, for i større kode, kan sagtens være fejl, bagdøre og lign. trods der er millioner som bruger det. Så derfor, så sættes krav til, hvordan at koden er opstået. Er koden frembragt på en måde, så vi også er 100% sikker på, at den er fejlfri, så må vi først bruge den. Man kan - også med den metode jeg beskriver - i visse tilfælde acceptere kode og biblioteker, der er godkendt. Men, det er altid en risiko at noget trods det ikke er ok, så det er bedst med mindst 3 uafhængige godkendte biblioteker. Og normalt er det ikke et problem, når vi sikre os, at der altid er flere hold, som laver samme kode.

  • 0
  • 0
Kjeld Flarup Christensen

I dag køber man oftest færdige chips der er gennemtestet og knytter så de enkelte komponenter sammen til en færdig løsning.

Samme fremgangsmåde bør man benytte til software. Undgå så vidt muligt boilerplate kodning. En kilde til fejl uanset hvad!


Det er derfor sprog som Python, PHP, Ruby og mange flere har vundet så stor udbredelse.
Alle sprogene har tilknyttede Open Source library repositories hvor man blot skriver 'pip install fed-feature' og så kan man lave en fancy applikation på 1.000 linjers kode. Reelt så ligger der måske millioner af linjer bagved.

Den slags repositories, eller rettere letheden og åbenheden mangler lidt ved C/C++.

Når man kigger på github.com og gitlab.com, så har de eferhånden tilknyttet avancerede Continious Integration systemer, som kan teste komponenterne, inden reviewerne kan kigge rettelserne igennem og merge dem til master.

  • 0
  • 0
Hans Nielsen

"der kan bevise, at et givent program ikke indeholder fejl."

De fleste programer laver vel hvad de bliver bedt om ? ;-)

Kan huske at jeg for rigtigt mange år siden læste om en test af software til et atomkraftværk. Her have man brugt timmer og teste alle kombinationer, da sikkerheden er vigtigt. Men der stod også, at det nok blev sidste gang at det skete, da komplexitet var stigene.

Også står vi her, hvor vi tror at man så kan lave software som finder (alle) fejl. Selv om sådan automatiske værktøjer jo skal udvikles og bruges. Da de jo er nemme, bilige og hurtige at bruge, når de først er færdigt udviklet.


Men det bliver aldrig fejlfri, af de her, og sikkert 1000 andre grunde.

Der kan være fejl i kompejler eller fortolker
Der kan sættes forkerte flag i kompejler eller fortolker
Der kan komme nye version af kompejler eller fortolker med fejl
Der kan være fejl i CPU og hardware, så selv rigtigt kode fejler
Der kan være fejl i dokumentation, så selv rigtigt kode fejler

Det var de nemme at rette, men dem her

Hvad hjælper et program til fejlfri programering, hvis man ikke kender til de enheder og proceser som man skal styre. Selv om et program er fejlfri, så kan de enheder man skal styre være fulde af fejl. Eller proces beskrivelsen kan være fyldt med fejl.

Tænk på SKAT, Bistand, Akasse. Hvad hjælper et fejlfrit program her, når der er trivl om lovgivning og fortoklning.

Og den farligste fejl af den ALLE, når man har kørt dette program.
Betragter det som fejlfri, og derfor springer andre test over.

Også har vi ikke haft AI på banen :-)


Alt efter hvad for typer af programmer og styring vi snakker om, så er det mere vigtigt at noget er robust.

Som hvis et program, proces går ned på PC/server, så kan man kill og genstarte den. Eller automatisk overvågning og genstart hvis det sker.

Hvis vi så på første måned landning, hvor fejl i procedure overbelaster CPU. Som så er den første med IRQ og proces styring. Den begynder at springe mindre vigtige opgaver over, og sørger for at der stadigt kan styres.

Eller hvis en ventil, ved en softwarte fejl bliver åbnet (eller manuelt som på 3 mile øen) At man kan se at der er åben, at man har mulighed for at lukke den. Og at man får alamer på de fejl den resultere i.


Eller mere lag praktisk. Det gør ikke noget at ens browser, programer eller textbehandling går ned. Bare den har gemt en korekt kopi af det arbejde man er i gang med.

  • 0
  • 1
Jens Madsen

Der kan være fejl i kompejler eller fortolker
Der kan sættes forkerte flag i kompejler eller fortolker
Der kan komme nye version af kompejler eller fortolker med fejl
Der kan være fejl i CPU og hardware, så selv rigtigt kode fejler
Der kan være fejl i dokumentation, så selv rigtigt kode fejler

Det var de nemme at rette, men dem her


Du har helt ret - det er de nemme at rette. De fejl du nævner er i meget høj grad rettet, hvis du anvender metoden, med at dupplere softwaren og have en enentydig specifikation, og et 100% deterministisk programmeringssprog. "Der kan være fejl i dokumentation, så selv rigtigt kode fejler" er måske den sværeste, og beror på, at de hold der tjekker dokumentationen (specifikationen) indser, hvis noget er forkert.

Det var de nemme at rette, men dem her

Hvad hjælper et program til fejlfri programering, hvis man ikke kender til de enheder og proceser som man skal styre. Selv om et program er fejlfri, så kan de enheder man skal styre være fulde af fejl. Eller proces beskrivelsen kan være fyldt med fejl.

Tænk på SKAT, Bistand, Akasse. Hvad hjælper et fejlfrit program her, når der er trivl om lovgivning og fortoklning.

Og den farligste fejl af den ALLE, når man har kørt dette program.
Betragter det som fejlfri, og derfor springer andre test over.


Jeg er helt enig. Men, lad os være enige om, at desto bedre vi håndtere software problemet, desto færre fejl er der at pukle med. Det som gør et problem løseligt, er netop at vi kan reducere antallet af fejl. Ofte kan vi - indenfor de andre problemstillinger - også finde metoder, så vi kan reducere muligheden for fejl.

Typiske metoder er feedback fra systemet, og validering af at det opfører sig korrekt, samt lukkemetoder der sikrer at det lukkes ned i tide.

Også har vi ikke haft AI på banen :-)


I den grad, at AI giver tilfældige svar, så er spørgsmålet om det overhovedet kan defineres som programmering. Normalt, så deler vi kode op i forskellige klasser. Der er seriøs programmering, hvor at alt er 100% deterministisk, og der findes ingen tilfældighed. Og så er der games. AI hører klart under den sidste gruppe... Ikke brugbart - helt enkelt.

  • 0
  • 0
Jens Madsen

Der er tidligere nævnt muligheden for codereview.
Code review virker ikke.

Bevis fra dataundervisningen:
En reviewer blev sat til at reviewe en kode, som der er en bagdør i. Han finder bagdøren, og tænker - det er sku en god idé, og skriver adgangskoden ned... Da han senere bliver spurgt hvorfor han ikke så bagdøren, så svarer han, at han lod sig hypnotisere af den gode dokumentation til at tro at koden var uden fejl.

Konklusion:
Det er ikke tilladt, at revieweren kan se koden, og kommentarer til den. Det betyder, at review ikke er muligt.
Eneste mulighed er at have flere programmer skrevet af uafhængige, og som kører samtidigt. Kommunikationen fra kode til reviewer er et brud på sikkerheden. Det skal være uafhængige grupper, der laver kode og kopikode (hvilket kan sammenlignes med review), og dette opnås ikke ved review modellen. Review modellen, er derfor bevist ikke fungerer. Den er samtidigt ikke holdbar i retten.

Derimod modellen med flere hold, der skal lave eksakt samme fejl, er holdbar i retten. Fejl kan kun opnås ved koordineret indsats, og dermed er det tale om terror eller organiseret kriminalitet. Uden organisering, ingen mulighed for fejl. Koordinering er bevisbart. Og bevis holder i retten. Som regel har man tilmed gode værktøjer, såsom tekstbehandlinger og editorer, der kontrolerer ethvert dataflow, og kan bevise programmørens arbejde, herunder på videoer.

Vi kan diskutere modellens sikkerhed, ud fra om holdene er uafhængige. Men, der findes råd for dette.

Jeg har i mange år argumenteret for, at vi skulle indføre fængsler for intellektuelle, specielt programmører. Det vil muliggøre, at vi kan indsespære dem, uden de har adgang til omverdenen, herunder familie. Vi kan erklære dem døde. Denne type kriminelle "systemmodstandere", giver mulighed for, at vi kan lave sikre systemer.

Netop derfor, har vi kæmpe underjordiske fængsler med store svømmebasiner, hvor der umuligt kan komme uvedkommende ned eller opnås kontakt med omverdenen.

Tanken er, at vi til dels fjerner dygtige personer som vi har brug for, ved at overvåge dem, og binde dem en sag på halsen, for at aflive dem (proppe dem i underjordisk fængsel), samt at der er personer der opvokser i de underjordiske fængsler, og lever hele livet i fængsel.

  • 0
  • 2
Christoffer Kjeldgaard

Der er tidligere nævnt muligheden for codereview.
Code review virker ikke.

Bevis fra dataundervisningen:
En reviewer blev sat til at reviewe en kode, som der er en bagdør i. Han finder bagdøren, og tænker - det er sku en god idé, og skriver adgangskoden ned... Da han senere bliver spurgt hvorfor han ikke så bagdøren, så svarer han, at han lod sig hypnotisere af den gode dokumentation til at tro at koden var uden fejl.

Konklusion:
Det er ikke tilladt, at revieweren kan se koden, og kommentarer til den. Det betyder, at review ikke er muligt.
Eneste mulighed er at have flere programmer skrevet af uafhængige, og som kører samtidigt. Kommunikationen fra kode til reviewer er et brud på sikkerheden. Det skal være uafhængige grupper, der laver kode og kopikode (hvilket kan sammenlignes med review), og dette opnås ikke ved review modellen. Review modellen, er derfor bevist ikke fungerer. Den er samtidigt ikke holdbar i retten.

Sikke da noget frygteligt vrøvl - Det er jo netop hele ideen med open source software at alle kan reviewe koden og foreslå ændringer. Hvis man læser artiklen handler den om semantisk analyse af kode, hvilket principielt er det samme som sker i en kodefortolker (compiler), som sikrer en relativt høj kvalitet af den kode der kommer ud i den anden ende - Men alle der har prøvet at kompilere det samme program 2 gange ved også, at et fortolket program (build) kan være optimeret forskelligt ud fra hvilke switches der gives til compileren, selvom det er samme high-level kode, så kan det compilerede system have et sæt fejl, som den kode du har kompileret med andre switches ikke har. Bruges en anden version af compileren producerer den også anderledes bytekode end det samme kode du kompilerede tidligere.

En ting er sikkert: Kode bliver ALDRIG fejlfri. Principielt er programmeringssprog deterministiske systemer, men kun på det tidspunkt koden afvikles - derfor er det umuligt at teste for alle kombinationer af input og output af funktioner (og kombinationer af funktioner som kan kalde hinanden) i alle lag fra hardware til et high-level programmeringssprog - det kan simpelthen ikke lade sig gøre, og alle der påstår at det er muligt at lave fejlfri kode har ikke forstået hvor uendelig komplekst og foranderligt IT er.

Det man kan gøre er at minimere antallet af fejl ved at skrive intelligente tests og holde kompleksiteten nede. Det er en naturlov for programmører at når kompleksiteten stiger lineært (målt på f. eks. antallet af kodetimer / kodelinje), så stiger antallet af fejl også med en eksponentiel faktor.

  • 1
  • 0
Jens Madsen

Sikke da noget frygteligt vrøvl - Det er jo netop hele ideen med open source software at alle kan reviewe koden og foreslå ændringer.


Og det er en del af den normale dataundervisning, at denne model ikke fungerer.

Der må ikke være mulighed for overførsel af information, herunder kode til reviewer.

Open source, er kendt for at ikke kunne bruges. Det er faktisk en trussel mod sikkerheden, og der er lavet mange sikkerhedssystemer, der alene har til formål, at sikre imod at der ved en fejl skulle indgå open source, som nogen har kopieret uden tilladelser.

  • 0
  • 5
Jens Madsen

Sikke da noget frygteligt vrøvl - Det er jo netop hele ideen med open source software at alle kan reviewe koden og foreslå ændringer. Hvis man læser artiklen handler den om semantisk analyse af kode, hvilket principielt er det samme som sker i en kodefortolker (compiler), som sikrer en relativt høj kvalitet af den kode der kommer ud i den anden ende - Men alle der har prøvet at kompilere det samme program 2 gange ved også, at et fortolket program (build) kan være optimeret forskelligt ud fra hvilke switches der gives til compileren, selvom det er samme high-level kode, så kan det compilerede system have et sæt fejl, som den kode du har kompileret med andre switches ikke har. Bruges en anden version af compileren producerer den også anderledes bytekode end det samme kode du kompilerede tidligere.


Jeg ved ikke, om du helt forstår modellen som jeg angiver. Code switches har ingen betydning, og du kan også fint bruge andre compilere, der netop producerer en helt anden kode - det er faktisk en forbedring af sikkerheden, og det gør man altid. Der bruges helst andre compilere, og de producerer koden til anden hardware.

Det, som sker, er ikke en sammenligning af koden. Det, der sker, er em sammenligning af resultaterne på de specificerede grænseflader, f.eks. IO, når koden kører. Denne specifikation er lavet så det er muligt, f.eks. så at forsinkelser ikke har nogen betydning, eller at forsinkelserne er eksakt defineret, så resultatet er direkte sammeligneligt. Der anvendes flere "kloner", og den/de som fejler i forhold til de andre kobles ud, samt data på grænsefladen logges. På grund af determinismen, er alt muligt at simulere helt forfra, med præcist samme resultat. Det sikrer programmeringssprogene. De har 100% determinisme, og der kan ikke kodes noget, der svarer tilfældigt.

Der findes også metoder til at sammenligne kode. Dette kan ske på mange måder, og i flere niveauer. Som eksempel, så kan sammenligningen ske, ud fra om det står det samme, men uden hensyn til navngivning. Det kan ske ud fra, om det har samme betydning. Og det kan ske, ud fra om man forholdsvis nemt matematisk kan manipulere med koden, til at den bliver ens.

Dette er en teknik der bruges, når man skal afsløre om flere hold har kopieret kode - f.eks. fra open source.

I kritiske problemer, kan man være nødsaget til at bruge fængselsmetoden.

  • 0
  • 1
Jens Madsen

Re: Code review

Der må ikke være mulighed for overførsel af information, herunder kode til reviewer.

Altså, man kan ikke lave kodereview at have koden.
Er du sikker på, at du ikke taler om test.

Det skriver jeg også - code review er umuligt.

Det, som du kan, er at du har flere uafhængige hold, der følger samme specifikation, og laver funktionel ens kode. Du har mulighed for, at tjekke denne kode er funktionel ens på de specificerede grænseflader i forhold til specifikationen. Metoden fungerer på alle dele helt ned i bunden af systemet, hvis der bruges forskelligt hardware, forskellige operativsystemer, og forskellig compiler. Der kan også anvendes forskellige sprog.

Ved code review, har du en master code, som en person læser som en roman - dette kaldes review. I de fleste tilfælde, syntes revieweren at romanen er god, men den har bare et par problemer.

Ved min metode, har du flere hårdt arbejdende hold, er arbejder uafhængigt. De har ikke kendskab til hinandens kode, eller master koden (prototype koden). De udvikler eksakt samme program, efter samme specifikationer. Programmerne tjekkes på grænsefladen, som er defineret i specifikationen. Dette sker i hardware. Såvel fejl i hardware, som fejl i koden sikres ved, at alle skal svarer ens. Er der forskel, så kobles den der svarer forskelligt ud i forhold til de andre. Fejl logges. Og, i mange tilfælde, har man en måde så den del af koden, der kobles ud, også kobles ind igen.

Du har ikke en direkte code review, men den fysiske sammenligning på grænsefladen gør, at det svarer helt til code review. Men, det sker automatisk, og uden at "reviewerne" har kendskab til hinandens kode.

I mange tilfælde, fanges fejlene allerede før at koden bruges til noget - for alle hold, skal lave test programmer, der tjekker deres kode grundigt. Og holdenes kode udsættes for de andres test programmer, og ikke kun de test programmer, som de selv laver. Der er automatik, der sikrer bedst muligt, at test programmerne er fyldstgørende for koden. Og, man sammenligner koden, inden man bruger den til noget, på baggrund af testene. De fleste fejl opdages allerede på dette niveau - men der er naturligvis fejl, der opdages når at det kører i applikationen. Her sker dog ingen fejl, hvis det kører i fejlsikker tilstand.

Som jeg skrev tidligere, så er der ofte også en public tilstand, der bruges i offentlige sammenhæng. Her vælges den fejlende kode, med henblik på, at få offentligheden til at forstå, at sikker kode ikke er muligt. Og, fordi at man på den måde fanger hackere, og finder ud af deres hensigter, hvem de arbejder for, hvem de er, og hvilke programmører de kender.

  • 0
  • 1
Hans Dybkjær

Code review virker ikke.

Jeg ved ikke hvad du mener her. Vi bruger code review, og det virker glimrende. Inden indtjek gennemgås koden sammen med en kollega. Vi ser på hvad kravbeskrivelsen er, hvilke tests der er udformet og gennemført, hvilke dele af koden der er ændringer i og hvorfor, linje for linje, og hvilken dokumentation der er lavet eller opdateret.

Nej, det fanger ikke alle fejl. Men det fanger mange fejl og mangler i både kode, dokumentation og test, det skaber videnoverførsel, og det er betragteligt billigere end den metode du beskriver.

Metoden med uafhængige hold der analyserer og koder hver sin udgave uafhængigt, går meget dybere og vil givet fange flere fejl.
Om det er den ekstra omkostning værd, kræver mere viden, flere forsøg med metoderne. I nogle tilfælde, som Troels Henriksens eksempel med rumfærger, er prisen for fejl så høj at det helt sikkert giver værdi at fange flere af de sidste promiller af fejl. I andre, nok ikke.

  • 0
  • 0
Jens Madsen

Jeg ved ikke hvad du mener her. Vi bruger code review, og det virker glimrende. Inden indtjek gennemgås koden sammen med en kollega. Vi ser på hvad kravbeskrivelsen er, hvilke tests der er udformet og gennemført, hvilke dele af koden der er ændringer i og hvorfor, linje for linje, og hvilken dokumentation der er lavet eller opdateret.


Bevisteknisk fungerer det ikke.

Nej, det fanger ikke alle fejl. Men det fanger mange fejl og mangler i både kode, dokumentation og test, det skaber videnoverførsel, og det er betragteligt billigere end den metode du beskriver.


Netop. Når jeg laver kode laver jeg også code review - jeg reviewer typisk min egen kode. Jeg er den som er bedst inde i det, og det kræver færrest resourcer. Men, det er bestemt heller ikke kritisk kode.

Metoden med uafhængige hold der analyserer og koder hver sin udgave uafhængigt, går meget dybere og vil givet fange flere fejl.


Ja

Om det er den ekstra omkostning værd, kræver mere viden, flere forsøg med metoderne. I nogle tilfælde, som Troels Henriksens eksempel med rumfærger, er prisen for fejl så høj at det helt sikkert giver værdi at fange flere af de sidste promiller af fejl. I andre, nok ikke.


Det afhænger af opgaven.

Men, sættes krav til fejlfri kode, så er det svært at undgå metoden.

Indenfor f.eks. beregninger bruges metoden meget - man sætter flere uafhængige til at lave de samme kalkulationer, og stemmer resultaterne, så ved man at svaret er korrekt. Jeg vil tro at bankerne også anvender metoden, for at kunne få deres beregninger godkendt. Metoden er stort set den eneste, som er hacker-proof, og fungerer til kritisk kode. Den fungerer, uanset at der er direkte spioner og hacker på holdet, som har til formål at lægge bagdøre ind, eller at ødelægge funktionaliteten. Det opdages hurtigt, da koderne ikke vil kunne svare ens.

  • 1
  • 0
Hans Nielsen

ingen af rumfærgeulykkerne kan tilskrives programfejl.

Men det var tæt på, fly by wire var i sin vorden.
Startet med Apollo/Månelander og F16

Da de landet de forsøgsvis test landet de føste færger, var det ved at gå galt. Da der blev intruduceret, en forstærket positiv feetback mellem styring og pilot, på grund af "lag" i styringen. Noget nyt op det tidspunkt, samt noget ligende det, som fik et Saab Gripen til at styrte.

Kort - Se link
En ældre pilot på et stor fly have måske klaret sig bedre, end en testpilot med adralinen kørende :-)

Mente det blev løst analog, med en kondensator. (Efter hukommelse, meget langt tid siden jeg har læst det, og kan ikke finde link)

https://en.wikipedia.org/wiki/Pilot-induced_oscillation

  • 0
  • 1
Jens Madsen

Og du pontere hermed, hvorfor at fejlfri programmering aldrig kommer til at virke ;-)


Nej, det har jo ikke noget med kodningen at gøre, men specifikationen, og specielt den menneskelige faktor. Vi er her udenfor software domænet. Det betyder ikke, at der ikke eksisterer løsninger.

Som eksempel, så har vi i mange år, for at løse den menneskelige faktor i fly, anvendt en CO-Pilot.

Den nyere, og mere moderne løsning, er at bruge en Auto-Pilot som overtager, hvis automatikken detekterer fejl i den menneskelige faktor.

  • 0
  • 0
Kjeld Flarup Christensen

Den fungerer, uanset at der er direkte spioner og hacker på holdet, som har til formål at lægge bagdøre ind, eller at ødelægge funktionaliteten. Det opdages hurtigt, da koderne ikke vil kunne svare ens.


Hmm, der er du måske for optimistisk.

Hvad nu hvis verifikationen ikke stiller alle spørgsmål.
Din metode ville fejle fælt på en bufferoverrun, med mindre det og de 117 andre bagdørs betoder bliver specificeret. Og så gå det galt på metode nr. 119.

  • 0
  • 0
Jens Madsen

Hmm, der er du måske for optimistisk.

Hvad nu hvis verifikationen ikke stiller alle spørgsmål.
Din metode ville fejle fælt på en bufferoverrun, med mindre det og de 117 andre bagdørs betoder bliver specificeret. Og så gå det galt på metode nr. 119.


Tror ikke, at du forstår metoden.

Der er forskellige programmører, der laver identisk kode. Den identiske kode er lavet ud fra samme specifikation, uden at kende hinandens kode. En buffer overrun, kan ikke forekomme i alle kloner. Er der f.eks. 5, så vil den med bufferoverrun ikke svare, og resultatet fra de øvrige 4 bestemmer resultatet. Dette sker som sagt mens programmerne kører - og derfor, så koster det CPU resourcer, eller ekstra hardware. Det er mest sikkert med ekstra hardware.

I mange tilfælde, viser det sig dog at det svarer hurtigere. Vælges f.eks. 5 der kører samtidigt, så kan man vælge at ens svar fra 3 er nok. Det betyder, at hvis en af holdene, ikke har forstået at lave en effektiv algorithme, og bruger en O(n^2) metode, mens de andre bruger korrekt O(log(n)) metode, så er svaret O(log(n)). Kort, så kan vi sige, at svartiden er n gange større, hvor n er antallet af samtidige hold, hvis det bruger samme CPU, men da der vælges de bedste 3 algorithmer, så kobles fjolserne fra, og det giver hurtigt et hurtigere svar. Ud fra store O funktionen, er metoden således altid hurtigere da O(k) intet betyder, hvor k er antallet af hold, som er en konstant.

  • 0
  • 2
Kjeld Flarup Christensen
  • 0
  • 0
Jens Madsen

Du mener noget i stil med det system der var på rumfærgen, hvor tre computere skulle stemme om hvordan færgen skulle styres.


Ja, det er eksakt samme system.

I nogle sammenhæng er det måske udbygget lidt, men det kan det også have været på rumfærgen, uden det er noget vi har hørt om. Jeg har beskrevet det meget kort i det første indlæg.

Inden det når til en rumfærge, så vil det allerede være gået igennem en række tests, som de forskellige hold har defineret. Under disse tests laves desuden nogle målinger på de pågældende holds software performance, f.eks. hvor mange instruktioner der køres, hvor stor strømforbrug det medfører, hvor godt strømforbruget styres, hvor stort ram forbruget er, hvordan ram forbrugets mønster ændres, og alle disse parametere analyseres for alle programmerne, så det også er nemt at se, om nogen programmer f.eks. har en bedre store O funktion end andre af programmerne. I nogle tilfælde, kan være nødvendigt, at enten få forbedret nogle af programmerne først, eller det kan være nødvendigt at helt kassere en af dem. Så, når de installeres på rumfærgen og stemmer om svaret, så er det sidste fase. Der er normalt også logging systemer, og der er styr på hvem og hvor at softwaren kommer fra, så man kan finde den ansvarlige. Som regel er tidspunkt stemplet, og det er muligt at bevise kodens indtastning, videoer osv.

  • 0
  • 0
Niels Danielsen
  • 2
  • 0
Niels Danielsen
  • 1
  • 0
Niels Danielsen

Inden for sikkerheds relaterede kontrol systemer på maskiner, betragtes systemer hvori der indgår elektronik, FPGA'er, og software som noget der skal udføres efter IEC61508.
Der er ikke tiladt at anvende 'Fault exclusion' på denne type komponenter https://www.google.com/search?q=Fault+exclusion
Dvs. at alle fejl i HW skal detekteres inden at det når at påvirke sikkerheden. (Safe Process Time)
Der kan feks. være defineret at det max. må tage 100ms fra et nødstop aktiveres til at et relæ afbryder forsyningen til en motor.
Inden for den tid skal man kunne detektere kortsluttede ledninger, afbrændte transistoere, og CPU'er der regner forkert pga. bit flip.
Og man skal så kunne bringe systemet i sikker tilstand via. en redundant kanal.
Den CPU der overvåger dette må så bruge sin del af Safe Proces Time, f.eks. 15 ms. F.eks. kan der køre et scan hvert 10 ms, der max må tage 5 ms. Der findes værktøjer der kan kontrollere WCET (Worst Case Exceution Time) på object kode der er forholdsvis triviel.
Koden må ikke kalde OS funktioner (dynamisk allokering, og låse er forbudt), og den må ikke have unbound loops.
Man kan bede værktøject om at undersøge WCET på en object fil, givet at CPU'en f.eks. er en TSM570@300MHz (Lock-steped)
https://www.absint.com/ait/index.htm

Der findes et formelt værktøj der hedder SCADE som kan anvendes til sikkerheds relaterede systemer.
https://www.ansys.com/products/embedded-software/ansys-scade-suite

SCADE er/var? baseret på Lustre
https://en.wikipedia.org/wiki/Lustre_(programming_language)

Det anvendes også af Airbus, bemærk at for det højeste sikkerheds nivau (DAL A) anvendes der ikke noget operativ system.
http://projects.laas.fr/IFSE/FMF/J1/P04_JSouyris.pdf#page=4

  • 1
  • 0
Jens Madsen

Der er ikke tiladt at anvende 'Fault exclusion' på denne type komponenter https://www.google.com/search?q=Fault+exclusion
Dvs. at alle fejl i HW skal detekteres inden at det når at påvirke sikkerheden. (Safe Process Time)


Jeg mener fint at det jeg beskriver fungerer sammen med ovenstående. Selvom jeg skriver, at en del af hardwaren kobler ud, så betragtes det ikke som ignorering af fejl, men rettelse af fejl. Såfremt, at der er tilstrækkelige ens hold der giver samme svar, så er det ikke en fejl. Normalt vil man søge at indkoble den udkoblede del igen, for at komme tilbage på samme fejlretningsnievau. Opstår fejl, vil normalt udføres nogle fejlhåndteringsrutiner, der f.eks. sikrer at de logges. Kan man ikke fortsætte sikkert (altså, kan fejlen ikke rettes sikkert), så vil man straks udføre fejlhåndtering, der sikrer systemet lukker sikker ned. Derudover vil man normalt også tjekke på signaler, så der er feedback på alt, og i mange tilfælde er der også en model af systemet, så man kan sikre sig, at systemets svar er ok. Som jeg tidligere har nævnt, så er det nødvendigt med kode fra flere uafhængige grupper, hvis du også skal tage hensyn til menneskelige fejl, herunder tilsigtede fejl, f.eks. hacking, bagdøre, og spioners ondsindede kode. I det system som jeg beskriver, skal der koordineret indsats, hos grupper man ikke kender positionen af, for at kunne bryde systemet. I simple tilfælde, hvor vi kan acceptere at systemet stopper helt - der kan man ofte nøjes med to hold, og hvis de ikke svarer ens, så lukker systemet ned. Det kan man måske også gøre i fly, hvis det ikke betyder så meget, da der jo er en pilot. Men, det er mest brugt i industrien, hvor man bare stopper maskinen, og retter fejlene, hvorefter man starter op igen.

  • 0
  • 0
Niels Danielsen

Der er en fejl i den redundante kanal. En spion har lagt fejl ind, så den svarer ikke, når det endeligt går galt. Den fungerer kun ved test, da der så ikke er en fjentlig handling involveret.


De burde ikke kunne ske, tre senarier:
1 Udefra kommende bad actor
2 Intern bad actor
3 foreseeable misuse

Udefra kommende bad actor
Normalt kan man ikke ændre sikkerheds kritisk software remote.
Og der skal selvfølgelig være en mekaniske til at beskytte imod at installere ikke signet software.
Ofte vil der også være defineret en safety perimier, og hvis den er brudt så skal der foretages en audit af systemerne.
F.eks. hvis et 'tamper prof' segl er blevet brudt til en controller så skal den kasseres.
Jeg ved at der er diskution omkring hvad der skal ske af audit hvis der har været indbrud i en vindmølle. (NERC CIP intrusion detection)

Intern bad actor er svært at gardere sig imod.
Hvis der er fysisk adgang til en maskine, eller et fly, så er softwaren ikke nødvendigvis det sageste punkt.
F.eks. kunne man forestille sig en bad actor der delvist oversavede roden af fan bladende på begge motorere, således at de begge fejlede når flyet var kommet i luften.

Functional Safety fokusere meget på foreseeable misuse, f.eks skal man undgå at kunne bytte rundt på stik:
Cross-wired controls almost bring down Lufthansa A320
https://www.flightglobal.com/news/articles/cross-wired-controls-almost-b...

Ofte genbruges det samme hardware modul mange steder, der skal sikres imod konfiguration fejl, feks. at begge krænge rors servoer er konfigureret til at reagere som venstre side.
Eller at de er konfigureret til en forkert flytype.

En klasisk tilfælde af foreseeable misuse, er hvis en maskine er bøvlet at rengøre pga. at sikkerheds systemet forhindre masskien i at køre med en persion inde i maskinen. Og maskien er nemmest at rengøre mens den køre.
Der er personer der er kommet alvorligt tilskade pga. de har fundet ud af hvorledes at de kunne snyde f.eks. sikkerheds dørlåse ved at placere mangneter på dør rammen.

  • 1
  • 0
Niels Danielsen

Der er en fejl i den redundante kanal. En spion har lagt fejl ind, så den svarer ikke, når det endeligt går galt.


"...svarer ikke, når det endeligt går galt...."
Sådan virker det ikke i de systemer jeg har set...
Her er alle replica aktive hele tiden..
Og hvis der er signaler der normalt ikke ændre sig, så indføres der diagnose pulser for at kunne detektere fejl.

  • 1
  • 0
Jens Madsen

Sådan virker det ikke i de systemer jeg har set...
Her er alle replica aktive hele tiden..
Og hvis der er signaler der normalt ikke ændre sig, så indføres der diagnose pulser for at kunne detektere fejl.


Jeg tror på dig.

Men, skal software være 100% sikkert, så gælder:
1. Det skal være robust overfor enhver menneskelig fejl.
2. Det skal være robust overfor alle bevidste fejl.
3. Det skal være robust overfor personer der kender hinanden, og samarbejder, og som i fællesskab bevidst lægger fejl ind, eller bare tror på hinanden.
4. Det skal være robust overfor tilfældige fejl, op til en fastlagt fejlrate.
5. Det skal være robust overfor både hardwarefejl og softwarefejl.

Der skal meget mindre til, for at softwaren er troværdigt.

  • 0
  • 0
Jens Madsen

En klasisk tilfælde af foreseeable misuse, er hvis en maskine er bøvlet at rengøre pga. at sikkerheds systemet forhindre masskien i at køre med en persion inde i maskinen. Og maskien er nemmest at rengøre mens den køre.
Der er personer der er kommet alvorligt tilskade pga. de har fundet ud af hvorledes at de kunne snyde f.eks. sikkerheds dørlåse ved at placere mangneter på dør rammen.


De ydre faktorer hører som jeg ser det lidt udenfor software, men det er naturligvis mindst ligeså vigtigt. Det er også vigtigt, at softwaren overvåger det som er tilkoblet. Har vi f.eks. et display, hvor ledningen tages ud og sættes i igen, så skal vi opdage denne fejl, vi skal tage stilling til hvad der skal ske, og vi skal sikre at det kommer til at fungere igen. Sensorer der ikke virker, svarer forkert skal opdages. I mange tilfælde, har vi en model af systemet, og tjekker for rimelige svar. Har vi f.eks. problemet med magneter, så ved vi kontakterne skal svarer samtidigt, eller indenfor en bestemt tid, og ellers kan det være tale om en fejl - f.eks. at nogle har forsøgt at trylle med den, at den er gået i stykker, hænger, eller er dårlig og behøver at blive skiftet hurtigst muligt. Vi skal have tilstrækkelig redundans i systemet, til at det kan fortsætte indtil en nedlukning er muligt. Tastaturer, knapper, kontakter, switche osv. indeholder ofte flere kontakter, så vi kan måle om de fungerer. F.eks. både slutte og bryde funktion.

Der er også en række af samme type problemstillinger der tages, når man har et system, der består af forskelligt redundant hardware - evt. kodet af forskellige. Hvad skal ske, hvis der opdages fejl, og kun en svarer forkert? Hvad skal ske, hvis der er flere fejl? Hvordan skal vi lukke det ned? Hvordan skal sikres, at der ikke kan være menneskelig fejl i nedlukningssoftwaren?

Er redundansen tilstrækkelig, så kan vi i nogle tilfælde tillade os at fortsætte funktionen. Er det ikke nok, så må vi afbryde. Vi skal altid have en tilstrækkelig redundans, så vi kan fortsætte nok, til at afbryde sikkert.

Normalt så har vi overvågningstasks der sikrer sig, at alt fungerer, også selvom det ikke bliver brugt aktivt. Ofte bliver vi nød til, at kunne "aktivere" et tjek, for at sikre det fungerer som det skal. Og vi tjekker, at der ikke er personer der fusker med noget.

  • 0
  • 0
Jens Madsen

Re: Software - Rumfærger - ulykke tæt på -fly by wire

Som eksempel, så har vi i mange år, for at løse den menneskelige faktor i fly, anvendt en CO-Pilot.

Den nyere, og mere moderne løsning, er at bruge en Auto-Pilot som overtager, hvis automatikken detekterer fejl i den menneskelige faktor.

Sådan er der mig bekendt ikke nogen fly der virker... Det er faktisk omvent.
Piloterne skal være klar til at overtage kontrollen hvis autopiloten spontant kobler ud.


Mener, at automatikken overtager i mange situationer, hvis piloten f.eks. detekteres bevidstløs. Det kan ske, at flyet staller, og i kritiske situationer, overtager automatikken styringen, indtil piloten detekteres at svare korrekt.

Tror nok, at millitæret i høj grad anvender autonome robotter der overtager styringen når automatikken detekterer fejl i den menneskelige faktor. Der er også lavet flere film om det...

  • 0
  • 0
Hans Nielsen

Der er også lavet flere film om det...


Nu håber jeg ikke, at du kun har din viden der fra.

Men jeg mangler stadig svare på min sprøgsmål, som jeg synes er meget fornuftig, når man ser på Niels Danielsen meget kompetente svar og indspark i debatten.

"Lever du selv af at programere, eller er du projekt leder eller andet, på større projekter. Som involvere software, som er kritisk ?"

Tror svaret kan opklare meget.

I mit eget tilfælde er det nej, men har i min ungdom været med til meget fejlsøgning og rettelser, også i software. Og derfor fastholder jeg min egen konklution fra første indlæg, at der ikke er muligt med software at finde og fjerne alle fejl i programmer, og et forsøg på det, kan være farligt, hvis det giver falsk trykhed.

  • 0
  • 0
Jens Madsen

Og derfor fastholder jeg min egen konklution fra første indlæg, at der ikke er muligt med software at finde og fjerne alle fejl i programmer, og et forsøg på det, kan være farligt, hvis det giver falsk trykhed.


Selve artiklen omhandler det at finde alle fejl.

Mener du, at de standarder der findes, som netop har til formål at undgå fejl bør undgås, fordi at de giver falsk trykhed?

Noget, som mere end noget andet giver trykhed, er en standard med et nummer. Skal vi helt skippe numrene, for at slippe af med en falsk trykhed?

Jeg syntes, at det vil være konstruktiv, hvis du kommer med forslag til, hvordan vi undgår fejl, og specielt undgår fejl lavet af mennesker, herunder også bevidste fejl lavet af flere der samarbejder. Og jeg syntes, at det er rigtigt godt, at nogen forsker i det at undgå fejl.

  • 0
  • 0
Jens Madsen

Der står i artiklen:

*Og det er som tidligere nævnt også stadig meget svært at teste flertrådede programmer.

»Det kan man nærmest ikke. Det er også derfor, at det er et af de områder vi fokuserer på.«

Det er et meget fornuftigt område at fokusere på. Men, at det er flertrådet er ikke et problem.

Det, som er det væsentlige, er om programmet er deterministisk. Det kan flertråde programmer godt være - men som jeg tidligere skrev, sætter det nogle krav til programmet. Der må ikke være et element, som finder ud af, hvem der kommer først, for det er et helt tilfældigt svar - altid. Dette svar findes ikke. Hvis man vil vide hvem der kommer først, så er det ikke noget man "måler" men noget man vælger. Og det man vælger kommer først. For man opsætter simpelthen prioriteten på alt det, som følger til det pågældende, så det kommer først. Det eneste sted, hvor vi kan tale om hvad der kommer først, er udenfor softwaren - ved grænsen til den fysiske virkelighed. Her har vi mulighed for tidsstempling, og kan ud fra denne vælge deterministisk ud fra den pågældende tidsstempling, det som vi vælger kommer først. Tid, er noget som kun eksisterer på grænesfladen til den fysiske verden - ikke i software verdenen. Det kan sammenlignes lidt med kvantemekanik - kvantemekanikken er (så vidt vi ved nu) uden tid. Tiden eksisterer først ved berøring med en fysisk virkelighed. En delay instruktion i selve koden er således ikke muligt.

Jeg savner lidt, at man lærer om hvad der skal til, for at et programmeringssprog er deterministisk - herunder også programmeringssprog til parallel programmering, og med mulighed for interrupts.

Indenfor datalogi, er deterministisk normalt ikke kun et spørgsmål om tidsmæssige tilfældigheder, men også tilfældigheder der skyldes andre forhold. F.eks. ikke initialiserede tal, compilerens rækkefølge at oversætte, den underliggende hardware osv. Et deterministisk sprog, lever altid op til, at også kunne flyttes til enhver anden hardware platform, og man må på ingen måder i sproget kunne detektere platformen, ej heller om det er en binær computer, eller få viden til hardwarens talsystem eller deres bitbredde. Det er ikke lovligt, at f.eks. kunne se CPU hastighed, processorens type og art, eller mængden af lagerplads. Men, man må gerne sætte krav til de pågældende ting i compiler direktiver. F.eks. må man gerne sætte krav til, at udførslen skal ske på en elektronisk computer - så man sikrer sig, at programmet ikke bliver udført på mennesker, biologiske computere eller andet. Vi må heller ikke kunne detektere hvor mange parallele processer at hardwaren har, og programmet skal automatisk blive oversat til det parallele processer som er rådig. Et programmeringssprog skulle i princippet kunne oversættes til enhver platform, herunder den genererer et diagram, en FPGA, eller en ASIC. Normalt sættes også krav til et programmeringssprogs ensartethed, f.eks. at dynamiske variable, og statiske variable, er ens i syntax.

Et programmeringssprog skal altid være deterministisk.

Vi kan så spørge, hvorfor der er så mange ikke deterministiske programmeringssprog.

Hvor kommer de ikke deterministiske sprog så fra, når vi ikke må bruge dem til noget?

Jo, de hævdes at være skabt i sin tid, af en professor til de studerende, for at lære dem nødvendigheden af, at kunne datalogi...

Og de blev så udbredt i hele verden.

  • 0
  • 0
Niels Danielsen

Og derfor fastholder jeg min egen konklution fra første indlæg, at der ikke er muligt med software at finde og fjerne alle fejl i programmer, og et forsøg på det, kan være farligt, hvis det giver falsk trykhed.

Fejl kan opstå i hele kæden fra problem analyse, til afvikling af instruktioner i CPU'en.
Jeg tvivler på at det nogensinde bliver muligt at lave værktøjer der formelt kan bevise rigtigheden af software, der skal kunne løse opgaver inden for alle domæner.
Men det er meget nemmere inden for områder hvor problem domænet er nemt at formulere ’matematisk’.
Jeg har mødt en der forklarede at han havde udført en formel verifikation af logikken i det danske jernbane signal system. Det virker plausibelt.
Det er også muligt at der kan defineres et formelt sprog til beskrivelse af krypto, der på den eneside har så simpel beskrivelse at det er muligt sikre det er korrekt, samt på den anden side er fyldestgørende nok til at kunne generere kode.

Hvis man kigger på standarderne for maskin sikkerhed så indeholder det både qualitative, og quantitative krav.
-Quantitative: metrikker, hvor ofte fejler en komponent på en (usikker) måde (F.eks. B10 værdier).
-Qualitative: processer, risiko analyse, fejl træs analyse, reviews etc.
Jeg ser de qualitative krav som en erkendelse af at mange ting ikke kan løses via. et formelt bevis, men kræver erfarne folk med forskellig baggrunds viden, som analysere tingede minutiøst.
Boeings problem med B737 Max er også relateret til fejlagtig system design, ikke SW implementering.

Det at formulere kravene til sikkerheds funktioner på maskiner er ikke noget der kan sættes på formel, man kan ikke tage et billede af maskinen og få et system til at generere risiko analyse og krav til sikkerheds funktioner :-)
Men opgaven med at verificere systemet reduceres kraftigt, hvis der anvendes et værktøj der er formelt kvalificeret til opgaven.

F.eks. PNOXmulti er et system hvor man kan drag-n-drop en sikkerheds kreds, og er rettet imod elinstallatører, maskinmestre, etc. som har hoved fokus på maskin og elektrisk sikkerhed. (og ikke software udvikling)
Funktion blokken for et nødstop har indbygget ’Diagnostic Coverage’ for et to kanals nødstop op til SIL 3 (Mindre end en farlig fejl for hver 10^-7 time).
Da konfiguratoren (PC værktøjet), og funktions blokkene (Runtime kode) er sikkerheds godkendt af TÜV skal der kun udføres en system test op imod sikkerheds krav.
https://www.youtube.com/watch?v=l9ysa_tQtuU&t=46
PNOXmulti er begrænset til boolesk logisk, timere, flip-flops etc.
Men det kræver ikke den store organisation at bruge værktøjet, to personer er nok.

Med SCADE har en kvalificeret kode generator.
Men du skal selv lave funktions blokken til nødstop funktioen, samt de 20 test cases, med hver 5 trin til at teste bare denne ene simple blok.
Coverage skal teste at du kommer rundt i alle state overgange som er defineret i det grafiske sprog.
Men den kvalificerede kode generator gør at det er ikke nødvendig at teste gennemløb af alle branch instruktioner på object kode nivau.
SCADE kan meget mere end PNOXMulti, men det kræver også en større organisation på minimum 10-15 personer for at besætte alle roller.

Hvis du programmere i C med alm. compiler, så skal du teste hver eneste branch på object kode niveau, samt i princippet inspicere object koden efter hver kompilering.

Java.. og IEC61508, det er vist ikke muligt.

  • 1
  • 0
Jens Madsen

Fejl kan opstå i hele kæden fra problem analyse, til afvikling af instruktioner i CPU'en.
Jeg tvivler på at det nogensinde bliver muligt at lave værktøjer der formelt kan bevise rigtigheden af software, der skal kunne løse opgaver inden for alle domæner.
Men det er meget nemmere inden for områder hvor problem domænet er nemt at formulere ’matematisk’.
Jeg har mødt en der forklarede at han havde udført en formel verifikation af logikken i det danske jernbane signal system. Det virker plausibelt.
Det er også muligt at der kan defineres et formelt sprog til beskrivelse af krypto, der på den eneside har så simpel beskrivelse at det er muligt sikre det er korrekt, samt på den anden side er fyldestgørende nok til at kunne generere kode.

Hvis man kigger på standarderne for maskin sikkerhed så indeholder det både qualitative, og quantitative krav.
-Quantitative: metrikker, hvor ofte fejler en komponent på en (usikker) måde (F.eks. B10 værdier).
-Qualitative: processer, risiko analyse, fejl træs analyse, reviews etc.
Jeg ser de qualitative krav som en erkendelse af at mange ting ikke kan løses via. et formelt bevis, men kræver erfarne folk med forskellig baggrunds viden, som analysere tingede minutiøst.
Boeings problem med B737 Max er også relateret til fejlagtig system design, ikke SW implementering.

Det at formulere kravene til sikkerheds funktioner på maskiner er ikke noget der kan sættes på formel, man kan ikke tage et billede af maskinen og få et system til at generere risiko analyse og krav til sikkerheds funktioner :-)
Men opgaven med at verificere systemet reduceres kraftigt, hvis der anvendes et værktøj der er formelt kvalificeret til opgaven.

F.eks. PNOXmulti er et system hvor man kan drag-n-drop en sikkerheds kreds, og er rettet imod elinstallatører, maskinmestre, etc. som har hoved fokus på maskin og elektrisk sikkerhed. (og ikke software udvikling)
Funktion blokken for et nødstop har indbygget ’Diagnostic Coverage’ for et to kanals nødstop op til SIL 3 (Mindre end en farlig fejl for hver 10^-7 time).
Da konfiguratoren (PC værktøjet), og funktions blokkene (Runtime kode) er sikkerheds godkendt af TÜV skal der kun udføres en system test op imod sikkerheds krav.
https://www.youtube.com/watch?v=l9ysa_tQtuU&t=46
PNOXmulti er begrænset til boolesk logisk, timere, flip-flops etc.
Men det kræver ikke den store organisation at bruge værktøjet, to personer er nok.

Med SCADE har en kvalificeret kode generator.
Men du skal selv lave funktions blokken til nødstop funktioen, samt de 20 test cases, med hver 5 trin til at teste bare denne ene simple blok.
Coverage skal teste at du kommer rundt i alle state overgange som er defineret i det grafiske sprog.
Men den kvalificerede kode generator gør at det er ikke nødvendig at teste gennemløb af alle branch instruktioner på object kode nivau.
SCADE kan meget mere end PNOXMulti, men det kræver også en større organisation på minimum 10-15 personer for at besætte alle roller.

Hvis du programmere i C med alm. compiler, så skal du teste hver eneste branch på object kode niveau, samt i princippet inspicere object koden efter hver kompilering.

Java.. og IEC61508, det er vist ikke muligt.

Jeg kan ikke være mere enig - og vil da også godt afsløre, at det er mig, som har givet dig tommelfinger op for alle dine indlæg.

Noget af det, som gør at SW er så svært at få til at fungere, er at mange anvendte programmeringssprog ikke er deterministiske. Et ikke deterministisk sprog giver problem hele vejen igennem. Er der f.eks. en fejl, så kan denne fejl ikke reproduceres. Ved reproduktion af den fejlende tilstand, så fungerer den. En af hovedårsagerne til at vælge et deterministisk sprog, er netop muligheden for at kunne gentage fejl og analysere fejl. Og, det er de eneste, hvor du kan have flere hold, til at udføre samme opgave, og komme med samme resultat. Et ikke determinstisk sprog, vil anvende ulovlige tilfældige tilstande, og det får betydning i output. Et deterministisk sprog, er også det langt mest overskuelige, og jeg har ingen kendskab til fordele i ikke deterministiske sprog.

Den metode som jeg skriver, er primært rettet mod at lave software (altså, kun indenfor SW og hardware domænet), hvor intensionen er at opdage menneskelige fejl, herunder fejl der søges placeret bevidst, og der er metoder til at finde de pågældende, og at fange dem på video, når de taster koden til bagdøren.

Den dækker langt fra alt - men, du kan i mange sammenhænge godt tænke den ind i et bredere perspektiv, f.eks. sætte flere personer på den samme opgave - også på en maskine. Og dermed, få en del af det mekaniske med. Noget som er et problem, er at der sikkert kommer forslag til 5 maskiner, der virker på hver sin måde... Men, det kan faktisk godt være med til, at man kan vurdere de forskellige muligheder, og få en til at indse om der er fejl, eller kan gøres mere smart, når det sammenholdes.
Oprindeligt havde man samme problemer i software, men her er det løst, ved at man først laver en prototype, som specifikationen laves efter, og derved sikres ens funktion i de uafhængige kloner. Er funktionen forskelligt, så opdages det. Og det er analyserbart.

Måske lyder det meget enkelt, at lave et deterministisk sprog. Men, det er faktisk en større videnskab, end det umiddelbart lyder. Som jeg tidligere skrev, så førte det til hardwareuafhængighed, og det betyder også, at du ikke må kunne se antallet af fysiske processorer der er til rådighed i koden. Alene denne detalje medfører, at programmet skal kunne omsættes til en parallel graf, der af automatikken skal kunne yderligere paralleliseres, og der skal kunne lægges "elastikker" ind, f.eks. løkker deles op, så alle dele ikke behøver samtidigt udførsel, og denne paralleliserede version, skal herefter kunne mappes ind på den givne hardware. Her skal tages hensyn til både timing og prioriteter, således at compileren garanterer alle timingkrav. Det, at man paralelliserer den sekventielle kode totalt, betyder blandt andet, at koden ikke udføres fra start til slut - det er kun funktionen der defineres sådan. Mapning på hardware, er aldrig en del af sproget, da hardware er ukendt for sproget. Det er compileren og et eventuelt operativsystem, som gør det. Den svære del, er egentligt ikke paralleliseringen, men mapningen ned på hardware, f.eks. reduktion af antallet af paralelle processer, til det hardwaren tilbyder. Her skal sikres at alle timing krav opfyldes, og det er umuligt at de på noget tidspunkt nogensinde overskrides. Derudover, skal også være mulighed for at opsætte inputs og outputs, til at f.eks. fungere synkron (f.eks. kører mus, tastatur, skærm synkron, da at klik med musen, ellers ikke relaterer til skærmens indhold). Og, man skal kunne prioritere inputs og outputs, således at f.eks. skærmterminalen er højt prioriteret. Mange prioriteter er af intern art. Det kan bevises, at tidsinterrupt for at udføre multitasking ikke er en god idé. Enhver skift af task baseret på et tidsinterrupt, fører til dårligere udførsel, og til at det ikke sker ud fra prioriteter og realtids krav. Alt i alt, er det faktisk ikke nogen helt simpel udgave. Så kommer også mapning på hardwaren. Her skal vi gerne kunne vælge mange hardwaretyper, og ofte kombineret. Mapper vi det på en FPGA, så vil de dele der er timing kritiske blive analyseret og sorteret, således at det langsomme anbringes i processorer, enten i soft processors eller hard processors i FPGA'en, mens det tidskritiske lægges i hardware. En meget skæg ting, er hvordan man laver sådan en fuldt parallelt dataflow graf til bedst mulig udførsel på en CPU struktur. Der har man behov for at analysere grafen, for at finde ud af, hvilken af koden der hører naturligt sammen. Dette oversættes, typisk til en VLIW kode, der er delvis parallelt. Disse blokke bliver herefter styret af en maskine, som sikrer at timing opfyldes, at prioriteter håndteres, og at de enkelte dele af koden udføres hurtigt og korrekt. Man går i analysen ofte baglands fra I/O.

Ja, alt i alt, så kan vi sige, at vi har noget meget kompleks også i compileren, og det er derfor vigtigt, at vi også kan dupplere denne del flere gange (forskellige compilere), og sikre de fungerer ens. I nogle tilfælde, bruges forskellige sprog for holdene.

  • 0
  • 0
Morten Bøgh

Kurt Gödel - matematiker, fra 1940’erne, kollega og ven med Albert Einstein i Princeton - mente (dvs. kunne matematisk bevise) at: Vi kan ikke på forhånd vide hvad den simplest mulige beskrivelse af et system er. Dvs man er velkommen til at opstille en hypotese, og søge at beskrive systemet ud fra denne, men der er ingen garanti for succes. Det kan vise sig at det som hidtil har krævet 2000 siders uoverskuelig beskrivelse, nu med den nye hypotese kræver 4000 sider beskrivelse, hvilket så bare er ærgerligt. Yderligere ærgerligt er at man ikke på forhånd kan sige at der må findes en eller anden hypotese i lyset af hvilken beskrivelsen af systemet bliver simplere. Super-eksemplet er Einsteins almene og generelle relativitetsteori hvor det lykkes for Einstein at samle en række fænomener (tyngde og acceleration samt masse og energi) under en fælles beskrivelse som har vist sig dækkende, trods en forbavsende simpel grundlæggende hypotese, nemlig den at lysets hastighed er konstant og udgør overgrænsen for udbredelsen af enhver information. ‘Moderne’ teoretisk fysik prøver at brodere dette anderledes, via andre grundlæggende hypoteser (nemlig streng-teori), men succesen er ikke åbenbar, og om der overhovedet eksisterer en simplere og mere dækkende teori end Einsteins, virker efterhånden tvivlsomt. Ordet ‘simpel’ kan erstattes med ‘ordnende’: Opgaven er at skabe orden via gode teorier udfra produktive hypoteser.

Kurt Gödel er for mig at se det tætteste man kommer på en indkredsning af det matematiske grundlag for korrekt programmering af it-systemer: Kvaliteten af et programmel må vurderes udfra den grad af orden som programmellets beskrivelse skaber. Det er bedre at udtrykke sig klart og kort, end langt og rodet. Programmellet skal være præget af nogle grundbegreber, som afgørende bidrager til at strukturere beskrivelsen af området, altså at skabe orden. I vore dage, dvs siden 1990’erne, sker en sådan begrebsdannelse fortrinsvis i databasedesignet og ikke i programmellet. Eller lidt mere korrekt sagt: Programmellet skal være præget af nogle fornuftige hypoteser omkring området, og disse skal afspejles i begrebsdannelsen i datagrundlaget.

Modsat gælder (jo) at der ikke er nogen overgrænse for hvor rodet et programmel og dets datagrundlag kan være - og at rod ikke nødvendigvis betyder at programmellet ikke virker. Rod betyder blot at testopgaven bliver så meget større, og fra et vist punkt uoverskuelig stor.

Som debattråden her er inde på, så er ‘programmellet’ lig det totale it-system: At programmere ovenpå et operativ-system som viser sig dårligt egnet til at bidrage til strukturering af den foreliggende opgave, er ikke positivt. At anvende programmel-biblioteker fx fra et open-source miljø (eller fx fra SAP) kan rumme lignende farer. Tro på hvad andre har lavet er oftest forudsætning for at komme igennem med opgaven, men vi kan ende langt fra ideen om at finde den maksimale grad af orden på området.

At programmere er at anvende sprog - og at skabe sprog - for at beskrive virkeligheden på et område. Ordet ‘sprog’ kan her erstattes af ord som ‘begreber’ og ‘beskrivelser’, men det er stort set det samme. Vi bør tro på at den perfekte beskrivelse ligger et sted derude i mørket, men vi har ingen garanti for at finde den. Spørgsmålet om hvorvidt vort programmel er fejlfrit, bliver et anden-ordens problem: Den primære opgave er at beskrive virkeligheden nogenlunde dækkende. Resten er et spørgsmål om rettidig omhu: At få programmeret samtlige exceptions, dvs. håndtere uventede situationer inden programmet farer vild. At udvikle i et samspil med test, grundigt og velplanlagt. At programmere løsningen to gange i to forskellige setup, fx i et prototypesprog og i en produktionsrettet løsning, og kun i sidstnævnte fokusere på brugergrænsefladen.

Kurt Gödels matematiske bevis handler om hvad man ikke kan. Det er alligevel interessant, fordi det så samtidig siger noget om hvad man bør stræbe mod: Den (matematisk) klare beskrivelse. Og dermed handler om noget som it-programmører og it-arkitekter burde have som ideal.

Kilde: Tor Nørretranders: 'Einstein, Einstein'.

  • 1
  • 0
Hans Nielsen

Du mener noget i stil med det system der var på rumfærgen, hvor tre computere skulle stemme om hvordan færgen skulle styres.


Nu mener jeg det var 5 ?
Hvoraf der blev kørt et andet oprativ system og brugt et andet programerings sprog på nogle af dem. Så en software fejl som kunne låse eller fejl ramme en enhed, ikke vil ramme alle.
Det var desuden også rigtige enhedr, store kasser fra IBM med teknologi fra opstarten af projektet i start af 1970.

Efter hukommelsen. Fra en artikkel jeg har læst for meget lang tid siden. start 90'er mener jeg.

  • 0
  • 0
Bjarne Thomsen

Kurt Gödel forærede i 1949 Einstein en fødselsdagsgave i form af et modelunivers, som Einstein uden tvilv hadede.
For Einstein kom et fysisk princip altid over en matematisk teori.
Baggrunden for Einsteins idèer var de 2 fysiske teorier omkring år 1900: a) Newtons universelle gravitation, som udbreder sig øjeblikkeligt, så Jorden ikke accelereres mod Solens tilsyneladende position, men mod dens placering 8 min senere. b) Maxwells ligninger, som viser, at elektromagnetiske bølger (lys) udbreder sig med en konstant hastighed.
Einstein fulgte Galileis argument for, at intet eksperiment kan afgøre, om man befinder sig i hvile eller bevæger sig med en konstant hastighed. Dette var egentligt et argumen mod, at Jorden behøvede at være Universets ubevægelige centrum.
Einstein greb Galileis mekaniske relativitetsprincip og krævede, at elektromagnetisk stråling skal udbrede sig med samme hastighed i alle systemer med konstante relative hastigheder. Dette er det fysiske princip bag Einsteins specielle relativitetsteori· Princippet medfører, at den newtonske absolotte samtidighed må opgives. Absolutte afstande må i stedet måles i den firedimensionale rumtid.
Einstein udviklede i de følgende 10 år den idè, at gravitationen kan forklares ved en krumning af rumtiden, idet frit faldende legemer følger geodætiske kurver i rumtiden. Krumme rum kan ikke længere beskrives ved retvinklede koordinater som i den specielle relativitetsteori. Einstein kaldte derfor sin nye garvitationsteori for den generelle relativitetsteori.
Einstein konstruerede i 1917 det første modelunivers baseret på den generelle relativitetsteori. Einstein agtede at forklare, hvad Jorden roterer i forhold til. Han opfandt et princip, som han opkaldte efter Ernst Mach. Jordens rotation må nødvendigvis måles i forhold til meget fjerne masser. Massetætheden kan derfor ikke gå mod nul i det uendeligt fjerne. Man antager ellers normalt, at Solsystemet befinder sig i et uendeligt tomt rum, når man beregner planeternes bevægelser.
Einsteins løsning var at antage, at rummet var en tredimensional kugleskal med et endeligt volumen. En kugleskal har ingen rand, så man behøver ikke at angive randværdier. Einsteins oprindelige feltligninger tillader uheldigvis ikke en statisk løsning med et endeligt rumvang. Einstein indførte derfor en integrationskonstant, som han kaldte den kosmologiske konstant.
Einstein var så begejstret for denne statiske og endelige model, at han helt overså, at den er dynamisk ustabil. Da Georges Lemaître i 1927 forsøgte at vise Einstein, at den statiske model ville ekspandere bort fra løsningen, var hans kommentar "det var dog en afskyelig tanke".
Hubbles afstandsmålinger fik dog Einstein overbevist om Universets ekspansion, men han var stadig overbevist om, Jordens rotation nødvendigvis skulle måles i forhold til de fjerne masser. Det er her Kurt Gödel kommer ind i billedet. Han konstruerede et univers, som er en løsning til Einsteins feltligninger, og hvor de fjerne masser roterer i forhold til et lokalt inertialsystem.

  • 0
  • 0
Jens Madsen

Jeg er enig i, at kode gerne skal skrives kort og præcist.

Men - det er nemmere sagt end gjort. Har du lidt erfaring, vil du ofte opleve, at det ikke er den korte og præcise formulation, som du kommer til først. Det kræver at der bruges tid og resourcer på opgaven. Erhvervslivet lukker for længst et projekt ned som løst, inden du når så langt.

En meget simpel formulering, der er nemmere at opnå, er at løse ens opgaver ens. Men, det er heller ikke så enkelt. Vi kan tage et eksempel fra programmeringsverdenen.

Hvordan skal et sprog fungere med hensyn til variable? Og, hvordan skal det fungere med hensyn til pointere?

Svaret er meget simpelt - det bør virke ens. Vi bør derfor kun have noget der svarer til referencer i C++, for så bliver koden ens, uanset om den arbejder på statiske variable, eller dynamiske. Det er altid et krav. Sproget må ikke supportere andet, for så bliver det brugt.

For pointere ved vi, at der i nogle tilfælde er erklæret plads for variable. Og andre ikke. Skal statiske og dynamiske variable fungere ens, så kræves også her ensartethed.

Allerede nu, kan vi se at C++ fejler.

For at leve op til noget så simpelt, så kræves at statiske variable også kan være uden tildelt lager - eller rettere, uden "værdi". Der skal derfor være en værdi, også for statisk lager, der betyder ikke tildelt værdi.

Og der skal virke med samme funktioner på de to lagertyper. Det vil sige, at vi skal kunne bruge delete på både referencer og på statiske variable. Og så fjernes værdien. Ved opstart, må de ikke have en tilfældig værdi, men skal være uden værdi.

Dette gælder også pointer typer - vi må ikke have nogen new instruktion, som ikke samtidigt tildeler en værdi.

Og, igen så sætter vi krav til at statiske og dynamiske variable(referencer), skal fungere ens. Så det betyder at en tildeling, skal fungere eksakt som new.

Nu har vi gået igennem bare en ganske lille smule af C++, for at se om det så var fejlfrit. Nej, det var det ikke. Det kunne ikke leve op til den simple lov om ensartethed, som er et krav i enhver form for logisk sprog.

Ensartethed er grundlaget indenfor logikkens verden, for er tingene ikke ensartet, så kan vi ikke udregne det, uden at vide det. Fungerer det ens, så kan vi meget nemt regne ud, også hvordan noget andet fungerer. Og det er jo netop sagen. Det gør det nemmere at forstå. Når vi ser noget kode, skal vi ikke "arbejde" med den inde i hovedet. Vi ved, hvad den laver, uden at vi skal ombytte symboler først.

Hvad er så pointen i denne historie - jo, det er at det at lave noget simpelt er ikke nemt. Og uanset, hvor mange der læser review på et programmeringssprog, så er der ingen brokkerier over hverken mangel på enkelthed. Og, der er ingen som foreslår, hvordan det skulle være i stedet. Det, som alle gør, er udenadslære. De lærer udenad, at i tilfælde a, så skal det være sådan, og i tilfælde b, så skal det være på en anden måde, på trods af, at problemerne er totalt ens. Logik, og enkelthed, virker ikke til, at være det som mennesker har nemmest ved at indsé. De fleste kan ganske enkelt ikke hverken se mangel på logik, eller forstå logik. De fleste kan dog godt lære det - så længe de ikke selv skal indse, opdage, eller opfinde noget logisk.

Generalt, så gælder det, at det at lave ting logisk, er en ekstra anstrengelse, som de færreste giver. De vil hellere skrive 2000 kodelinjer ekstra, end bruge hjernen til at gøre ens ting ens.

  • 0
  • 0
Log ind eller Opret konto for at kommentere