芯之康牌红曲丹参胶囊动物毒理学安全性评价研究

目的对芯之康牌红曲丹参胶囊的服用安全性进行毒理学研究。方法按照国家标准要求和相关规定,对本品进行小鼠急性毒性实验、遗传毒理实验(含Ames实验、微核实验和小鼠精子畸形实验)和大鼠30 d喂养实验。结果以20.0 g/kg·bw剂量给小鼠灌胃后,14 d动物无中毒症状,无动物死亡;3项遗传毒性实验结果均为阴性;30 d喂养实验的结果与阴性对照组相比无显著差异(P0.05)。结论本品在本实验范围内无急性毒性、无遗传毒性,产品安全,可以作为辅助降血脂类保健食品用于人体。     

基于XYZ/SE的软件部分正确性验证

针对软件形式化描述和正确性验证研究中存在的问题,提出了基于XYZ/SE的统一框架研究该问题。在该框架下,基于逐步求精思路对软件进行抽象;对软件整体进行形式化描述和部分正确性验证;对抽象得到的软件各部分进行形式化描述和部分正确性验证;进行调整和验证,即：如果推导结果与预期不一致,则需要重写相关程序或者回溯检查推导过程是否存在错误,直至程序部分正确性得到验证为止。以国库信息处理系统为对象,分析了基于XYZ/SE的统一框架性能。分析表明,基于该框架能够对软件的不同抽象层次进行规范描述,实现从抽象（静态语义）到具体（动态语义）的平滑过渡。同时,基于XYZ/SE的统一框架也可以表示Hoare逻辑推演规则。     

UML活动图的时序逻辑语义

UML活动图可以表示不同抽象级的控制流,很适合用于对系统的行为建模．但是缺乏精确的语义使得难以对它所表示的系统行为进行分析．XYZ／E是一可执行线性时序逻辑语言,既可描述系统的动态行为又可表示程序性质,用它对活动图形式化后,就可在统一的逻辑框架下分析活动图的性质．定义了一个有向图结构用以表示UML活动图,再给出其XYZ／E语义,并用一个例子说明活动图到XYZ／E的语义转换,为进一步的分析提供形式化基础．     

色彩空间转换的理论和实证研究综述

首先介绍了一些主流的色彩空间,对色彩空间转换流程进行了介绍,随后对国内外关于各种主流色彩空间的转换的研究文献进行了综述,最后给出了未来色彩空间转换研究的发展方向。     

基于UML和XYZ/E的ATM系统体系结构描述

本文提出了将可视化建模语言UML和时序逻辑语言XYZ/E相结合来描述软件体系结构的方法。首先给出了该方法的基本框架,然后对XYZ/E进行扩展,使之能够显式地表示软件体系结构的基本元素,并定义了UML活动图的形式语义,最后,通过银行ATM实例进一步说明了该方法的可行性,对可视化和形式化相结合描述软件体系结构的研究具有一定的推动作用。     

基于XYZ/E的混成系统

混成系统是由计算机和物理设备组成的嵌入式实时计算系统.它允许在交互式实时系统中引入连续变化的单元.XYZ/E 是基于Manna-Pnueli的线性时序逻辑的程序设计语言.它将程序的动态语义与静态语义统一在同一框架中,支持从抽象的程序规范到可执行代码的逐步求精的全过程.该文使用XYZ/E语言描述和验证混成系统.首先介绍了计算模型,然后介绍了XYZ语言对混成系统的形式化描述,最后介绍了混成系统的验证.与同类工作相比,XYZ/E支持状态转换,从而可以方便地描述复杂的控制算法.     

三机冗余容错系统的描述和验证

使用XYZ/E描述和验证三机冗余容错系统.考虑每台计算机加载了一个不断向外界环境输出数据的确定性顺序程序P,用XYZ/E程序SingleProcessor_P刻画程序P在单机上运行,用时序逻辑式Spec_P刻画P向外部环境输出的数据所满足的性质.最后证明,采用三机冗余模式所得到的程序TripleProcessors_P即使在出现硬件错误的情况下运行,也能满足性质Spec_P.     

基于XYZ/ADL的Web服务组合形式化描述

组合现有的Web服务是为了能快速地开发复杂的Web服务。介绍了几种常见的Web服务组合方法，并根据4种关键需求（连通性、非功能服务质量属性、正确性、可伸缩性）对它们加以比较。提出了一种基于软件体系结构描述语言XYZ／ADL的Web服务组合形式化描述方法，由XYZ／ADL定义描述Web服务的组件、组件之间交互的连接件以及建立组件和连接件实例联系的配置．最后结合一个实例描述Web服务组合的工作方式。     

使用时序逻辑检测软件需求阶段的特征干扰

针对需求阶段的特征干扰问题，提出了使用时序逻辑语言XYZ／E检测特征干扰的方法。最后给出了一个简单的升降机系统的实例。