嵌入式周期控制系统广泛应用于汽车电子,航空电子等安全攸关的嵌入式领域.一般来说,这些控制系统都具有周期性行为,它们的共同特点是：(1)以模式为基础.一个周期控制系统由一组模式组成,系统处于一个模式表示系统处于一个特定的状态.每个模式或是包含若干子模式,或是周期性地进行控制计算.(2)面向计算.在一个模式中,周期控制系统会执行包含复杂的计算过程的控制算法.例如,在特点的模式下,一个汽车电子控制系统可以需要处理大量的即时数据,以便确定车辆的位置和姿态.(3)周期性.周期控制系统是一个反应式系统,可能会连续运行很长一段时间.每个模式的行为由其自身的周期决定.因此,大部分的计算任务都是在一个周期内完成的.如果没有发生模式切换,那么这些计算任务还将在下一个周期再次执行.在周期结束时,如果满足特定的条件,系统将从当前模式转入其它模式.尽管这类系统被广泛地应用于航天／航空,汽车电子等安全攸关的嵌入式领域,但是工业界仍然缺少一种针对这一领域的形式化建模语言.我们曾对现有的建模语言做过广泛的调研,这些语言或是较为复杂,使用门槛较高,或是过于通用,难以处理这类系统的特征.因此,我们根据领域工程师的需求,设计了SPARDL建模框架.该框架主要包括两个部分,第一部分是作为建模标记的模式图(ModeDiagram),第二部分是规范语言SPRL.模式图是以经典的状态图(Statecharts)[56]为基础,增加了支持周期控制系统建模的特殊领域需求的建模标记.模式图的核心部分是一组模式.每个模式都有特点的周期长度.不同的模式的周期可以不同.在周期结束时,如果满足一定的条件,将发生模式切换.允许模式嵌套,也允许模式-子模式之间发生切换.与其它建模语言相比,SPARDL的特色之一是模式之间的迁移条件是可以涉及历史状态的时序表达式.模式图的结构是层次化的,分为模式-控制流-模块三个层次.一个模式既可以包含若干子模式,也可以包含一个控制流.控制流是特定的控制算法,计算任务的封装.控制流的细节在控制流层面表述.允许在控制流中调用模块,模块的细节在模式层展示.为了支持模式图的形式化推理,SPARDL框架还包括基于区段演算[42]的规范语言.该语言适于描述领域工程师关心的时序性质.SPARDL模型的正确性取决于它的模式图是否满足规范.由于SPARDL模型可能涉及到复杂的非线性运算,因此,完整的验证是不可行的.为了解决这个问题,本文利用概率模型检查技术[125,126]验证SPARDL模型.试验结果表明,本文的方法学能够发现真实系统中的设计错误.本文主要有下列贡献：●提出了新的形式化建模框架SPARDL,该框架的主要目的是为嵌入式周期控制程序提供一套清晰而准确的建模机制.●通过两种方式研究了SPARDL的形式化语义,一是将SPARDL模型解释为价格时间自动机(Priced Timed Automata),二是在迁移系统上定义它的操作语义.在操作语义的基础上讨论了SPARDL的类型安全,互模拟,等价等问题.●在形式化语义的基础上,实现了SPARDL的仿真.并扩展了最初的操作语义,提出了SPARDL的概率语义.根据新的概率语义,开发了以仿真为基础的概率模型检查,用于验证SPARDL模型是否满足各种时序性质.●在真实的案例中试用了SPARDL眶架,发现了一个控制系统中的两个真实的缺陷.试用结果充分说明了SPARDL的有效性.