Speaker:Gokul Hariharan

Formal Specifications for Cyber-Physical Systems

Formal methods are used extensively in software and hardware verification, quantum system verification, ensuring autonomous vehicle safety, and protecting security-critical software from threats. However, the validity of formal methods critically depends on the correctness of specifications. This thesis contributes to (a) developing a new specification language, Mission-time Linear Temporal Logic Multi-type (MLTLM), to ease writing and verifying specifications that involve multiple types, e.g., different time scales, (b) solving for the satisfiability and maximum satisfiability of two popular specification languages, MLTL and LTL, to aid specification debugging and optimally design systems that are safe by construction. 

Part 1 will introduce MLTLM as a specification language, provide theoretical comparisons to its single-type counterpart, MLTL, and present optimal translations from MLTLM to MLTL.  Comparisons between the optimal MLTL translations and MLTLM specifications on native MLTL and MLTLM runtime verification monitors suggest that the latter results in substantially lower hardware resource usage and verification times.

Part 2 explores solving the maximum satisfiability (MaxSAT) of MLTL specifications. Given a set of specifications, MaxSAT solves for the subset of the largest cardinality that is simultaneously satisfiable. MaxSAT is important for feature prioritization and cost analysis while designing systems that are safe by construction. We develop a new algorithm that does fast translations to Boolean logic, and use off-the-shelf Boolean MaxSAT solvers to solve the MLTL MaxSAT problem. Results show that MLTL satisfiability checking is faster using the Boolean translations of this work compared to other recent approaches.

Part 3 provides a solution to the MaxSAT of LTL specifications. Whereas MLTL specifications have equivalent Boolean logic formulas, such translations are unavailable for LTL. Hence, we approach the problem using core-based techniques. We modify an existing algorithm to extract the unsatisfiable core from a set of LTL formulas and use the unsatisfiable core with a Boolean MaxSAT algorithm to solve for LTL MaxSAT. Compared to the original algorithm, the core-extraction feature has minimal overhead ($\mathcal O(1)$). The LTL MaxSAT solver is applied to two real design instances: robot navigation and power load distribution, and on randomly generated instances.

Committee: Tichakorn Wongpiromsarn (major professor), Samik Basu, Gianfranco Ciardo, Kristin-Yvonne Rozier, and Phillip Harrison Jones