论文部分内容阅读
该文针对嵌入式实时软件系统的需求规约和验证问题,提出了系统建模语言RTRSM,并以该语言为基础,展开全文,包括模型性质描述语言RITL的提出和相关规约验证问题的研究.需求属于问题空间,因此其研究应面向特定应用领域.针对ERS的特点,我们基于离散时间域,选取有穷状态机作为系统模型,在继承了已有层次、并发状态机的研究在果之上,加强了时间限制的描述,提出了以扩充的层次有穷状态机HCA为核心,以模板为基本组成单元,以规则作为状态图的内部形式化表示的可执行的需求描述语言RTRSM.该语言图形化,易于理解和使用,且具有形式语义.文章通过两种方式定义了RTRSM的语义,包括执行步语义和合成的结构化语义.其形式语义是进行有效规约验证的基本前提.该文提出了基于离散时间域的线性命题时序逻辑RITL,以描述RTRSM模型所应满足的性质,从而弥补其过于细化而不能描述整体性质的不足.RITL以时间状态序列为语义模型,具有基于区间和时间点的量化时间属性的描述功能,能较为自然和全面地描述RTRSM模型的性质.该文在需求归约验证方面所做的工作包括两个方面:首先对RTRSM规约的一致性和完备性及其检查方法进行讨论,然后根据RTRSM语义,给出了可达图的构造算法,以及RTRSM和RITL的PVS语义编码.可达图不仅为模型检查提供了所需要的穷尽的状态空间,还可用于规约的一致性和完备性检查.通过语义编码,将RTRSM和RITL嵌入较为成功的通用证明框架PVS,从而可利用该工具对RTRSM规约进行验证.以上工作不仅是RTRSM和RITL语义的使用,也是对它们的检验.RTRSM的可执行性很好地支持了规约的原型化验证.我们所开发的面向嵌入式实时软件系统的需求工程环境SREE具有RTRSM规约的编辑和文档生成,以及部分验证功能,尤其是提供了用户输入和动画演示两种模型执行方式,以实现规约的原型化验证.文末总结全文并提出了下一步工作.