ITR: Automated Verification of Asynchronous Software Systems

这项研究致力于开发和实现新的顺序和并行算法，用于验证异步软件系统，如通信协议和分布式或嵌入式软件。现有的基于状态空间探索的自动化技术，特别是基于二叉决策图(BDDS)的符号模型检测，侧重于验证硬件和软件的同步。虽然符号模型检查在原则上也可以应用于异步软件系统，但这带来了新的挑战，这些挑战在文献中没有或只是没有得到充分的解决。最重要的是，除了内存受限的问题外，异步软件固有的复杂性使得状态空间探索成为一个时间受限的问题。这项研究通过开发使用多值决策图(MDDS)和布尔Kronecker算子来分别对状态集和转换集进行编码的算法来解决这两个基本限制，这与传统上用于这两个目的的BDDS形成了对比。这为利用异步软件固有的事件局部性属性铺平了道路，从而极大地提高了顺序算法的效率并实现了它们的高效并行化。

Abstract0219745Ciardo -College of William and MaryThis research is devoted to the development and implementation of novel sequential and parallel algorithms for the verification of asynchronous software systems, such as communication protocols and distributed or embedded software. Existing automated techniques based on state-space exploration, in particular symbolic model checking based on Binary Decision Diagrams (BDDs), focus on verifying synchronous hardware and software. Although symbolic model checking may in principle be applied to asynchronous software systems as well, this poses new challenges that are not, or only insufficiently addressed in the literature. Most importantly, the inherent complexity of asynchronous software makes state-space exploration a time-bound problem, in addition to a memory-bound problem. The research addresses these two fundamental limitations by developing algorithms that employ Multi-valued Decision Diagrams (MDDs) and Boolean Kronecker Operators to encode sets of states and transitions, respectively, in contrast to BDDs traditionally used for both purposes. This paves the way for exploiting the property of event locality that is inherent in asynchronous software and, thereby, for greatly improving the efficiency of sequential algorithms and enabling their efficient parallelization.