his.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • 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
University of Skövde, School of Humanities and Informatics. University of Skövde, The Informatics Research Centre.
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.

Place, publisher, year, edition, pages
Linköpings universitet , 2009. , 150 p.
Series
Linköping Studies in Science and Technology, Dissertations,, ISSN 0345-7524 ; 1262
Keyword [en]
ECA rules, Timed automata, Formal verification
National Category
Engineering and Technology
Research subject
Technology
Identifiers
URN: urn:nbn:se:his:diva-3206ISBN: 978-91-7393-598-2 OAI: oai:DiVA.org:his-3206DiVA: diva2:225354
Public defence
(English)
Available from: 2009-06-26 Created: 2009-06-26 Last updated: 2013-03-26Bibliographically approved

Open Access in DiVA

No full text

Other links

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

Search in DiVA

By author/editor
Ericsson, AnnMarie
By organisation
School of Humanities and InformaticsThe Informatics Research Centre
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

Total: 60 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • 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