随着多核处理器的发展，对并发程序的研究已成为程序设计的热点。然而，并发程序的交错执行存在不确定性，这导致了传统的测试、仿真、演绎推理技术很难发现程序中隐匿的错误和漏洞。模型检测是一种通过穷尽搜索的自动化验证技术，作为传统验证方法的一种补充，已成为保证程序安全和可靠的重要手段。可达性分析是一种常用的程序验证技术，通过分析程序某一状态是否可达，从而查找程序中的漏洞或错误。　　基于共享内存进行异步通信是并发程序中常用的通信方式之一，然而现有模型对该类程序进行建模时，其可达性是不可判定的，基于k-限界技术可使其为可判定。本文结合k-限界技术，对基于共享内存进行异步通信的并发程序的可达性进行研究。主要工作如下：　　针对含有递归、动态线程创建的并发系统的可达性分析问题，提出动态下推网络模型DPN，采用k-限界技术算法实现可达性分析。由于该算法存在状态空间爆炸问题，对模型中下推系统进行符号化，缩减状态空间，避免穷尽搜索每一条路径，以便节省大量计算时间。　　针对含有递归、动态线程创建的实时并发系统，提出了时间动态下推网络对其进行建模。首先在动态下推网络中引入描述连续时间的全局时钟，以及能描述与时间相关的全局变量和栈字符“年龄”的实数时钟。然后给出一种基于时钟关键点的优化技术来缩减时钟区间，缓解转换后的状态空间爆炸问题，为了进一步缩减状态空间，采用仅关注栈顶的动态转换方法，将连续的时间动态下推网络转换成时间域表示的动态下推网络，同时给出转换的等价算法，并且证明状态p在时间动态下推网络中可达当且仅当其转换状态p在动态下推网络中可达。最后通过实例，详细阐述整个转换过程。