SynQ: Synchronous System Design with Quantitative Types

QC 20261014

Abstract

Inbyggda system utgör i allt högre grad grunden för ett säkrare, effektivare och mer uppkopplat modernt liv. Följaktligen ökar antalet inbyggda system, liksom den funktionalitet de tillhandahåller. Denna situation ställer krav på utformningen och verifieringen av inbyggda system, särskilt de säkerhetskritiska, såsom de som används inom fordons-, flyg- och rymdindustrin samt inom hälso- och sjukvården. Det kräver därför att systemutformningsprocessen blir mer automatiserad och formellt redovisningsbar/rigorös. Det förstnämnda gör att processen kan bli mer effektiv och tillämplig på allt mer komplexa system, medan det sistnämnda gör att processen kan bli mer transparent och tillförlitlig för säkerhetskritiska system. Dessa två krav på en designprocess uppfylls konsekvent i ett modernt, typteoribaserat språk/bevisassistent som i allt högre grad anpassar sig till allmän programmering. Ett sådant språk gör det möjligt att harmoniskt kombinera beräkningar och formell logik i den typteori som det implementerar. Den beräkningsmässiga aspekten gör det möjligt att definiera både exekverbara modeller och tillämpliga designsteg i språket, vilket underlättar designautomatiseringen. Samtidigt gör den logiska aspekten det möjligt att formella specificera och verifiera önskade egenskaper hos systemet och designstegen i språket, vilket främjar ansvarsskyldigheten i en designprocess. Sammantaget kan ett sådant språk och en sådan typteori fungera som en idealisk metateori för en sådan ovannämnd designprocess.

Motiverat av ovanstående undersöker denna monografi hur Idris2, ett kvantitativt typteoribaserat (QTT-baserat) språk, kan stödja formellt ansvarsfulla designprocesser för synkrona system, en klass av inbyggda system som vanligtvis används i säkerhetskritiska signalbehandlings- och styrapplikationer. Mer specifikt presenterar denna monografi ett komponentbaserat designramverk, centrerat kring det inbäddade domänspecifika språket SynQ (synkron systemdesign med kvantitativa typer), i Idris2 för synkrona system.Genom att utnyttja den tagglösa slutliga inbäddningen och uttrycksfullheten i Idris2, särskilt dess kvantitativa typsystem, gör designramverket att: (1) tillståndsbaserade black-box-komponenter säkert kan användas i en designprocess och analyseras i QTT; (2) gör det möjligt att modellera system som funktionsliknande termer samtidigt som de mappas till sina implementationer på olika plattformar genom Idris2-funktioner; och (3) gör det möjligt att definiera designtransformationer på systemmodeller som Idris2-funktioner. Den första punkten garanterar att designramverket är kompatibelt med vanliga designmetoder. Samtidigt gör den andra och tredje punkten det möjligt att definiera hela designramverket, inklusive både systemmodeller och designsteg (transformations- och implementeringssteg), i Idris2 och verifiera det i QTT. Med alla dessa funktioner gör designramverket det möjligt att utnyttja både de beräkningsmässiga och logiska aspekterna av Idris2 för att leverera en formella redovisningsbar designprocess för synkrona system. Denna monografi visar således hur ett modernt typteoribaserat språk kan utnyttjas för design av synkrona system och utgör ett steg mot automatisering av systemdesign i allmänhet.

Link to DiVA