his.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Enabling Tool Support for Formal Analysis of ECA RUles
Högskolan i Skövde, Institutionen för kommunikation och information. Högskolan i Skövde, Forskningscentrum för Informationsteknologi.
2009 (Engelska)Doktorsavhandling, monografi (Övrigt vetenskapligt)
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.

Ort, förlag, år, upplaga, sidor
Linköpings universitet , 2009. , s. 150
Serie
Linköping Studies in Science and Technology, Dissertations,, ISSN 0345-7524 ; 1262
Nyckelord [en]
ECA rules, Timed automata, Formal verification
Nationell ämneskategori
Teknik och teknologier
Forskningsämne
Teknik
Identifikatorer
URN: urn:nbn:se:his:diva-3206ISBN: 978-91-7393-598-2 OAI: oai:DiVA.org:his-3206DiVA: diva2:225354
Disputation
(Engelska)
Tillgänglig från: 2009-06-26 Skapad: 2009-06-26 Senast uppdaterad: 2017-11-27Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-18427

Personposter BETA

Ericsson, AnnMarie

Sök vidare i DiVA

Av författaren/redaktören
Ericsson, AnnMarie
Av organisationen
Institutionen för kommunikation och informationForskningscentrum för Informationsteknologi
Teknik och teknologier

Sök vidare utanför DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetricpoäng

isbn
urn-nbn
Totalt: 61 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf