ITR: Automated Verification of Asynchronous Software Systems

ITR：异步软件系统的自动验证

• 批准号: 0219745
• 负责人: Gianfranco Ciardo
• 金额: $ 36万
• 依托单位: College of William and Mary
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-09-01 至 2005-01-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0219745&HistoricalAwards=false
• 关键词: ITR; Automated; Verification; Asynchronous; Software

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.

摘要0219745 Ciardo-威廉与玛丽学院这项研究致力于开发和实现用于验证异步软件系统（例如通信协议和分布式或嵌入式软件）的新型顺序和并行算法。 现有的基于状态空间探索的自动化技术，特别是基于二叉决策图（BDD）的符号模型检查，专注于验证同步的硬件和软件。 虽然符号模型检查原则上也可以应用于异步软件系统，但这提出了新的挑战，这些挑战在文献中没有或仅仅没有得到充分解决。 最重要的是，异步软件固有的复杂性使状态空间探索成为一个时间限制的问题，除了内存限制的问题。 该研究解决了这两个基本的限制，开发算法，采用多值决策图（MDDs）和布尔Kronecker运算符编码的状态和转换集，分别与传统上用于这两个目的的BDD。 这为利用异步软件中固有的事件局部性属性铺平了道路，从而大大提高了顺序算法的效率，并使其有效的并行化。