随着信息技术的迅猛发展,嵌入式系统作为一种灵活地专用操作系统,已经进入了人们生活的方方面面。在一些安全攸关领域中,嵌入式系统的失效可能会导致极为严重的人员伤亡及财产损失。另一方面,随着嵌入式操作系统向智能化、网络化、多媒体化发展,软件在嵌入式系统中的地位越来越高,也越来越复杂。如何针对嵌入式系统的特点,对其进行安全性验证,受到了学术界及工业界的广泛关注及深入研究。运行时验证是一种新兴的轻量级程序验证技术,它通过监控实际系统的运行状态来判断系统的执行是否满足安全需求,是传统软件验证和确认技术的有效补充。它不但可以监测到系统当中的异常行为,也可以在系统违反安全性质时,执行相关代码,对系统进行修复。因此,将运行时验证技术运用于嵌入式系统的行为验证与系统监控中,是一种有效的思路。本文结合运行时验证最新的研究成果,嵌入式系统的特点,以及我们在工程项目中遇到的问题,展开了相关研究,主要工作如下:1.规约语言体系的扩充。根据实际项目中遇到的问题,扩充现有规约语言体系,将离散时间上的MTL应用于实际项目研究,用于表达嵌入式系统中常见的周期性质和实时性质。2.针对周期性质和实时性质的监控方法。基于Discrete-Time MTL,开发周期性质和实时性质的监控框架。设计实现了从Discrete-Time MTL到自动机的两个算法,并形成工具成果。3.面向参数化时序性质的监控方法。基于路径切片技术,在面向C语言的运行时验证框架中,实现了对参数化性质进行监控的框架设计,并进行了实现。4.针对嵌入式C程序的工具扩展。结合LLVM编译框架,面向嵌入式C语言搭建运行时验证框架,并进行了工具实现。