|
1 | 1 |
|
| 2 | +@inproceedings{wilson-memocode-2024, |
| 3 | +title = {Physics-Aware Mixed-Criticality Systems Design via End-to-End Verification of CPS}, |
| 4 | +author = {Kurt Wilson and Abdullah Al Arafat and John Baugh and Ruozhou Yu and Zhishan Guo}, |
| 5 | +booktitle = {22nd ACM-IEEE International Symposium on Formal Methods and Models for System Design, MEMOCODE}, |
| 6 | +year = {2024}, |
| 7 | +publisher = {ACM/IEEE}, |
| 8 | +OPTpages = {1-1}, |
| 9 | +url_pdf = {papers/wilson-memocode-2024.pdf}, |
| 10 | +abstract = { |
| 11 | +Autonomous systems are heavily used in many safety-critical systems, |
| 12 | +such as industrial automation, autonomous cars, Industrial Internet of |
| 13 | +Things (I-IoT), etc. Verification of the functional and temporal |
| 14 | +correctness of such systems is necessary before deployment to ensure |
| 15 | +their safety. However, due to the presence of physical systems in the |
| 16 | +continuous-time domain and computational models in the discrete-time |
| 17 | +domain, end-to-end verification of these systems is highly |
| 18 | +challenging. Existing formal methods focus on verifying physical |
| 19 | +models assuming static or simplified computation models. In contrast, |
| 20 | +existing real-time systems focus on satisfying strict timing bounds |
| 21 | +but do not care how those bounds are obtained and how they relate to |
| 22 | +physical safety. Our approach bridges these two domains, and |
| 23 | +constitutes an end-to-end verification framework for arbitrary |
| 24 | +physical models and computational models incorporated within a |
| 25 | +cyber-physical automated system. By allowing the interaction between |
| 26 | +the computational and physical models, our verification framework |
| 27 | +enables a fine-grained scheme that verifies against the local |
| 28 | +environment instead of verifying against global worst-case |
| 29 | +assumptions. Moreover, to support locally varying worst-case |
| 30 | +scenarios, a mixed-criticality system is proposed where the system |
| 31 | +supports several critical models and switches among the modes based on |
| 32 | +environmental uncertainty. Finally, a proof-of-concept evaluation of |
| 33 | +the proposed framework is reported.} |
| 34 | +} |
| 35 | + |
2 | 36 | @inproceedings{banach-icgt-2024, |
3 | 37 | title = {The `Causality' Quagmire for Formalised Bond Graphs}, |
4 | 38 | author = {Banach, Richard and Baugh, John}, |
|
0 commit comments