【摘 要】
：
在模型驱动软件开发过程中,基于模型的测试方法往往用于检验软件代码针对软件模型的一致性以确保软件质量.然而,随着当今软件系统规模的不断增大,相应的软件开发过程也变得越
【机 构】
：
华东师范大学计算机科学技术系,上海200241
【出 处】
：
2016年上海市研究生学术论坛——电子科学与技术
论文部分内容阅读
在模型驱动软件开发过程中,基于模型的测试方法往往用于检验软件代码针对软件模型的一致性以确保软件质量.然而,随着当今软件系统规模的不断增大,相应的软件开发过程也变得越来越灵活,代码有时会先于模型被修改,更忠实地体现系统功能和实现机制.传统的基于模型的测试方法只能检测代码之于模型的一致性而不能反作用于模型层面,模型的修改者只能人为地评估修改的正确性,大大降低了效率并增加了系统的潜在隐患.为此,本文对传统基于模型的测试方法的一致性检验进行了扩展,实现了持续验证系统Eunomia,通过从实现系统中抽取表达模型与代码的不一致的性质来自动定位模型中与实际运行系统不匹配的属性,并将其表示为可直接用于模型检测的线性时序逻辑(LTL)表达式,通过不断扩充该LTL属性表达式持续的验证模型与代码间的双向一致性.研究结果表明,Eunomia能有效查找软件模型和代码间的不一致并生成可直接检测模型的系统性质,从而实现了自动化的模型与代码间的双向一致性检测,不仅提高了一致性检测的有效性而且大大减少了人力开销.
其他文献
An H-shape dielectric resonator antenna with U-slot on the patch is proposed in this paper, the H-shape dielectric resonator is mounted on the vertical grou
针对人体参数测量的需求,研制一种基于MCU的人体参数测量系统.人体生物阻抗的测量是利用MCU产生方波激励,通过低频滤波产生50kHz正弦波恒流信号施加在电极上,通过采样测量电
随着SoC在便携产品中越来越多的应用,低功耗技术变得越来越重要.针对SoC系统的低功耗需求,本文采用华润上华0.18um CMOS工艺在Aether全定制集成电路设计环境下完成了一种低功
传统的验证方法通常是对设计打入相应的激励,并观察输出波形是否满足预期,这样的验证方法可观察性低,并且不能保证验证的完备性.本论文主要研究基于OVL的断言验证,将断言技术
随着无线通信技术的发展,宽带应用场景越来越多,并且信号的形式也从单频段向多频段发展.传统数字预失真方法受限于系统设计成本及AD采样速率,若应用到宽带无线通信中将会遇到
In this paper, a time amplifier is proposed to improve the resolution of TDC.Basing on the traditional current-steering charge pump, the time amplifier can
模数转换器是连接模拟世界与数字世界的桥梁.连续时间模数转换器对量化噪声的抑制有着重要作用,本文对连续时间模数转换器的建模进行了研究,运用Matlab对整个系统进行了建模,
本文设计一款兼容CAN2.0B协议的CAN控制器软核IP.该软核同时支持CAN协议中的标准帧和扩展帧,具有四种工作模式,总线时序参数可配置,64字节的接收FIFO,同时集成了常见总线接口
本文设计了一种输出动态范围可调的二阶Sigma-Delta调制器.首先针对Sigma-Delta ADC在实现高精度的同时如何降低系统功耗这一问题,进行了详细的建模分析并得出满足精度需求的
随着软件定义无线电(SDR)的发展,人们对接收机的线性度要求越来越高,而作为接收通路的第一级,低噪声放大器(LNA)的线性度要求也越来越高.在分析电路系统的非线性时,Volterra