论文部分内容阅读
从上世纪70年代第一个单片机的诞生到现在,经过40多年的发展,嵌入式系统已经无处不在,小到移动电话、家用电器、电子娱乐设备等,大到工业制造、航空航天、环境工程等,都离不开嵌入式系统。但是,随着系统需求的不断迭代以及应用场景的不断丰富,嵌入式系统正在变得庞大而复杂。例如,近年来发展迅速的信息物理融合系统(Cyber-Physical System,CPS)就是一类典型的复杂嵌入式系统。新的发展趋势给嵌入式系统的设计与开发带来了极大的挑战,尤其是对于一些安全攸关嵌入式系统(Safety-Critical Embedded Systems)而言,如何在确保开发效率的同时,保证系统的安全可靠,成为系统研发过程中的关键。 目前,基于模型的设计方法(Model-Based Design,MBD)已经成为嵌入式系统设计的主流方法,其主要步骤为:首先,构造整个系统的模型(最好具有严格的形式语义);然后,基于模型对系统进行分析和验证;最后,从已验证的模型自动生成系统的代码描述(代码生成)。通常情况下,嵌入式系统被建模为既包含连续行为又包含离散行为的混成系统模型,其中,关于混成系统的分析和验证已存在很多有效的方法,但是,如何从已验证的模型自动生成与之保持某种一致性关系的代码,始终是一个研究热点和难点。混成系统代码生成的困难源自于:混成系统既包含连续行为又包含离散行为,甚至二者之间的交互,而计算机代码只能描述离散行为。因此,如何将混成系统中的连续行为离散化,同时保证原模型和离散化模型之间,以及离散化模型和生成代码之间的一致性,是混成系统代码生成技术的关键,也是本文的主要研究内容。 本论文的研究内容涉及一般混成系统(无延时)的代码生成和延时混成系统的代码生成两个方面,其核心均在于如何将原系统离散化为与之保持某种一致性关系的离散化系统。本文首先研究了如何定义两个混成系统之间的一致性关系,然后基于此关系,研究了两种混成系统建模语言:混成通信顺序进程(Hybrid Communicating Sequential Processes,HCSP)和延时混成通信顺序进程(Delay Hybrid Communicating Sequential Processes,dHCSP)到SystemC的代码生成问题,最后,实现了相应的工具并应用于若干实例。本文定义的一致性关系是传统近似互模拟关系的扩展,整个代码生成过程正是在保持此关系的基础上逐步实现的,同时,我们对文中出现的所有定理均进行了严格的证明,保证了生成代码与原模型在语义上的一致性。 本论文的成果和创新性贡献主要有以下几点: 一、提出了新的描述两个混成系统一致性的近似互模拟关系。因为HCSP和dHCSP中同时包含等待、通信和中断等机制,所以传统的仅考虑系统状态误差的近似互模拟关系,难以作为判断两个HCSP(dHCSP)进程一致性的标准。为此,我们定义了新的近似互模拟关系,此关系中允许系统的动作之间存在一定的误差,从而为HCSP(dHCSP)进程间的一致性判断,提供了严格的判定标准。 二、定义了HCSP和dHCSP的离散化规则,并提出了原进程与其离散化进程满足近似互模拟的条件。针对HCSP,我们同时定义了它在有界和无界时间内的离散化规则,并分别给出了这两种情况下,原HCSP进程与其离散化进程满足近似互模拟的条件;对于dHCSP,我们定义了它在有界时间内的离散化规则,同时给出了原dHCSP进程与其离散化进程满足近似互模拟的条件。 三、提出了离散化HCSP(dHCSP)到SystemC的转换方法,并证明了生成代码与原进程在语义上等价。在保证原进程和离散化进程满足近似互模拟的前提下,我们进一步定义了从离散化HCSP(dHCSP)进程到SystcmC代码的生成函数,并且证明了离散化进程和生成代码在语义上等价,从而保证了原进程与生成代码的近似互模拟。 四、实现了HCSP(dHCSP)的代码生成工具并应用于具体实例。基于上述理论,我们实现了HCSP(dHCSP)到SystcmC的代码生成工具并应用于三个实际案例,实验结果和理论预期保持一致。