航天航空,医疗机构,汽车电力,化工工厂,银行金融等领域都离不开实时系统的运作,并且这些系统大多为安全攸关系统,它们需要经过严格的建模、分析和验证才能保证系统的正常工作。对嵌入式实时系统来说,其会受到外界条件的影响从而发生不确定的行为,例如任务执行时间发生改变以及周期任务会产生偏移和抖动。因此对这些系统进行建模与验证时是需要考虑这些因素的。本文提出一种基于任务的对实时系统中不确定行为进行建模与验证的方法。该方法使相关人员能依据系统中对任务的规格描述直接进行建模,并能表达系统中的不确定性行为,同时也能基于这种建模方式对系统要满足的性质进行验证。该方法相比于传统的基于状态的形式化方法,其不仅能够表达系统中存在的不确定行为并且在验证时也不被物理时钟局限,同时也在一定程度上减少了使用者对系统进行建模与验证的学习成本与使用难度。本文首先对系统的任务规格进行分析,通过任务中存在的三种不确定性时序行为对基础任务模型进行扩展从而使其能够表达不确定行为,再结合系统中任务之间的依赖关系定义系统模型。然后对系统需要满足的安全需求进行分析,并使用时钟约束描述语言来形式化表达系统中的不应该出现的行为。最后将系统模型转换为时钟约束模型并采用基于有界模型检验的方式来对系统进行安全性验证。最后使用本文提出的方法对三个嵌入式实时系统进行建模与验证,通过实验的方式证明了该方法的可行性与有效性。