Abstract:

An automatic synthesis problem is often characterized by an overall goal or specification to be satisfied, the set of all possible outcomes, called the design space, and an algorithm for the automatic selection of one or more members from the design space that are provably guaranteed to satisfy the overall specification. A key challenge in automatic synthesis is the complexity of the design space. 

In the first half of the talk, we introduce a formal model, termed hierarchical contract nets (HCN),  and a framework for the efficient automatic synthesis of hierarchical contract nets, based on a library of conditional refinement relations between contracts and contract nets. Assurance cases (ACs) have gained attention in the aerospace, medical, and other heavily-regulated industries as a means for providing structured arguments on why a product, typically a complex cyber-physical system,  is dependable (i.e., safe, secure, etc.) for its intended application. Challenges in AC construction stem from the complexity, uniqueness and the heterogeneous nature of the CPS and the supporting evidence, and the need to assess the quality of the argument and evidence.

In the second half of the talk, we present an application of HCN in the DARPA program Automatic Rapid Certification of Software (ARCOS) for an automated AC creation framework that facilitates the synthesis, validation, and confidence assessment of ACs based on dependability argument patterns and confidence patterns capturing domain knowledge.

Speaker Bio:

Dr. Timothy E. Wang is currently at RTX Technologies Research Center (formerly Raytheon/United Technologies Research Center). He earned his B.S., M.S., and PhD all from the Department of Aerospace Engineering at Georgia Institute of Technology.   He has been working on various aspects of the modeling, analysis, verification, and validation (V&V) and certification of complex cyber-physical systems.  This includes application of formal methods to industrial systems such as Pratt & Whitney engine FADEC, compositional modeling and formal verification of human-machine systems, formal verification of on-board helicopter autonomy, and also machine learning with formal robustness guarantees.  He has participated and led several government-sponsored research programs from DARPA, ONR and NASA.