随着嵌入式控制软件的软件规模与复杂度的不断上升,考虑到嵌入式软件对于安全性、实时性、可靠性等非功能属性的要求,传统的软件开发方法,以代码为核心的开发方法面临着越来越多的困难,基于模型的软件开发方法成为了嵌入式软件开发领域的主要方式。这其中,考虑到嵌入式软件的对非功能性属性的要求,就必须要有一种有效的方式能够对模型进行分析与验证,以此提高软件系统的安全性与可靠性。本文就是在这样的背景下,在SmartC建模语言的基础上,为实时嵌入式软件一体化设计开发与验证语言(RTESIDDVL)这个描述能力更强大的建模语言提出了行为模型的定义,并给出了 RTESIDDVL行为模型到时间自动机模型的转换方法,并对时间自动机模型的验证进行了分析。所以本文的工作主要如下:(1)为RTESIDDVL建模语言提出了行为模型的定义。在分析了行为模型的概念特点,以及与结构模型的关系之后,给出了行为模型的语法定义,包括了行为模型的各个组成部分,以及各个组成部分的图形与文本两种方式的表达。(2)提出了 RTESIDDVL行为模型到时间自动机模型的转换方法。模型验证对于基于模型的开发方法来说必不可少,相比于其他提高软件可靠性的方式,如测试、定理证明等具有各种不可替代的优势,所以本文定义了由行为模型到时间自动机模型转换的规则,包括了各个元素之间的转换,以及转换流程。然后对行为模型转换之后的时间自动机模型的验证给出了分析。(3)最后本文给出了一个模型转换工具的实现。通过使用Lex与Yacc这两个工具,经过对RTESIDDVL行为模型的分析,设计了行为模型的词法与语法文件,并根据转换规则对词法与语法的规则动作进行了设计。最终通过这两个工具实现了一个RTESIDDVL行为模型到UPPAAL时间自动机模板的转换工具。