Formal specifications for cyber-physical systems
Gokul Hariharan · 2024
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. Chapter 2 introduces MLTLM as a specification language and provides many examples of system specifications that involve different types. We prove the succinctness of MLTLM and develop translations to MLTL that are minimally succinct and equivalent to MLTL. Lastly, we integrate an MLTLM runtime verification (RV) monitor into the popular R2U2 MLTL RV monitor. Comparisons between the optimal MLTL translations and MLTLM specifications on the native MLTL and MLTLM RV monitors suggest that the latter results in substantially lower hardware resource usage and verification times. Chapter 3 explores solving for 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. Chapter 4 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 then we 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.