/
faq.html
564 lines (463 loc) · 36.9 KB
/
faq.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
<!DOCTYPE html>
<html lang="en">
<script src="components/header.js" type="text/javascript" defer></script>
<script src="components/navigation.js" type="text/javascript" defer></script>
<script src="components/footer.js" type="text/javascript" defer></script>
<header-component></header-component>
<body>
<navigation-component></navigation-component>
<div class="breadcrumbs margin-bottom-40">
<div class="container">
<h1 class="pull-left">FAQs</h1>
</div>
</div>
<!--=== Content Part ===-->
<div class="container">
<div class="row">
<div class="col-md-9">
<!-- General Questions -->
<p>The questions below are provided by the Pacemaker Challenge community.</p>
<div class="headline"><h2>General</h2></div>
<div class="panel-group acc-v1 margin-bottom-40" id="accordion">
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapseOne">
1. What needs have you addressed?</a>
</h4>
</div>
<div id="collapseOne" class="panel-collapse collapse in">
<div class="panel-body">
<p>Our work aims to increase the confidence on safety and efficacy of the device itself and its development process while reducing the cost due to revisions during the development process. Our research has three outcomes: </p>
<ul class="list-unstyled">
<li><i class="icon-ok color-green"></i>Reduced the <em><strong>effort for evaluation</strong></em> of closed-loop safety of the device software. This is achieved via an end-to-end verification, simulation-based testing and platform testing model-based tool chain.</li>
<li><i class="icon-ok color-green"></i>Improved <em><strong>dynamic system testing</strong></em> with interactions between the pacemaker and the heart model. We have developed an integrated functional and formal heart model to interact with the pacemaker.</li>
<li><i class="icon-ok color-green"></i> Provide a <em><strong>Model-based Development Toolchain</strong></em> to increase the confidence of the medical device software development process.</li>
</li>
</ul>
To get a quick overview of our work please watch <a href="http://youtu.be/8SK8NGldOm0" target="_blank">this short video</a> on the Heart-on-a-Chip. </div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapseTwo">
2. Who are your target readers? From which domain?
</a>
</h4>
</div>
<div id="collapseTwo" class="panel-collapse collapse">
<div class="panel-body">
<ul class="list-unstyled">
<li><i class="icon-ok color-green"></i> <strong>Software engineers</strong> overseeing requirements, specification and testing in medical device manufacturing companies</li>
<li><i class="icon-ok color-green"></i> <strong>Regulatory authorities</strong> such as the US Food and Drug Administration (FDA) for medical device software development process improvements</li>
<li><i class="icon-ok color-green"></i> <strong>Cardiac rhythm therapy algorithm designers</strong> from both academia and industry.</li>
</ul>
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapseThree">
3. What is the technology readiness level of your approach?
</a>
</h4>
</div>
<div id="collapseThree" class="panel-collapse collapse">
<div class="panel-body">
<p>Our Heart-on-a-Chip, Virtual Heart Model, Model Checking and end-to-end Model-based Design testing approach have been designed, published and are currently in the prototyping phase. This puts us in the TR4 level of readiness according to the <a href="http://www.lbl.gov/dir/assets/docs/TRL\ guide.pdf" target="_blank">DoE Technology Readiness Assessment Guide</a> (page 9)</p>
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapseFour">
4. How much time was spent to produce the solution?
</a>
</h4>
</div>
<div id="collapseFour" class="panel-collapse collapse">
<div class="panel-body">
We have invested 4 years with two productive Ph.D. students in this project.
</div>
</div>
</div>
<div class="headline"><h2>Scope</h2></div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapseFive">
1. Which parts of the pacemaker specification did you consider?
</a>
</h4>
</div>
<div id="collapseFive" class="panel-collapse collapse">
<div class="panel-body">
<p>Our focus has been on establishing high confidence in the system software and the software development process of the pacemaker. We have developed the following component evaluations: </p>
<ul class="list-unstyled">
<li><i class="icon-ok color-green"></i> Sensing and actuation - established safety criteria for the basic timing cycles and the effect of noise in sensing, lead placement, lead dislodgment and failure to sense/pace on the timing behaviors of the pacemaker software.</li>
<li><i class="icon-ok color-green"></i> Pacemaker software - established correctness of different timers in the pacemaker</li>
<li><i class="icon-ok color-green"></i> Pacemaker parameter settings - timing parameters such as Lower Rate Interval, Upper Rate Interval, A-V interval, Refractory periods, etc.</li>
</ul>
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapseSix">
2. What aspects did you consider? (e.g. System level / Hardware / Software)
</a>
</h4>
</div>
<div id="collapseSix" class="panel-collapse collapse">
<div class="panel-body">
We considered software and system level safety within the closed loop context of the pacemaker and heart.
<ul class="list-unstyled">
<li> <i class="icon-ok color-green"></i><strong>Virtual Heart Model</strong> - We have developed a Timed Automata model of the heart to interact with the pacemaker. The model incorporates the electro-physiological function of the heart. The heart model provides both functional (electrogram signals) and formal (timing events) interfaces to pacemaker models. The VHM has also been implemented in Matlab and Simulink for simulation-based testing. We have a working Heart-on-a-Chip platform for closed-loop testing with real pacemakers at the University of Pennsylvania. See details at http://pvs.medcps.org/</li>
<li><i class="icon-ok color-green"></i> <strong>Pacemaker Model Verification and Translation</strong> - We have implemented a model of the pacemaker with all the timers to satisfy the Boston Scientific specification. This model was implemented in UPPAAL (model checker for timed automata models). The verified model was then automatically translated to Stateflow/Simulink by the UPP2SF model translation tool. The tool, which was developed by us, preserves the properties proven in the verified model to Staflow's loose semantics.</li>
<li><i class="icon-ok color-green"></i> <strong>Pacemaker Tester</strong> - We implemented a large set of Medtronic timing tests. These are implemented on a hardware platform and automatically test real pacemaker hardware.</li>
<li><i class="icon-ok color-green"></i> <strong>Automated Code-generation of Verified Models</strong> - Stateflow/Simulink models are used to automatically generate pacemaker code for a variety of microcontroller architectures. </li>
</ul>
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapseSeven">
3. Which parts of the environment have you modeled?
</a>
</h4>
</div>
<div id="collapseSeven" class="panel-collapse collapse">
<div class="panel-body">
<ul class="list-unstyled">
<li> <i class="icon-ok color-green"></i><strong>Virtual Heart Model</strong> - It is important to verify and test the closed-loop heart and pacemaker system. We have a heart model to interface with pacemaker models (Timed Automata, Stateflow/Simulink), pacemakers implemented on microcontroller platforms and also real pacemakers manufactured by Boston Scientific, Medtronic and St. Jude. Currently the heart model covers the following electrophysiological arrhythmias:
<ul>
<li>
Normal Sinus Rhythm
</li>
<li>
Bradycardia</li>
<li>
Heart block</li>
<li>
Supraventricular Tachycardia</li>
<li>
Lead displacement</li>
<li>
Lead Cross-talk and race conditions</li>
<li>
Pacemaker Mediated Tachycardia</li>
</ul>
</li>
The heart model has a common kernel and exposes a functional interface} for both simulation-based and platform testing. It also exposes a formal interface of the event timing for verification of the pacemaker timing properties.
<li><i class="icon-ok color-green"></i> <strong>Blood-oxygen Physiological Modeling:</strong> For quantative verification of the closed-loop system with costs such as efficacy of therapy and device energy consumption, we have developed parts of the blood-oxygen model which interfaces with the heart and pacemaker closed-loop system. This way, we can evaluate the effectiveness of therapies related to rate-response, pacemaker mediated tachycardia and newer algorithms. </li>
</ul>
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapseEight">
4. Which process phases have you considered?
</a>
</h4>
</div>
<div id="collapseEight" class="panel-collapse collapse">
<div class="panel-body">
We focus on the requirement specification, software design, testing for certification. Our primary contribution is the development of an end-to-end model-based design approach for rapid certification of the design process. This incorporates:
<ul class="list-unstyled">
<li><i class="icon-ok color-green"></i> <strong>Formal Modeling of the Heart</strong> - timing behaviors of electric conduction of the heart are modeled by a network of timed automata. This helps us to specify requirements for pacemaker under specific heart conditions. </li>
<li><i class="icon-ok color-green"></i> <strong>Formal Modeling of the Pacemaker</strong> - majority of timing aspects in the Boston Scientific pacemaker specification are implemented using timed automata. Timing properties have been checked and verified. </li>
<li><i class="icon-ok color-green"></i> <strong>Model Translation of Verified Pacemaker Models</strong> - Automated translation of UPPAAL timed automata pacemaker model to Stateflow/Simulink while preserving verified timing properties.</li>
<li><i class="icon-ok color-green"></i> <strong>Simulation-based Testing of the Closed-loop system</strong> - Detailed heart model has also been implemented in Matlab and Simulink and interfaces with the pacemaker Stateflow/Simulink model.</li>
<li><i class="icon-ok color-green"></i> <strong>Code-generation of Verified Pacemaker Model</strong> - From the above pacemaker model we have generated code for a variety of microcontroller architectures.</li>
<li><i class="icon-ok color-green"></i> <strong>Closed-loop Platform Testing</strong> - The Heart-on-a-Chip platform incorporates the Virtual Heart Model implemented on an FPGA hardware platform and interfaces with an automated hardware tester for timing analysis. It also interfaces with real pacemakers for closed-loop platform testing.</li>
</ul>
</div>
</div>
</div>
<div class="headline">
<h2>Modeling</h2></div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapseten">
1. What modeling formalisms did you use? Why?
</a>
</h4>
</div>
<div id="collapseten" class="panel-collapse collapse">
<div class="panel-body">
<p>Timed Automata and the Mathworks toolchain. The reasons for using timed automata are: </p>
<ul class="list-unstyled">
<li><i class="icon-ok color-green"></i> Timed automata is suitable for modeling timing behaviors of a system. The coordinated contractions of the heart are based on timing behaviors of its electrical activities, which makes timed automata a good formalism to model both the heart and the pacemaker.</li>
<li><i class="icon-ok color-green"></i> Timed automata is well studied and tools like UPPAAL are available and mature.</li>
<li><i class="icon-ok color-green"></i> Most pacemaker functions we would like to cover can be modeled by timed automata </li>
</ul>
We also use the Mathworks Stateflow/Simulink/Embedded Coder toolchain as it is practical and is widely used in industry. All models and tools are publicly available. The implementation is clean and moderately easy to adopt.
The model is scalable which allows for more than enough refinement to check a large variety of common properties. See publications for more details.
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapseEleven">
2. Are the formalisms used rigorous?
</a>
</h4>
</div>
<div id="collapseEleven" class="panel-collapse collapse">
<div class="panel-body">
<p>Timed automata is a rigorous formulation. </p>
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapseTwelve">
3. How accessible are the modeling methods and notations for practicing engineers? (e.g. need training, fairly accessible)
</a>
</h4>
</div>
<div id="collapseTwelve" class="panel-collapse collapse">
<div class="panel-body">
<p>Timed automata is an extension of state machine with real-time clocks, which is intuitive for engineers. The tools and Temporal Logic are intuitive to learn with minimal training.</p>
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapse13">
4. Which aspects did you not model? Why?
</a>
</h4>
</div>
<div id="collapse13" class="panel-collapse collapse">
<div class="panel-body">
<ul class="list-unstyled">
<li><i class="icon-ok color-green"></i> <strong>On the heart side:</strong> We did not model non-timing related properties such as the mechanical contractions of the heart muscle. The performance of heart pumping can be inferred by the electrical behaviors of the heart (i.e. which is how the pacemaker interacts with the heart). This point is shown to be valid in the Cardiac Electrophysiology domain. </li>
<li><i class="icon-ok color-green"></i> <strong>On the pacemaker side:</strong> We did not model pacemaker components other than the core diagnosis/therapy software. We only focused on potential safety violations caused by the diagnosis/therapy software. The interaction between the diagnosis/therapy software and the rest of the pacemaker can be isolated by safety protocols thus the rest of the pacemaker has little impact on the safety of the diagnosis/therapy software. </li>
</ul>
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapse14">
5. What are the most difficult aspects to model?
</a>
</h4>
</div>
<div id="collapse14" class="panel-collapse collapse">
<div class="panel-body">
<ul class="list-unstyled">
<li><i class="icon-ok color-green"></i> <strong>On the heart side</strong>: How to use abstraction to cover different heart conditions and refine the heart model to pinpoint a specific heart condition. We have implemented a Counter-Example Guided Abstraction Refinement (CEGAR) methodology to verify complex closed-loop properties such as Endless-loop Tachycardia (pacemaker mode switch operation) and Pacemaker Mediated Tachycardia.</li>
<li><i class="icon-ok color-green"></i> <strong>On the pacemaker side:</strong> Advanced features which operate on heart condition history. Some of them cannot be modeled using Timed Automata. </li>
</ul>
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapse15">
6. What is the cost of the modeling?
</a>
</h4>
</div>
<div id="collapse15" class="panel-collapse collapse">
<div class="panel-body">
<p>All our models, code and platforms are publicly available for the research community. The UPPAAL tool is free and open sourced. Mathworks tools require a license to be purchased. The models themselves are easy to use and require less than a week's effort by a software engineer with 5 years of experience.</p>
</div>
</div>
</div>
<div class="headline">
<h2>Verification & Validation</h2></div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapse16">
1. What properties have you verified?
</a>
</h4>
</div>
<div id="collapse16" class="panel-collapse collapse">
<div class="panel-body">
<p>We have verified safety properties regarding avoidance of unsafe closed-loop states (i.e. low heart rate, paced high heart rate) and unsafe closed-loop executions (i.e. existence of Pacemaker Mediated Tachycardia).</p>
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapse17">
2. What properties could be ensured by construction?
</a>
</h4>
</div>
<div id="collapse17" class="panel-collapse collapse">
<div class="panel-body">
<p>Timing and correctness of software properties are verified at the abstract pacemaker model level. These properties are maintained in the Stateflow/Simulink by the UPP2SF model translation tool. The verified models are used to generate operational pacemaker code. Thus, our end-to-end model-based toolchain allows us to proceed from verified models to verified code.</p>
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapse18">
3. What methods did you use for the verification?
</a>
</h4>
</div>
<div id="collapse18" class="panel-collapse collapse">
<div class="panel-body">
Model checking of timed automata models.
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapse19">
4. How accessible are the verification methods for practicing engineers?
</a>
</h4>
</div>
<div id="collapse19" class="panel-collapse collapse">
<div class="panel-body">
Fairly accessible.
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapse20">
5. How did you validate the system?
</a>
</h4>
</div>
<div id="collapse20" class="panel-collapse collapse">
<div class="panel-body">
The heart model was based on techniques and terminologies used during clinical practices and the model has been validated by the Director of Cardiac Electrophysiology of the Philadelphia VA Hospital and the University of Pennsylvania Hospital. These hospitals are among the top hospitals responsible for the most cardiac ablation and cardiac device implants in the US.
We have also demonstrated that our model captures the timing behaviors of a real hearts (given the same input signals.) See <a href="http://youtu.be/jJjgOFxQOQ8?t=2m29s" target="_blank">Atrial Flutter video here</a></div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapse21">
6. Is the functional design verified against the requirements specification? How complete?
</a>
</h4>
</div>
<div id="collapse21" class="panel-collapse collapse">
<div class="panel-body">
Yes. For each timing cycle of the pacemaker we specified a property to verify whether the requirement has been satisfied.
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapse22">
7. Have you simulated the model?
</a>
</h4>
</div>
<div id="collapse22" class="panel-collapse collapse">
<div class="panel-body">
Yes. The models of the closed-loop system have been simulated both in model checker (UPPAAL) and Simulink.
</div>
</div>
</div>
<div class="headline"><h2>Tools</h2></div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapse23">
1. Which tools did you use? What is their maturity?
</a>
</h4>
</div>
<div id="collapse23" class="panel-collapse collapse">
<div class="panel-body">
<ul class="list-unstyled">
<li><i class="icon-ok color-green"></i> <strong>Verification:</strong> we use model checker UPPAAL. It is a mature tool that has been used for various applications.</li>
<li><i class="icon-ok color-green"></i> <strong>Model Translation: </strong> from UPPAAL to Simulink we use UPP2SF which is developed by Pajic et.al. The tool is not fully automated yet and requires some manual effort.</li>
<li><i class="icon-ok color-green"></i> <strong>Simulation & Code Generation: </strong>we use Matlab/Simulink which is widely adopted by both academia and industry. Even though Stateflow does not have formal semantics the UPP2SF tool ensures verified properties are maintained and the practicality of using Mathworks tools makes it more available than academic tools for code generation.</li>
</ul>
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapse24">
2. How much expertise is expected from the users of these tools?
</a>
</h4>
</div>
<div id="collapse24" class="panel-collapse collapse">
<div class="panel-body">
For UPPAAL, the user needs to know basic state transition system and the ability to specify requirements using temporal logic. For Matlab/Simulink the user requires basic understanding of programming and syntax of Simulink.
</div>
</div>
</div>
<div class="headline"><h2>Certification</h2></div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapse25">
1. What aspects of the functional safety certification did you cover?
</a>
</h4>
</div>
<div id="collapse25" class="panel-collapse collapse">
<div class="panel-body">
None.
</div>
</div>
</div>
<div class="panel panel-default">
<div class="panel-heading">
<h4 class="panel-title">
<a class="accordion-toggle" data-toggle="collapse" data-parent="#accordion" href="#collapse26">
2. How have you used this challenge?
</a>
</h4>
</div>
<div id="collapse26" class="panel-collapse collapse">
<div class="panel-body">
I personally have used the challenge as a case study of my research for developing a model-based design framework for Cyber-Physical Systems like medical devices.
<ul class="list-unstyled">
<li><i class="icon-ok color-green"></i> The Heart-on-a-Chip platform won the First Prize in the 9th World Embedded Systems Competition (Medical Devices category), Seoul, Korea 2012. </li>
<li><i class="icon-ok color-green"></i> Our work has won the Best Student Paper Award in the 2012 Real-Time System Conference (RTAS) at CPSWeek 2012.</li>
<li><i class="icon-ok color-green"></i> Our work was nominated for Best Paper at TACAS 2012.</li>
</ul>
Several research groups are using our models and tools. These include Marta Kwiatkowska, University of Oxford and Sanjit Seshia, UC Berkeley, etc. The models have been downloaded over 100 times in the past year.
</div>
</div>
</div>
</div><!--/acc-v1-->
</div><!--/col-md-9-->
<div class="col-md-3">
<!-- End Social -->
</div><!--/col-md-3-->
</div><!--/row-->
</div><!--/container-->
<footer-component></footer-component>
<script type="text/javascript" src="assets/css/jquery-1.10.2.min.js"></script>
<script type="text/javascript" src="assets/css/hover-dropdown.min.js"></script>
</body>
</html>