No description available.

Rule-based systems implemented as event-condition-action (ECA) rules utilize a powerful and flexible paradigm when it comes to specifying systems that need to react to complex situation in their environment. Rules can be specified to react to combinations of events occurring at any time in any order. However, the behavior of a rule based system is notoriously hard to analyze due to the rules ability to interact with each other. Formal methods are not utilized in their full potential for enhancing software quality in practice. We argue that seamless support in a high-level paradigm specific tool is a viable way to provide industrial system designers with powerful verification techniques. This thesis targets the issue of formally verifying that a set of specified rules behaves as indented. The prototype tool REX (Rule and Event eXplorer) is developed as a proof of concept of the results of this thesis. Rules and events are specified in REX which is acting as a rule-based front-end to the existing timed automata CASE tool UPPAAL. The rules, events and requirements of application design are specified in REX. To support formal verification, REX automatically transforms the specified rules to timed automata, queries the requirement properties in the model-checker provided by UPPAAL and returns results to the user of REX in terms of rules and events. The results of this thesis consist of guidelines for modeling and verifying rules in a timed automata model-checker and experiences from using and building a tool implementing the proposed guidelines. Moreover, the result of an industrial case study is presented, validating the ability to model and verify a system of industrial complexity using the proposed approach. / Avhandlingen presenterar en ny ansats för att formellt verifiera regel-baserade system. En verktygsprototyp, REX, är utvecklad inom ramen för detta projekt i syfte att stödja ansatsen genom realisering av de teoretiska resultaten. De regler som avses är Event-Condition-Action (ECA) regler, vilket betyder att en regel exekverar ett stycke kod (Action) om ett villkor (Condition) är sant när en specifik händelse (Event) inträffar. ECA-regler är användbara för att speci¯cera beteendet av system som måste reagera på komplexa situationer i sin interagerande miljö. En regel kan till exempel reagera på en kombination av händelser som kan inträffa när som helst och i vilken ordning som helst. Avhandlingen fokuserar på hur man med hjälp av formella metoder kan påvisa att en regelmängd beter sig som förväntat. Användandet av formella metoder för att öka kvalitén på mjukvara är inte så utbrett som det skulle kunna vara. Några av anledningarna kan vara att formella metoder anses svåra att använda och att de kräver extra tid och kunskap. Avhandlingen handlar om en approach där utvecklare kan uttrycka sitt system i ett för dem enkelt språk och där detaljer rörande det formella verktyget döljs av ett verktyg som sköter interaktionen med det formella verktyget. Regler och händelser specificeras som indata till verktyget REX som agerar som en regelbaserad front-end till det formella verktyget UPPAAL. Regler, händelser och egenskaper som modellen ska uppfylla specificeras i REX. Formell verifiering stöds genom att REX automatiskt överför regler och egenskaper till en tidsautomat som kan verifieras av Uppaal. REX startar model-checkern i UPPAAL och returnerar resultatet från analysen till användaren. Resultatet från avhandlingen består av riktlinjer för hur man kan modellera och verifiera regler i en tidsautomat samt erfarenheter från att bygga och använda ett verktyg som implementerar dessa riktlinjer. Därutöver presenteras resultat från experiment och en fallstudie som genomförts för att validera den framtagna ansatsen.

This work is focusing on automatic verification of systems with parallel running processes. We discuss the existing methods and certain possibilities of optimizing them. Existing techniques are essentially based on finding an inductive invariant (for instance using a variant of counterexample-guided abstract refinement (CEGAR)). The effectiveness of these methods depends on the size of the invariant. In this thesis, we explored the possibility of improving the methods by focusing on finding invariants of minimal size. We implemented a tool that facilitates exploring the space of invariants of the system under scrutiny. Our experimental results show that many practical existing systems indeed have invariants that are much smaller than what can be found by the existing methods. The conjectures and the results of the work will serve as a basis of future research of an efficient method for finding small invariants of parallel systems.

This thesis introduces the concept of assertion-based verifi cation of application-specifi c instruction set processors (ASIPs). The proposed design is implemented in SystemVerilog Assertions language as a part of veri fication environment created using Codasip Framework. The implemented concept is simulated in QuestaSim tool using model of Codix RISC processor. Main outcome of this thesis is the verifi cation concept usable not only on other processors, but as a part of system that automates the processor design as well.