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
Verifying transformations between timed automata specifications and ECA rules
University of Skövde, Department of Computer Science.
2003 (English)Independent thesis Advanced level (degree of Master (One Year))Student thesis
Abstract [en]

Event-triggered real-time systems are desirable to use in environments where the arrival of events are hard to predict. The semantics of an event-triggered system is well mapped to the behaviour of an active database management system (ADBMS), specified using event-condition-action (ECA) rules. The benefits of using an active database, such as persistent data storage, concurrency control, timely response to event occurrences etc. highlights the need for a development method for event-triggered real-time systems using active databases.

However, there are problems left to be solved before an ADBMS can be used with confidence in real-time environments. The behaviour of a real-time system must be predictable, which implies a thorough analysed specification with e.g. specified worst case execution times. The predictability requirement is an obstacle for specifying real-time systems as ECA rules, since the rules may affect each other in many intricate ways which makes them hard to analyse. The interaction between the rules implies that it is not enough to verify the correctness of single rules; an analysis must consider the behaviour of the entire rule set.

In this dissertation, an approach for developing active applications is presented. A method is examined which starts with an analysed high-level timed automaton specification and transforms the specified behaviour into an implicitly analysed rule set. For this method to be useful, the transformation from timed automata to rules must preserve the exact behaviour of the high level specification. Hence, the aim of this dissertation is to verify transformations between timed automaton specifications and ECA rules.

The contribution of this project is a structured set of general transformations between timed automata specifications and ECA rules. The transformations include both transformations of small timed automata constructs for deterministic environments and formally verified timed automata patterns specifying the behaviour of composite events in recent and chronicle context.

Place, publisher, year, edition, pages
Skövde: Institutionen för datavetenskap , 2003. , 142 p.
Keyword [en]
Active rules, Timed automata, Realtime systems, Transformations
National Category
Computer Science
Identifiers
URN: urn:nbn:se:his:diva-823OAI: oai:DiVA.org:his-823DiVA: diva2:3235
Subject / course
Computer Science
Educational program
Informatics - Master's Programme
Presentation
(English)
Uppsok
Technology
Supervisors
Available from: 2008-02-15 Created: 2008-02-15 Last updated: 2013-03-26

Open Access in DiVA

fulltext(975 kB)142 downloads
File information
File name FULLTEXT01.psFile size 975 kBChecksum MD5
1a512e1ef4f3abc5617497b83afc667dcd446f88252a33d2d15443d5446e534dd22970b0
Type fulltextMimetype application/postscript
fulltext(569 kB)76 downloads
File information
File name FULLTEXT02.pdfFile size 569 kBChecksum SHA-512
58477221a1eff6a220553b2a9fbfebcd9ef854f30c979141fbb8613e64fc9909309f958d7188c0ca79947bb2b197c7a43415b3b761ff37c402e205659556dbea
Type fulltextMimetype application/pdf

By organisation
Department of Computer Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 218 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

Total: 180 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