Verifying an industrial system using REX

Användandet av formella metoder för att höja kvalitén på mjukvara används inte i någon stor utsträckning inom industrin. Vi hävdar att användandet av ett verktyg där man kan specificera sitt system i ett högnivåspråk istället för direkt i det formella språket är en möjlig väg för att förse mjukvaruutvecklare med kraftfulla verifieringsverktyg som är specifika för olika paradigmer. Verktyget REX stödjer specifikation av applikationer specificerade som en mängd regler och sammansatta händelser. Dessutom tillhandahåller REX stöd för att överföra regelbaserade modeller och applikations specifika krav från REX till det formella verktyget Uppaal. Model-checkern i Uppaal kontrolleras automatiskt av REX. I denna rapport presenteras en fallstudie där ett system som används för att planera produktionen på Volvo IT i Skövde har specificerats som regler och verifierats formellt med hjälp av REX. Syftet med fallstudien är att visa att REX kan användas för att specificera och verifiera ett komplext system som används i verkligheten.The use of formal methods for enhancing software quality is still not used in its full potential in industry. We argue that seamless support in a high-level specification tool is a viable way to provide industrial system designers with complex and powerful formal verification techniques. The REX tool supports specification of applications constructed as a set of rules and complex events. REX provides seamless support for specifying and verifying application specific requirement properties in the timed automata model-checking tool Uppaal. The rules, events and requirements of an application design is automatically transformed to a timed automaton representation and verified in the Uppaal tool. In order to validate the applicability of our approach, we present experimental results from a case-study of an industrial system. Based on the case-study results, we conclude that complex applications can be efficiently verified using our approach