Research

Assume-Guarantee Contracts for Design and Verification of Cyber-Physical Systems

Designing and verifying modern cyber-physical systems (CPSs) is a challenging task due to several reasons. Modern CPSs are required to meet a growing number of heterogeneous requirements while operating under strict regulations. Furthermore, the design space has expanded, requiring decisions across multiple interconnected dimensions such as control reliability, sensing accuracy, and energy consumption. CPSs must also be designed to operate effectively in uncertain environments, where they may be subject to disturbances, noise, and other factors. In addition, components within a CPS may interact cooperatively or non-cooperatively to achieve their own objectives, adding another layer of complexity. To address these challenges, we leverage assume-guarantee (A/G) contracts. A/G contracts capture the assumptions on the behaviors that a component expects from its environment and the guarantees on the behaviors that a component promises in the context of the assumptions. Given that the A/G contracts correctly abstract the behaviors of the components, the system-level design and verification tasks simplify into manageable component-level tasks.

Publications:

1.  Y. Xiao, C. Oh, M. Lora, and P. Nuzzo, “Efficient Exploration of Cyber-Physical System Architectures Using Contracts and Subgraph Isomorphism," in the Design, Automation & Test in Europe Conference & Exhibition (DATE), Mar. 2024, to appear, Best paper award in E - Embedded Systems Design - track.

2. M. Lora, S. Gaiardelli, C. Oh, S. Spellini, P. Nuzzo, and F. Fummi, "Design Automation for Cyber-Physical Production Systems: Lessons Learned from the DeFacto Project," in the Design, Automation & Test in Europe Conference & Exhibition (DATE), Mar. 2024, to appear. 

3. C. Leet, C. Oh, M. Lora, S. Koenig, and P. Nuzzo, “Task Assignment, Scheduling and Motion Planning for Automated Warehouses for Million Product Workloads,” in IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), Oct. 2023.

4. C. Leet, C. Oh, M. Lora, S. Koenig, and P. Nuzzo, “Co-Design of Topology, Scheduling, and Path Planning in Automated Warehouses,” in the Design, Automation & Test in Europe Conference & Exhibition (DATE), Apr. 2023.

5. C. Oh, M. Lora, and P. Nuzzo, “Quantitative verification and design space exploration under uncertainty with parametric stochastic contracts,” in the IEEE/ACM International Conference on Computer-Aided Design (ICCAD), Oct. 2022.

6. C. Oh, E Kang, S Shiraishi, P Nuzzo, “Optimizing assume-guarantee contracts for cyber-physical system design," in the Design, Automation & Test in Europe Conference & Exhibition (DATE), Mar. 2019.

Assume-Guarantee Contracts for Validation and Assessment of Cyber-Physical Systems

The validation and assessment of cyber-physical systems (CPSs) is a lengthy and rigorous process that demands a vast amount of evidence about the system and its development process. Human evaluators assess the collected evidence to ensure that the product meets the qualification criteria stipulated by regulatory agencies, making the process complex and challenging. Assurance Cases (ACs) have emerged as a promising approach to provide comprehensive and defensible arguments that a system design satisfies the safety and security requirements. To advance this approach, we aim to develop a computer-aided framework that uses hierarchical networks of assume-guarantee (A/G) contracts to model ACs. Our framework use uncertainty quantification and logic reasoning to validate and assess the confidence of ACs..

Publications:

1. Z. Daw, C. Oh, M. Low, T. Wang, I. Amundson, A. Pinto, M. Chiodo, G. Wang, S. Hasan, R. Melville, and P. Nuzzo, “AACE: Automated assurance case environment for aerospace certification,” in 42nd AIAA/IEEE Digital Avionics Systems Conference, Oct. 2023. (Best of Session Award)

2. Z. Daw, T. Wang, C. Oh, M. Low, I. Amundson, G. Wang, R. Melville, and P. Nuzzo, “Computer-aided evaluation for argument-based certification,” in 42nd AIAA/IEEE Digital Avionics Systems Conference, Oct. 2023. (Best of Session Award)

3. T. E. Wang, C. Oh, M. Low, I. Amundson, Z. Daw, A. Pinto, M. L. Chiodo, G. Wang, S. Hasan, R. Melville, and P. Nuzzo, “Computer-Aided Generation of Assurance Cases,” in the 10th International Workshop on Next Generation of System Assurance Approaches for Critical Systems (SASSUR), Sep. 2023.

4. C. Oh, N. Naik, Z. Daw, T. E. Wang, and P. Nuzzo, “ARACHNE: Automated validation of assurance cases with stochastic contract networks,” in the 41st International Conference on Computer Safety, Reliability and Security (SAFECOMP), Sep. 2022.

Optimal Routing in Wireless Communication Networks with Uncertainty