基于疲劳强度分布的复合材料疲劳验证载荷放大系数

传统的载荷放大系数(LFE)法是在复合材料静强度和疲劳寿命的Weibull分布基础上推导得出的。为了保证复合材料疲劳试验验证的可靠性和疲劳载荷放大系数的分散性较小,利用疲劳可靠性理论,提出一种基于复合材料疲劳强度和疲劳寿命Weibull分布的载荷系数法——疲劳强度载荷放大系数(FLEF)法。将LEF和FLEF方法应用于疲劳试验数据分析,结果表明:在无批量数据的前提下,采用LEF法获得的疲劳载荷放大系数无法保证复合材料疲劳试验验证的可靠性,FLEF法确定的载荷系数具有更小的分散性,更高的可靠性。可见,与LEF法相比,FLEF法在理论和实践上更适合复合材料疲劳试验载荷放大系数的确定。     

基于MVC的GNSS验证系统授时指标软件设计与实现

为了方便分析GNSS验证系统授时指标,设计并实现了授时指标软件。该软件具有数据解析、授时载波频率准确性分析、载波频率稳定性分析、码载一致性分析、数据拟合、频域分析等功能。采用MVC(model-view-controller)模式对软件的系统架构进行设计,描述了Qt的信号与槽机制和核心模块的设计及其交互,并用C++语言在Qt平台完成了软件的开发。实验表明,该软件可方便地实现GNSS验证系统授时指标的定量分析,GNSS验证系统频率准确度为10~(-10)、码载一致性为10~(-10)。     

玉米高产产量形成特征及其验证

 分析中国玉米高产田(≧15000kg/hm²)的典型特征、内在规律,提出产量突破的途径与关键技术,并进行高产验证。结果表明,35°N～44°N可作为中国玉米高产带。收获穗数是产量构成因素中影响和决定产量的首要因素,按80%置信限计算,在目前生产水平下,产量实现15000kg/hm²的理想结构模式为:种植密度70755～101250株/hm²,穗数7.01×10⁴～10.09×10⁴穗/hm²,穗粒数453～642粒,千粒重323.0～414.9g,单穗粒重162.5～236.2g;高产田单株生产力以穗粒重200g左右的中穗型为主。选择耐密植、中晚熟品种,增密种植,保障水肥供应,精细管理,适时晚收,创建一个高质量群体,增加花后物质生产量和转移率,充分挖掘当地光热资源是当前中国玉米高产突破的主要途径。     

非线性方程组重根的可信验证方法

利用区间算法及边界矩阵理论, 研究非线性方程组重根的可信性验证方法. 提出一种可信验证算法, 该算法输出一个近似解及其相应的误差界, 使得在近似解的误差界范围内必存在一个精确解.     

充气钻井环空弹状流稳态流动模型与实例验证

国内外针对弹状流(段塞流)管流的力学模型研究很少,且计算误差较大,无法应用于钻井工程。为此,针对充气钻井开展环空气液弹状流稳态力学模型研究,可准确预测和设计井筒流体参数。首先,借鉴国外研究成果,对钻井气液两相管流型态进行描述分析,推导出环空弹状流与泡状流的转换判别关系式,认为环空充气钻井液主要出现泡状流和弹状流两种流型,且充气钻井井深小于300 m的环空内为弹状流。然后,建立环空弹状流单元的物理模型,并对其流动参数进行解析计算。依据管流机械能守恒定律,建立充气钻井环空弹状流稳态力学模型,并给出数值解法。通过两井连通充气钻水平井(DNP02井)的实钻模拟,计算出的环空流动参数与现场实测数据非常吻合,误差小于5%。证实模型的理论体系完整,计算结果满足钻井工程需求,具有很好的通用性。     

利用投影时序逻辑的多内核进程调度建模与验证

针对软件测试无法满足多内核处理器上进程调度的验证需要这一问题,提出利用投影时序逻辑(PTL)的定理证明方法来验证进程调度.使用PTL公式建立了支持当前主流进程调度算法的多内核处理器进程调度一般模型S,并将系统期望的性质描述为PTL公式P,在PTL公理系统的基础上,通过证明S蕴含P是否为一个定理来验证系统是否具备该性质.以2内核处理器上的多级反馈队列算法的正确性为案例进行检验,结果表明所提方法可验证多内核处理器进程调度的系统性质,保证多内核进程调度的可靠性.由于多内核处理器的进程调度具备了并发系统的主要特点,因此该方法也适用于一般的并发系统验证.     

面向命题投影时序逻辑的安全协议模型检测

针对无条件安全通信协议,特别是Russian Cards协议的安全性验证问题,提出基于命题投影时序逻辑(PPTL)的模型检测方法.根据协议构造规则建立了Russian Cards协议的ProMeLa模型;利用chop算子将多个交互事件进行顺序复合,以表达协议所期望的通信序列;由projection算子定义了协议在该序列上的安全性质,再将该性质转为Never Claim语法结构并连同协议模型作为模型检测器SPIN的输入,以完成验证工作.验证结果表明,由协议规则构造的Russian Cards通信协议是安全可靠的,该方法也适用于一般的无条件安全通信协议的验证.     

非否认协议公平性分析的扩展串空间方法

针对在非否认协议公平性的形式化分析中,如何弱化初始假定和避免状态空间爆炸等问题,提出了扩展串空间方法.通过将签名运算引入串空间理论,从而对串空间理论的项集合进行重新定义,进一步通过对子项关系、攻击者迹和自由加密假定的扩展,并结合丛概念,构成了扩展串空间.分析非否认协议的公平性,首先将协议行为归纳为攻击者串、发送者串、接收者串和可信第3方串,以此构造协议的扩展串空间模型,然后结合协议迹和定理证明验证丛中存在发送者串等价于丛中存在接收者串,从而证明非否认协议公平性.通过扩展串空间方法对Zhou-Gollmann协议公平性的分析,得到了与Kailar逻辑和Lanotte自动验证方法相同的结果.与Kailar逻辑相比,扩展串空间方法仅使用自由加密假定,弱化了初始假定;与Lanotte自动验证方法相比,扩展串空间方法无需使用状态空间搜索,避免了状态空间爆炸问题.     

FDA的高压灭菌器验证方法的讨论

文章对高压灭菌器在FDA认证中的验证方法进行了讨论,具体提出了验证方法和验证要求,并提出具体验证报告的编写过程。     

实时系统形式化描述和自动验证

实时系统是一种带有时间约束的计算机系统,这些系统许多动作的完成是与时间相关的,即要满足一定的时间限制,它需要在特定的时间范围内的对某些输入及时做出反应。例如,碰撞中汽车的安全气囊须在300毫秒膨胀开。它的许多嵌入式应用,都有一个共同的特点就是对实时性、安全性要求很高,都需要实时的形式化规范技术。