Vid formell verifiering konstruerar en designer först en modell, med matematiskt exakt semantik, av systemet under konstruktion, och utför en omfattande analys med avseende på korrekthetskrav. Den lämpliga matematiska modellen för inbyggda styrsystem är hybridsystem som kombinerar de traditionella statiska maskinbaserade modellerna för diskret styrning med klassiska differentialekvationsbaserade modeller för kontinuerligt föränderliga fysiska aktiviteter. I den här artikeln går vi kort igenom utvalda befintliga metoder för formell verifiering av hybridsystem, tillsammans med riktlinjer för framtida forskning.  Verifiering av kategorier och ämnesdeskriptorer. Hybridsystem, styrsystem, Modellkontroll, Formella metoder Modellbaserad design erbjuder ett lovande tillvägagångssätt för att upptäcka och korrigera fel i ett tidigt skede av systemkonstruktionen [33, 37, 49]. I denna metod konstruerar en designer först en modell, med matematiskt exakt semantik, av systemet under konstruktion, och utför omfattande analys med avseende på korrekthetskrav innan den genererar implementeringen från modellen. Inbäddade system, såsom styrenheter i fordon, medicinska och avioniska system, består av en samling interagerande programvarumoduler som reagerar på en ständigt föränderlig miljö. Rätt tillstånd att göra digitala eller hårda kopior av hela eller delar av detta arbete för personligt bruk eller klassrum beviljas utan avgift, förutsatt att kopiorna inte görs eller distribueras för vinst eller kommersiell fördel och att kopiorna är försedda med detta meddelande och den fullständiga hänvisningen på första sidan. För att kopiera på annat sätt, för att återpublicera, för att posta på servrar eller för att omfördela till listor, krävs tidigare specifik behörighet och/eller avgift. Emsoft'11, 9–14 oktober 2011, Taipei, Taiwan. Copyright 2011 matematisk modell för design av inbyggda styrsystem är hybridsystem som kombinerar de traditionella modellerna för diskret beteende med klassiska differential- och algebraikekvationsbaserade modeller för dynamiska system. Sådana modeller kan fånga både regulatorn - systemet under konstruktion, och anläggningen - miljön med ständigt föränderliga fysiska aktiviteter där systemet fungerar. Med tanke på att (1) automatiserade verifieringsverktyg nyligen har varit framgångsrika i att hitta buggar i "real-world" maskinvaruprotokoll och enhetsdrivrutiner [13, 15], (2) verktyg som Stateflow/Simulink används ofta inom fordonsindustrin och avionikindustrin för modellering, och (3) hög säkerhet är en nödvändighet i säkerhetskritiska applikationer som distribuerar inbäddad programvara, har formell verifiering av hybridsystem varit ett levande forskningsområde under de senaste 20 åren. Denna artikel är en översikt över aktuella forskningsinriktningar, som syftar till att ge en inledande "färdplan" snarare än en omfattande enkät. I början av 1990-talet integrerades formella modeller för diskreta reaktiva system med modeller för dynamiska system [2, 41]. Modellen hybridautomata [1, 2, 29] har visat sig vara ett populärt val. En hybridautomaton är en utökad ändstatsmaskin vars tillstånd består av ett läge som sträcker sig över ändligt många diskreta värden och en finit uppsättning realvärderade variabler. Varje läge är annoterat med begränsningar som anger systemets kontinuerliga utveckling, och kanter mellan lägen annoteras med vakter och uppdateringar som anger diskreta övergångar. Till exempel, beteendet hos en självreglerande termostat kan beskrivas av en hybrid automaton med två lägen, på och av, och en enda real värderad variabel T modellera temperaturen. För att ange hur temperaturen ändras i läget på, kan vi kommentera läget med en differentialekvation, t.ex., T = k(70 − T ), för en konstant parameter k. Alternativt kan vi använda en differentialojämlikhet, t.ex. k 1 ≤ till ≤ k2, för två konstanter k 1 och k2, för att ange dynamiken ungefär genom att bara använda gränser på derivatan. I samband med att läget sätts på med en invariantrestriktion T ≤ 70 anges att systemet måste avsluta detta läge innan temperaturen överstiger 70. En kant från läge till läge av med skydd T ≥ 68 anger att när temperaturen överstiger 68, systemet kan diskret ändra sitt tillstånd genom att uppdatera läget till av. En hybridautomaton kan naturligtvis tolkas som ett oändligt tillstånd övergångssystem, och detta utgör grunden för att formalisera klassiska begrepp såsom säkerhetsverifiering, egendomsbevarande abstraktioner, och simuleringsrelationer, för hybridsystem. De kommersiella modelleringsverktygen såsom Stateflow/Simulink (se www.mathworks.com) och Modelica (se www.modelica. org) används rutinmässigt i många olika branscher. Konceptuellt bör det vara möjligt att sammanställa modeller som uttrycks i sådana verktyg till formella noteringar som hybridautomata. Detta har visat sig vara svårt i praktiken på grund av den rikedom av funktioner i kommersiella verktyg och bristen på en standardiserad formell semantik av sådana funktioner (se [35] för insatser som syftar till semantik-bevarande omvandlingar över modellering notationer). I säkerhetskontroll problemet för hybridsystem, vi får en hybrid system modell M, en uppsättning I av inledande tillstånd av M, och en uppsättning S av "säkra" tillstånd av M, och vi vill kontrollera om varje utförande av M börjar i ett initialt tillstånd alltid stannar inom uppsättningen av säkra stater, och om inte, rapportera en överträdelse avrättning som ett motexempel. Med tanke på hybridsystemets modell för ett kollisionsundvikande protokoll vill vi till exempel kontrollera om avståndet mellan två fordon förblir större än säkerhetströskeln för givna ursprungliga förhållanden. Låt oss först notera att problemet med säkerhetsverifiering av hybridsystem inte kan lösas algoritmiskt: med undantag för klasser som kraftigt begränsar den tillåtna dynamiken hos verkligt värderade variabler såsom tidsinställd automata [5] och initialiserad rektangulär automata [32] är säkerhetsverifieringsproblemet obeslutsamt [1, 32]. Symbolisk räckvidd algoritmer för säkerhetsverifiering försöker beräkna uppsättningen R av nåbara tillstånd i ett hybridsystem M på ett iterativt sätt med början från uppsättningen I av initialtillstånd. Algoritmen kontrollerar, i varje steg av iterationen, om den nuvarande uppsättningen R av nåbara tillstånd är en delmängd av den uppsättning S av säkra tillstånd, och om inte, avslutas den med ett motexempel. I allmänhet finns det ingen termineringsgaranti, eftersom algoritmen kan fortsätta att lägga till fler och fler stater till R utan att kunna dra slutsatsen att systemet är säkert. Den viktigaste utmaningen för ett effektivt genomförande är att identifiera en lämplig representation för den uppsättning stater som stöder den verksamhet som används vid den iterativa tillförlitlighetsberäkningen. Verktyget HyTech var den första modellen kontroll att genomföra symbolisk räckvidd analys för hybridsystem [7, 31]. För en hybridautomaton med n real- valued variabler, varje nåbar uppsättning representeras genom att associera en finit förening av ndimensionell polyhedra med varje läge, där en polyhedron representeras som en förening av linjära ojämlikheter över variabler. En sådan polyhedra-baserad representation är tilltalande på grund av användningen av polyhedra i många datorprogram och tillgången till bibliotek med öppen källkod för att manipulera dem (c.f. Denna förordning träder i kraft den tjugonde dagen efter det att den har offentliggjorts i Europeiska unionens officiella tidning. Modellerna är begränsade till klassen linjär hybrida automata (LHA): vakter, uppdateringar, och invarianter omfattar endast linjära uttryck, och dynamiken specificeras med hjälp av skillnader ojämlikheter som är linjära begränsningar över första ordningen derivat. Till exempel beskriver den LHA-tillåtna dynamiken en tvådimensionell rörelse längs diagonallinjen med hastighetsgränser. För LHA är polyhedral representation stängd under både diskreta övergångar som motsvarar mode-brytare och kontinuerlig utveckling enligt differentialbegränsningar i ett läge: givet en polyhedron R som beskriver uppsättningen av aktuella tillstånd, den uppsättning R av tillstånd som systemet kan nå efter en diskret mode-omkopplare till ett mode m, är också en polyhedron som kan beräknas effektivt från R, och den uppsättning R av tillstånd som systemet kan nå som ett resultat att låta det utvecklas kontinuerligt enligt dynamiken som är associerad med mode m, är också en polyhedron som kan beräknas effektivt från R. Den mest använda dynamiken i matematisk utformning av styrsystem omfattar linjära differentialekvationer: om x representerar vektorn för statsvariabler, U representerar vektorn för indatavariabler, beskrivs ett linjärt system med ekvationen = Ax + Bu, där A och B är matriser av lämpliga dimensioner. En sådan dynamik är inte tillåten i LHA. Linjära hybridsystem (LHS) avser den klass av hybrida automata där vakter, uppdateringar och invarianter endast omfattar linjära uttryck, och dynamiken specificeras med linjära differentialekvationer. Lägg först märke till att polyhedral representation inte är stängd under kontinuerlig evolution specificerad av linjära differentialekvationer: om x = 1 är det initiala tillståndet och dynamiken ges av den linjära differentialekvaturen x = x, är uppsättningen av nåbara tillstånd den exponentiella kurva som ges av e t, för reella tal t ≥ 0. Eftersom det är svårt att beräkna transcendentala funktioner, är en populär strategi, som först förespråkas av verktyget Checkmate [14], och senare förfinas av verktyget d/dt [11], att beräkna över tillnärmningar av nåbara uppsättningar med hjälp av polyhedral representationer. Eftersom en polyhedron R representerar uppsättningen av aktuella tillstånd, för att beräkna uppsättningen R av tillstånd som kan nås inom en fast tidshorisont Δ enligt en given linjär differentialekvation, algoritmen genomför följande strategi. För varje hörn vertex v av R, beräknar det först tillståndet v av systemet vid tiden Δ börjar i tillstånd v. Sedan beräknar det konvexa skrovet R 1 av alla hörn hörn hörn v av R och deras respektive bilder v. Vi är garanterade att alla system trajectories börjar i polyhedron R 1 och slutar i R 1 vid tiden Δ, men är inte nödvändigtvis inuti R1 vid mellanliggande tider. Det sista steget innebär att beräkna den polyhedron R 2 som erhålls genom "ansiktslyftning" R1: antalet och normala vektorer för fasetter av R 2 sammanfaller med R1, men fasetterna flyttas utåt för att inkludera alla nåbara tillstånd upp till tiden Δ. Alla dessa steg kan effektivt genomföras för linjära system, och den resulterande polyhedron R 2 garanteras vara en superuppsättning av den önskade uppsättningen R. Processen kan upprepas för successiva tidsintervall, och den resulterande approximationen av den nåbara uppsättningen kallas flödespipe approximation. Komplexiteten i verksamheten på polyhedra är exponentiell i antalet dimensioner (dvs. antalet verkligt värderade variabler i hybridsystemet), och eftersom sådana operationer åberopas upprepade gånger i symbolisk analys baserad på polyhedral representation, har en betydande mängd arbete varit 274 som syftar till att bekämpa denna komplexitet och / eller ersätta polyhedra med alternativa representationer [11, 21, 36, 42]. Representation med hjälp av zonotopes och stödfunktioner [22, 26] har hittills resulterat i den mest skalbara metoden för analys av linjära hybridsystem, vilket leder till verktyget SpaceEx som kan analysera, till exempel, en komplex 28-dimensionell helikopterstyrning [20]. Vid reduceringsverifiering interagerar en designer med en mekaniserad teoremprovare för att skapa bevis på att systemen är korrekta. För säkerhetskontroll av diskreta system, en klassisk bevisprincip bygger på begreppet induktiva invarianter: för att visa att alla utföranden av ett system M som börjar i en initial uppsättning jag stannar inom en säker uppsättning S, identifierar vi en statlig egendom  på ett sådant sätt att (1) alla initiala stater uppfyller  och (2) är en delmängd av den önskade säkerhetsfastigheten S, och (3) egendomen är bevarad lokalt över systemövergångar (dvs. ingen övergång av systemet ändrar värdet av  och från 1 till 0). Vid interaktiv verifiering föreslår användaren en egenskap, och analysverktyget kontrollerar om det är en induktiv invariant. Begreppet induktiva invarianter för diskreta system har generaliserats och anammats till kontinuerliga dynamiska (och hybrida) system. Vi kommer informellt att förklara det första sådana begrepp, som kallas barriärcertifikat [47, 48]. För att visa att ett dynamiskt system M med dynamik att = f (x) med initial set jag uppfyller en säkerhetsfastighet S, identifierar vi en funktion från staterna till reals sådan att (1) i alla inledande tillstånd, värdet av  till är icke-negativa; (2) i alla osäkra tillstånd (dvs stater inte i den säkra uppsättningen S), värdet av  till är negativt; och (3) Lie derivat av  med avseende på vektorfältet f är positiv på gränsen som (kallas barriären) kännetecknas av  till x = 0. De två första villkoren säkerställer att barriären separerar de ursprungliga tillstånden från de osäkra tillstånden, och det tredje villkoret säkerställer att systemtrajectories inte kan undkomma barriären inifrån som vid barriären flödesfältet pekar inåt. Tillsammans innebär dessa villkor att  ska(x) ≥ 0 är en induktiv invariant av systemet. Vanligtvis är den önskade funktionen  på en polynom funktion av systemvariabler. Det är också värt att notera att barriärcertifikaten är nära relaterade till begreppet Lyapunov-certifikat för stabilitet i klassisk kontrollteori. Begreppet olika varianter generaliserar barriärcertifikat [44]: det lindrar det tredje villkoret, och tillåter också mer allmänna former av logiska påståenden som potentiella invarianter. Kontroll av säkerhetsegenskaper som grundar sig på identifiering av induktiva invarianter undviker iterativ beräkning av nåbara tillståndsuppsättningar och är inte begränsad till linjära system. Verktyget KeYmaera erbjuder stöd för att bevisa riktigheten i hybridsystem med hjälp av avdragsverifiering [43, 44]. För att kontrollera om ett visst polynomcertifikat uppfyller alla de villkor som krävs för att det ska vara ett barriärcertifikat, måste verktyget utföra symbolisk differentiering, och beräkningar som förenkling och kvantifiering, med formler i teorin om reals med aritmetiska operatörer. För att helt automatisera den avdragsgilla verifieringen måste ett sådant verktyg automatiskt generera kandidater för induktiva invarianter, och detta är fortfarande ett aktivt forskningsområde (se [28, 50] för automatisk generering av invarianter genom instantiering av mallar och [45] för att generera invarianter genom fixpoint-beräkning). En abstraktion A av en modell M är en "förenklad" modell som erhålls från M sådan att bevisa säkerhet och timliga egenskaper hos A är ett tillräckligt villkor för att bevisa motsvarande egenskaper hos M. Abstraction är en effektiv strategi för skalbarhet av verifieringsverktyg, förutsatt att det finns ett sätt att beräkna A från M på ett verktyg-stödd sätt, och ett sätt att förfina den aktuella abstraktionen A om det inte är lämpligt att bevisa de önskade egenskaperna. När det gäller hybridsystem kan enkelheten i den abstrakta modellen A vara av olika former: A kan vara diskret medan M är kontinuerlig; A kan ha linjär dynamik medan M har icke-linjär dynamik; och A kan vara en linjär modell av dimensionalitet lägre än M. Det finns en omfattande litteratur om automatisk abstraktion av hybridsystem. Vi noterar tre representativa exempel.
Mycket har skrivits om att verifiera hybridsystem REF, vanligtvis med hjälp av symboliska representationer för att över approximera stater och spår av hybrid automata.
Formal verification of hybrid systems
{'venue': "EMSOFT '11", 'journal': None, 'mag_field_of_study': ['Computer Science']}