近些年来,随着多核硬件以及云平台的兴起,高质量的异步程序(asynchronous programs)变得越来越重要。而在实时(real-time)系统中,异步程序仍缺乏相关的分析验证工具。经典的实时系统形式化模型,如时间自动机(timed automata),只能建模静态的并发程序(concurrent programs),其进程实例数是固定的并且运行时不允许创建新的进程实例。为了更好的支持实时异步程序的分析与验证,本文提出异步多进程时间自动机(asynchronous multi-process timed automata)模型:系统中每个进程被抽象为一个进程时间自动机,与时间自动机类似只是部分状态可用于触发新的进程实例;扩展了多重集合用于缓存运行时创建的新进程实例;触发进程实例不会被阻塞,与被触发进程实例异步的运行。异步多进程时间自动机模型的表达能力十分强大,足以建模许多复杂的实时异步程序(real-time asynchronous programs)。通过研究模型的可覆盖性问题(coverability problem),可验证实时异步程序的许多安全性性质。本文我们主要研究异步多进程时间自动机的形式化语义,可覆盖性问题可判定性以及可覆盖性问题算法:·设计了异步多进程时间自动机的形式化语义:连续变迁,对应系统整体的时延;激活变迁,对应开始运行缓存集合中的进程实例;动作变迁,对应一个进程实例的一步内部动作;触发变迁,与动作变迁类似,只是额外触发新的进程实例并置入缓存集合中;结束变迁,对应一个进程实例的结束。语义的表达能力足够建模许多有用的实时异步程序同时保证了可覆盖性问题可判定,并且语义在保持自身简洁的同时能容易的描述复杂的实时异步程序。·系统的许多安全性性质可以归约到可覆盖性问题,研究异步多进程时间自动机的可覆盖性问题可判定性,一方面是为了保证模型的安全性可被形式化验证,一方面可以在模型可覆盖性问题不可判定时重新调整模型的语义。直接证明模型的可覆盖性问题的可判定性是困难的,本文通过将异步多进程时间自动机归约到可读边时间Petri网(read-arc timed petri nets),证明了模型的可覆盖性问题可判定。归约过程中部分语义无法编码,通过限制语义使得归约可行。·设计异步多进程时间自动机的可覆盖性问题算法难点在于系统的格局是无穷多的。本文借鉴时间自动机可达性算法中用到的区段数据结构,并基于其扩展版本存在区段数据结构,不断的计算其Pre集合最终达到不动点集合Z,将可覆盖性问题转化为初始格局是否在Z存在区段集合所描述的所有格局之中。