|
1 | 1 |
|
| 2 | +@inproceedings{altuntas-vss-2025, |
| 3 | +author = {Alper Altuntas and Allison H. Baker and John Baugh and Ganesh Gopalakrishnan and Stephen Siegel}, |
| 4 | +title = {Specification and Verification for Climate Modeling: Formalization Leading to Impactful Tooling}, |
| 5 | +booktitle = {Verification of Scientific Software (VSS 2025), a workshop of ETAPS 2025: European Joint Conferences on Theory and Practice of Software}, |
| 6 | +year = {2025}, |
| 7 | +month = may, |
| 8 | +address = {Hamilton, Ontario, Canada}, |
| 9 | +url_pdf = {papers/altuntas-vss-2025.pdf}, |
| 10 | +abstract = { |
| 11 | +Earth System Models (ESMs) are critical for understanding past |
| 12 | +climates and projecting future scenarios. However, the complexity of |
| 13 | +these models, which include large code bases, a wide community of |
| 14 | +developers, and diverse computational platforms, poses significant |
| 15 | +challenges for software quality assurance. The increasing adoption of |
| 16 | +GPUs and heterogeneous architectures further complicates verification |
| 17 | +efforts. Traditional verification methods often rely on bitwise |
| 18 | +reproducibility, which is not always feasible, particularly under new |
| 19 | +compilers or hardware. Manual expert evaluation, on the other hand, is |
| 20 | +subjective and time-consuming. Formal methods offer a mathematically |
| 21 | +rigorous alternative, yet their application in ESM development has |
| 22 | +been limited due to the lack of climate model-specific representations |
| 23 | +and tools. Here, we advocate for the broader adoption of formal |
| 24 | +methods in climate modeling. In particular, we identify key aspects of |
| 25 | +ESMs that are well suited to formal specification and introduce |
| 26 | +abstraction approaches for a tailored framework. To demonstrate this |
| 27 | +approach, we present a case study using CIVL model checker to formally |
| 28 | +verify a bug fix in an ocean mixing parameterization scheme. Our goal |
| 29 | +is to develop accessible, domain-specific formal tools that enhance |
| 30 | +model confidence and support more efficient and reliable ESM |
| 31 | +development.} |
| 32 | +} |
| 33 | + |
| 34 | +@inproceedings{wilson-rtas-2025, |
| 35 | +author={Wilson, Kurt and Al Arafat, Abdullah and Baugh, John and Yu, Ruozhou and Guo, Zhishan}, |
| 36 | +booktitle={2025 IEEE 31st Real-Time and Embedded Technology and Applications Symposium (RTAS)}, |
| 37 | +title={Physics-Informed Mixed-Criticality Scheduling for {F1Tenth} Cars with Preemptable {ROS 2} Executors}, |
| 38 | +year={2025}, |
| 39 | +pages={215-227}, |
| 40 | +keywords={Mixed-Criticality Systems;Temporal Verification;Formal Methods;F1Tenth cars;UPPAAL}, |
| 41 | +doi={10.1109/RTAS65571.2025.00030}, |
| 42 | +url_pdf = {papers/wilson-rtas-2025.pdf}, |
| 43 | +abstract={ |
| 44 | +Autonomous systems are increasingly used in safety-critical domains, |
| 45 | +including industrial automation, autonomous vehicles, and the |
| 46 | +industrial Internet of Things. Verifying both the functional and |
| 47 | +temporal correctness of these systems is essential to ensure safety |
| 48 | +before deployment. However, end-to-end verification is challenging due |
| 49 | +to the interaction of continuous-time physical processes with |
| 50 | +discrete-time computational systems. Existing formal methods often |
| 51 | +assume simplified or static computational models, while traditional |
| 52 | +real-time systems focus on meeting timing constraints without |
| 53 | +explicitly linking them to physical safety. We address this gap by |
| 54 | +proposing a physics-informed mixed-criticality (MC) verification |
| 55 | +framework for cyber-physical systems, which allows the integration of |
| 56 | +computational and physical models for dynamic, fine-grained safety |
| 57 | +assurance. Our framework incorporates feedback from the local |
| 58 | +environment to guide criticality-based mode switching, ensuring |
| 59 | +adaptive responses to real-time physical states rather than relying on |
| 60 | +global worst-case assumptions. We demonstrate the feasibility of our |
| 61 | +approach with a prototype implementation on an autonomous F1 Tenth |
| 62 | +vehicle using preemptive EDF scheduling on ROS 2. Verification is |
| 63 | +conducted using UPPAAL to validate system behavior, mode transitions, |
| 64 | +and physical safety constraints. Results show that our framework |
| 65 | +effectively manages MC requirements, enhancing responsiveness and |
| 66 | +safety in dynamic environments.} |
| 67 | +} |
| 68 | + |
| 69 | +@inproceedings{wilson-hscc-2025, |
| 70 | +author = {Wilson, Kurt and Arafat, Abdullah Al and Baugh, John and Yu, Ruozhou and Liu, Xue and Guo, Zhishan}, |
| 71 | +title = {Soteria: A Formal Digital-Twin-Enabled Framework for Safety-Assurance of Latency-Aware Cyber-Physical Systems}, |
| 72 | +booktitle = {Proceedings of the 28th ACM International Conference on Hybrid Systems: Computation and Control}, |
| 73 | +year = {2025}, |
| 74 | +isbn = {9798400715044}, |
| 75 | +publisher = {Association for Computing Machinery}, |
| 76 | +address = {New York, NY, USA}, |
| 77 | +url = {https://doi.org/10.1145/3716863.3718028}, |
| 78 | +doi = {10.1145/3716863.3718028}, |
| 79 | +articleno = {22}, |
| 80 | +numpages = {11}, |
| 81 | +keywords = {Formal Methods, Hybrid Systems and Models, Real-Time Cyber-Physical Systems, Temporal Verification}, |
| 82 | +location = {Irvine, CA, USA}, |
| 83 | +series = {HSCC '25}, |
| 84 | +url_pdf = {papers/wilson-hscc-2025.pdf}, |
| 85 | +abstract = { |
| 86 | +Verifying the safety of latency-aware cyber-physical systems is both |
| 87 | +critical and challenging due to the interaction between continuous |
| 88 | +physical dynamics and discrete computational constraints. This paper |
| 89 | +introduces SOTERIA, a formal framework that integrates digital twins |
| 90 | +for ensuring safety in these systems. SOTERIA models both the physical |
| 91 | +dynamics and computational behavior, enabling integrated verification |
| 92 | +within a specific operating environment. This approach goes beyond |
| 93 | +conventional methods that either treat physical and computational |
| 94 | +aspects separately or rely on overly conservative worst-case |
| 95 | +analyses. By modeling hybrid dynamics alongside computational models |
| 96 | +and operating environments, SOTERIA verifies both functional and |
| 97 | +timing correctness. Leveraging established verification tools, SOTERIA |
| 98 | +determines whether end-to-end latencies meet formal specifications, |
| 99 | +bridging the gap between computational and physical requirements. We |
| 100 | +first introduce a simple example of a 1D adaptive cruise control |
| 101 | +system to illustrate its effectiveness. We then present findings from |
| 102 | +a case study using the F1Tenth racing car platform and the UPPAAL tool |
| 103 | +to demonstrate SOTERIA's effectiveness in realistic scenarios, |
| 104 | +enabling safety verification that was previously infeasible with |
| 105 | +conventional schedulability analyses. This work underscores the |
| 106 | +importance of an integrated verification approach for enhancing safety |
| 107 | +and reliability in autonomous systems.} |
| 108 | +} |
| 109 | + |
2 | 110 | @inproceedings{wilson-memocode-2024, |
3 | 111 | title = {Physics-Aware Mixed-Criticality Systems Design via End-to-End Verification of {CPS}}, |
4 | 112 | author = {Kurt Wilson and Abdullah Al Arafat and John Baugh and Ruozhou Yu and Zhishan Guo}, |
@@ -37,8 +145,8 @@ @inproceedings{wilson-memocode-2024 |
37 | 145 | @inproceedings{banach-icgt-2024, |
38 | 146 | title = {The `Causality' Quagmire for Formalised Bond Graphs}, |
39 | 147 | author = {Banach, Richard and Baugh, John}, |
40 | | -editor = {Harmer, Russ and Kosiol, Jens}, |
41 | 148 | booktitle = {Graph Transformation}, |
| 149 | +editor = {Harmer, Russ and Kosiol, Jens}, |
42 | 150 | year = {2024}, |
43 | 151 | publisher = {Springer Nature Switzerland}, |
44 | 152 | pages = {99-117}, |
|
0 commit comments