## Abstrakt

This paper presents how the tool TetaSARTS can be used to support the development of embedded hard real-time systems written in Java using the emerging Safety Critical Java (SCJ) profile. TetaSARTS facilitates control-flow sensitive schedulability analysis of a set of real-time tasks, and features a pluggable platform specification allowing analysis of systems including the hosting execution environment. This is achieved by approaching the analysis as a model checking problem by modelling the system using the Timed Automata formalism of the model checking tool Uppaal. The resulting Timed Automata model facilitates easy adjustment of a wide variety of parameters that may be of interest such as processor frequency.

This paper demonstrates that TetaSARTS can be used for tuning processor frequency, for conducting control-flow sensitive Worst Case Response Time analysis, and for conducting processor utilisation and idle time analysis.

This paper demonstrates that TetaSARTS can be used for tuning processor frequency, for conducting control-flow sensitive Worst Case Response Time analysis, and for conducting processor utilisation and idle time analysis.

Originalsprog | Engelsk |
---|---|

Tidsskrift | WiP Proceedings of the 19th IEEE Real-Time and Embedded Technology and Applications Symposium |

Sider (fra-til) | 41-44 |

Antal sider | 4 |

Status | Udgivet - 2013 |

Begivenhed | 19th IEEE Real-Time and Embedded Technology and Applications Symposium - Hyatt Regency Philadelphia at Penn's Landing, Philadelphia, Pennsylvania, USA Varighed: 10 apr. 2013 → 11 apr. 2013 Konferencens nummer: 19 http://www.cister.isep.ipp.pt/rtas2013/ |

### Konference

Konference | 19th IEEE Real-Time and Embedded Technology and Applications Symposium |
---|---|

Nummer | 19 |

Lokation | Hyatt Regency Philadelphia at Penn's Landing |

Land | USA |

By | Philadelphia, Pennsylvania |

Periode | 10/04/2013 → 11/04/2013 |

Internetadresse |

## Emneord

- Real-time
- Temporal correctness
- Real-time Java
- Safety Critical Java
- model checking
- Analysis Tools