一个基于两区间八边形约束的抽象域

抽象解释静态程序分析技术用来发现运行时错误,保证程序正确性,已经被成功应用到工业界。抽象域是抽象解释理论中的一个重要方面,然而大部分已存在的数值抽象域无法表示程序的非凸性质,抽象域的这种凸性限制很多时候会影响数值分析的精度,甚至带来更多误报。基于两区间八边形约束,提出了一个新的数值抽象域,其约束形式为x±y∈[a,b]∪[c,d],其中x和y表示变量取值,a,b,c,d∈R。该抽象域的域元素是用两区间八边形约束表示,因此可以表达某类非凸性质,表达能力强于经典的八边形抽象域,并且相对于八边形抽象域,域操作的计算复杂度并没有提高太多。

躁动

铃响的那刻，苏雨痕长舒了一口气，拿起笔走出考场。“妈的，终于考完了!”他在心里暗骂道。“终于结束了。这该死的高考。”

艳阳

1 总的来说，苏雨痕非常喜欢任何艳阳高照的时候，准确地说他喜欢的是光。而太阳是最古老且最明亮的光源。所以他喜欢太阳，尤其是艳阳。

支持抽象解释的静态分析方法的形式化体系研究

在安全关键领域中,如何保证软件的安全性已经成为了一个广受关注的重要课题。静态程序分析是一类十分有效的程序自动化验证方法。基于抽象解释的静态分析技术在验证软件的非功能性安全属性上表现十分突出。可配置程序分析(Configurable Program Analysis,CPA)是一种通用静态分析方法形式化体系,旨在用一种形式化体系对静态分析的分析阶段进行建模。使用CPA对基于抽象解释的静态分析进行建模,给出如何使用CPA形式化体系描述基于抽象解释的静态分析,给出了从待分析程序到CPA形式化体系的转换规则;提供了一种在安全关键性领域中的软件正确性自动验证方法,为基于抽象解释的静态分析工具的实现提供了一种可行方案。

基于CPA的抽象解释分析方法研究

安全关键领域中,如何保证软件安全性已经成为了一个广受关注的重要课题。确保程序中没有运行时错误,对于软件安全性的保证十分重要。基于抽象解释的静态分析方法对程序语义进行抽象,是验证运行时错误最合适的形式化方法之一。可配置程序分析(configurable program analysis,CPA)是一种适合多种静态分析方法的通用分析框架。本文使用CPA对抽象解释分析方法进行建模,给出了使用基于CPA的抽象解释方法验证程序中的运行时错误的验证流程,并用实例说明该验证方法的有效性。为程序中运行时错误的自动化分析和验证提供了一种可行方案。

基于正交试验的离心泵空化性能优化设计

针对当前离心泵在使用过程中抗空化性能差的问题,在现有IH80-50-250型化工离心泵的基础上,建立以泵汽蚀余量为目标函数的优化数学模型,采用正交试验对离心泵进行优化设计。基于L_(16)(4~5)正交表,选取叶轮进口直径、叶轮出口直径、叶片进口安放角、叶片出口安放角和叶片包角5个参数制定出16组正交试验方案。使用计算流体动力学技术对16组离心泵模型进行流场模拟,采用极差分析得到各参数对优化指标的影响顺序,并获得一组最优方案。采用Pump Linx软件模拟得到原型泵与优化泵在不同工况下的泵汽蚀余量以及在额定转速下离心泵的蒸汽质量分数,对比结果表明,优化泵的泵汽蚀余量和蒸汽质量分数分别降低了28.87%和21.02%,提高了离心泵的抗空化能力,验证了正交试验方法的可行性和准确性,为离心泵的优化设计提供了参考。

用于工程制图的多线型绘图仪设计

针对工程制图中,绘图精度不高、效率低下等问题,设计一款多线型绘图仪。该绘图仪主要由机械系统和支撑结构组成,绘图装置安装在绘图尺的燕尾槽上,在绘图尺上设置有实线、虚线和点画线3种轨道,可以实现不同线型的连续绘制。绘图仪中所有部件均可拆卸和更换,以便完成不同比例的线型绘制。该绘图仪的优势是结构简单、携带方便、绘制精度高。

氧化石墨烯增强环氧树脂复合材料的制备及其力学性能研究

以天然石墨为原料,利用改进的Hummers法制备氧化石墨烯,并对其进行X-射线衍射(XRD)和傅里叶变换红外光谱(FT-IR)表征。之后利用一种新型的有机溶剂三缩水甘油基对氨基苯酚(TGPAP)作为相转移剂和表面活性剂,将氧化石墨烯(GO)从水溶液转移到环氧树脂基体中,去除水分,加入固化剂进而得到混合液,最后利用浇铸法得到复合材料。通过万能测试拉力机对复合材料的拉伸性能和弯曲性能进行测试,结果表明氧化石墨烯的加入能够有效增强复合材料的力学性能:在添加0. 1%(质量分数)的氧化石墨烯时,复合材料拉伸强度达到最大值77. 29 MPa,与不添加氧化石墨烯相比提高了26. 60%;在添加1. 0%的氧化石墨烯时,拉伸模量达到最大值2 451. 99 MPa,与纯环氧树脂相比提高了21. 69%。

基于超声波原理的一种新型多功能洗鞋机的设计

在分析市场上现有的洗鞋机结构原理的基础上,设计了一种新型多功能洗鞋机。这款洗鞋机包括桶体、波轮、超声波发生器和电机四个部分。超声波发生器位于波轮的凸台内腔上,利用紫外线灯对鞋子进行杀菌,通过超声波换能器实现水流对鞋子的撞击和清洗。清洗完毕后,由于鞋子固定放置,洗鞋机自动实现脱水处理,不会在内桶内受到太多的损伤,最大程度保护鞋子。

贵州省赫章县印制殡葬改革宣传手册提高政策知晓率

近日，贵州省毕节市赫章县2018年订制的12万册《赫章县殡葬改革法规宣传手册》全部交货验收。截至目前，全县共印制宣传手册25万份（2017年印制3万册，2018年印制12万册），确保殡葬改革宣传手册户均一册，全面提高殡葬改革政策群众知晓率。

基于PV供能的CRC车辆分流装置结构设计

为改善高峰时期道路车流量较大而引起的道路压力较大,以及车道车流量分布不均的问题。从智能化、资源利用率最大化的角度出发,以减少人员参与及能源损耗为目标,设计了一种PV供能CRC车辆分流装置。该设计将传统的道路护栏改为可移动式道路护栏。利用成熟的CRC技术,采用远程计算机控制道路护栏横向移动,来改变车道数量,缓解道路压力,结合PV技术实现能源供给问题。所设计的车辆分流装置结构简单,操作方便,降低了能源损耗,提高了能源的利用率。

基于抽象解释的迹划分技术研究

确保程序中没有运行时错误,对于软件安全性的保证十分重要。基于抽象解释的静态分析方法对程序语义进行抽象,是验证运行时错误最合适的形式化方法之一。然而抽象解释对于程序语义的抽象可能导致过近似问题,从而引发误报,降低了分析精度。因此提出了迹划分的技术,根据程序的迹对程序控制流图进行划分,对静态分析过程进行局部细化,减少了抽象解释过程中过近似引发的误报。迹划分技术以局部分析效率降低为代价换来了分析精度的提高。

自走式交通标线划线车结构设计

为进一步提高交通标线划线的工作效率,促进划线技术的规模化、规范化和智能化,本文在结合国内外现有划线技术的基础上,设计了一种自走式交通标线划线车。该划线车依靠成熟的互联网技术和自动化技术,可以在较短时间内高效完成交通标线划线任务,从而降低人力、物力成本。

基于SolidWorks三维软件的移动式侧方停车位设计

为解决汽车侧方停车过程中存在的问题,设计了一种移动式侧方停车位。其主要依靠动力系统实现承载装置上升和移动来完成车辆的侧方位停车过程。通过其结构进行研究,利用SolidWorks软件进行三维建模,采用SolidWorks motion插件进行仿真。基于其运动学和动力学仿真结果分析,得到侧方停车位使用情况下的运动学参数变化规律和受力情况,并据此设计出一款结构合理的侧方停车位。所设计的停车位结构简单,使用方便,既节约了使用者停车所需时间,又降低了车位占地面积。

以心衰为首要临床表现的干燥综合征一例

干燥综合征是一种主要累及外分泌腺体的慢性炎症性自身免疫性疾病,其特征是口腔和眼睛干燥,但以累及心脏引起严重心力衰竭表现作为首要症状的较少见。本文报道1例老年女性,以心力衰竭为首要症状起病的干燥综合征患者,在标准抗心力衰竭治疗及抗干燥综合征治疗后,其心功能明显改善,心脏大小较发病时明显缩小,预后良好。

急性心肌梗死后并发自身免疫性溶血性贫血1例

1病例资料患者,男,40岁,2018年10月1日因“持续性胸痛4h余”就诊于外院,完善心电图、肌钙蛋白等检查,行急诊冠状动脉(冠脉)造影提示冠心病(3支病变),前降支近端急性完全闭塞,右冠次全闭塞(狭窄95%~99%)(图1),明确诊断为急性心肌梗死(AMI),予以急诊经皮冠脉介入(PCI)治疗。