I detta dokument presenteras en formell kontroll av kontrollsystemens egenskaper på hög nivå med hjälp av Why3-verktyget. Egenskaper som kan verifieras med detta tillvägagångssätt inkluderar bland annat stabilitet, återkopplingsvinst och robusthet. För systemen, modellerade i Simulink, föreslår vi tre huvudsteg för att uppnå verifieringen: att specificera egenskaperna av intresse över signalerna i modellen med hjälp av Simulink block, en automatisk översättning av modellen till Why3, och den automatiska verifieringen av egenskaper med Theorem visare i Why3. Vi presenterar en metod för att specificera egenskaperna i modellen och ett bibliotek med relevanta påståenden block (logiska uttryck), som för närvarande är under utveckling. Funktionaliteten hos blocken i Simulink-modellerna översätts automatiskt till Why3 som "teorier" och verifieringsmål genom vårt verktyg implementerat i MATLAB. Ett bibliotek av teorier i Why3 motsvarande varje stödd block har utvecklats för att underlätta processen för översättning. Målen verifieras automatiskt i Why3 med relevanta teoremprovare. Ett enkelt första ordningen diskret system används för att exemplifiera specifikationen av Simulink modellen, översättningsprocessen från Simulink till Why3 formella logik språk, och verifiering av Lyapunov stabilitet.
Dessutom finns det arbete med att kontrollera de kontrollrelaterade egenskaperna hos Simulink modeller med hjälp av teorem som bevisar REF.
Formal Verification of Control Systems Properties with Theorem Proving
{'venue': 'Proc. IEEE CONTROL (International Conference on Control) 2014, pp. 244 - 249, Loughborough, UK', 'journal': None, 'mag_field_of_study': ['Computer Science']}