liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Enabling Tool Support for Formal Analysis of ECA Rules
Linköping University, Department of Computer and Information Science. Linköping University, The Institute of Technology.
2009 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

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.

Abstract [sv]

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.

Place, publisher, year, edition, pages
Linköping: Linköping University Electronic Press , 2009. , 150 p.
Series
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 1262
Keyword [en]
ECA rules, Timed automata, Formal veri¯cation
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:liu:diva-18427ISBN: 978-91-7393-598-2 (print)OAI: oai:DiVA.org:liu-18427DiVA: diva2:219144
Public defence
2009-06-16, Hus D201, Högskolan i Skövde, Skövde, 13:15 (English)
Opponent
Supervisors
Available from: 2009-05-26 Created: 2009-05-26 Last updated: 2012-01-31Bibliographically approved

Open Access in DiVA

Enabling Tool Support for Formal Analysis of ECA Rules(1087 kB)978 downloads
File information
File name FULLTEXT01.pdfFile size 1087 kBChecksum SHA-512
94dc4d443ad571b6f44d4f91f37b80fd5fbda6769b0d00f340d0741d4b2562d7c57f581e0726cde369b11e70a7ac04a2f30baa81d2a29384d0fcd99c2a050354
Type fulltextMimetype application/pdf
Cover(108 kB)50 downloads
File information
File name COVER01.pdfFile size 108 kBChecksum SHA-512
ebe6e568e24a6dffcc52fac4e9f6e008818c235e310baba4fb7895f5c9a1f834560dbfd806ba720b7dc59c92a6edbc0358efdc0d17e1bdc5536d8a31c4036e11
Type coverMimetype application/pdf

Authority records BETA

Ericsson, AnnMarie

Search in DiVA

By author/editor
Ericsson, AnnMarie
By organisation
Department of Computer and Information ScienceThe Institute of Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 978 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 1478 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf