Name
Abstract | ||
|---|---|---|
Guaranteeing timing properties is an important issue as we develop safety-critical real-time systems such as cardiac pacemakers. We present a safety assured development approach of real-time software using a pacemaker as our case study. Following the model-driven development techniques, measurement-based timing analysis is used to guarantee timing properties in implementation as well as in the formal model. Formal specification with timed automata is checked with respect to timing properties by model checking technique and is transformed into implementation systematically. When timing properties may be violated in the implementation due to timing delay, it is suggested to measure the time deviation and reflect it to the code explicitly by modifying guards. The model is altered according to the modifications in the code. These changes of the code and the model are considered safe if all the properties are still satisfied by the modified model in re-performed model checking. We demonstrate how the suggested approach can be applied to single-threaded and multi-threaded versions of implementation. This approach can provide developers with a useful time-guaranteeing technique applicable to several code generation schemes without imposing many restrictions. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1109/RTCSA.2010.42 | RTCSA |
Keywords | Field | DocType |
real-time software,cardiac pacemaker,implementation systematically,code generation,real time software,time deviation,timed automata,safety-assured development approach,measurement-based timing analysis,safety assured development approach,multi-threading,code generation scheme,safety critical real time system,timing property,multithreaded version,re-performed model checking,model checking technique,model driven development technique,timing delay,measurement based timing analysis,time guarantee,single threaded version,guaranteeing timing property,safety-critical software,timing analysis,real-time systems,formal specification,modified model,formal verification,formal model,program compilers,multi threading,sensors,heart,satisfiability,automata,real time systems,real time,model checking | Model checking,Computer science,Automaton,Time deviation,Code generation,Formal specification,Real-time computing,Software,Static timing analysis,Distributed computing,Formal verification | Conference |
ISSN | ISBN | Citations |
1533-2306 | 978-1-4244-8480-5 | 21 |
PageRank | References | Authors |
1.46 | 4 | 6 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Eunkyoung Jee | 1 | 213 | 17.57 |
| Shao-hui Wang | 2 | 126 | 19.62 |
| Jeong Ki Kim | 3 | 27 | 1.95 |
| Jaewoo Lee | 4 | 308 | 35.20 |
| Oleg Sokolsky | 5 | 2193 | 154.94 |
| Insup Lee | 6 | 4996 | 413.64 |