Logotype Mälardalen University

MRTC publications



Scheduling Timed Modules for Correct Resource Sharing

Full text:  
Full text:
Authors: Cristina Seceleanu, Paul Pettersson, Hans Hansson
Source: In Proc. of the 1st IEEE International Conference on Software Testing, Verification and Validation (ICST 2008), IEEE Computer Society
 

Abstract

Real-time embedded systems typically include concurrent tasks of different priorities with time-dependent operations accessing common resources. In this context, unsynchronized parallel executions may lead to hazard situations caused by e.g., race conditions. To be able to detect such faulty system behaviors before implementation, we introduce a unified model of resource constrained, scheduled real-time system descriptions, in Alur’s and Henzinger’s rigorous framework of timed reactive modules. We take a component-based design perspective and construct the real-time system model, by refinement, as a composition of real-time periodic preemptible tasks with encoded functionality, and a fixed-priority scheduler, all modeled as timed modules. For the model, we express the notions of race condition and redundant locking, formally, as invariance properties that can be verified by model-checking.
 

BibTeX entry

@inproceedings{Seceleanu_1385:2008,
   author = {Cristina Seceleanu and Paul Pettersson and Hans Hansson},
   title = {Scheduling Timed Modules for Correct Resource Sharing},
   booktitle = {In Proc. of the 1st IEEE International Conference on Software Testing, Verification and Validation (ICST 2008)},
   month = {April},
   year = {2008},
   publisher = {IEEE Computer Society},
   url = {http://www.mrtc.mdh.se/index.php?choice=publications&id=1385},
}

  • Mälardalen University |
  • Box 883 |
  • 721 23 Västerås/Eskilstuna |
  • 021-101300, 016-153600 |
  • webmaster |
  • Latest update: 2010.05.10