You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.

The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.

For the reports in this repository we specifically note that

  • the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at http://www.ieee.org/web/publications/rights/copyrightpolicy.html)
  • the use of articles under ACM copyright is governed by the ACM copyright policy (available at http://www.acm.org/pubs/copyright_policy/)
  • technical reports and other articles issued by M‰lardalen University is free for personal use. For other use, the explicit consent of the authors is required
  • in other cases, please contact the copyright owner for detailed information

By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.

If you are in doubt, feel free to contact webmaster@ide.mdh.se

Verifying Temporal Constraints on Data in Multi-Rate Transactions

Fulltext:


Publication Type:

Conference/Workshop Paper

Venue:

proceedings of RTCSA 2000

Publisher:

IEEE Computer Society


Abstract

Transactions involving multiple tasks, possibly with different period times, are common constructs used in the design of real-time systems. Data flowing through a transaction is usually subject to temporal constraints, such as maximum time from input to output or a maximum time difference between inputs. Such constraints are of great importance to guarantee the correct functioning of the designed system. But normally they cannot be checked using the traditional approach to schedulability analysis. In this paper we describe how to use timed automata and reachability analysis to verify such temporal constraints on data in transactions. By making a timed automaton model of the data dependencies in a transaction, we enable automatic verification of timing constraints such as end-to-end latency. The model can handle different computational models and any non-preemptive execution order of the tasks in the transaction. Our experiences from industrial case studies indicate that in a substantial number of applications, the transactions are of sizes that can be handled using this approach.

Bibtex

@inproceedings{Wall190,
author = {Anders Wall and Kristian Sandstr{\"o}m and Jukka M{\"a}ki-Turja and Christer Norstr{\"o}m},
title = {Verifying Temporal Constraints on Data in Multi-Rate Transactions},
month = {December},
year = {2000},
booktitle = {proceedings of RTCSA 2000},
publisher = {IEEE Computer Society},
url = {http://www.es.mdu.se/publications/190-}
}