基于经典逻辑的安全协议模型检测方法

本文分别以安全协议模型检测器SATMC和ProVerif为例,介绍了基于经典逻辑的安全协议模型检测两种方法:SAT方法和归结方法,并简要地给出了我们设计实现的基于SAT方法的安全协议模型检测器JLU-PV.     

基于着色时间Petri网的实时系统的形式验证

嵌入式实时系统多数应用在安全性要求较高的场合,因此需要保证系统的正确性.复杂性不断增加的实时系统迫切需要在系统开发早期引入形式化分析技术来验证系统的期望性质.时间Petri网是有严格数学基础的图形表达工具,适合对实时系统建模;时间自动机(Timed Automata,TA)有成熟的验证工具,被广泛用于实时系统的模型检验和验证.本文提出一种基于着色时间Petri网(Colored Time Petri Net,CTPN)的实时系统的验证方法,用CTPN对带有控制流和数据流的实时系统建模,通过转换规则将CTPN模型转换成语义等价的TA模型,利用模型检验工具UPPAAL验证系统的性质.最后,用实例证明此方法有效.     

多水平模型的最新进展

多水平模型 ( Multilevel Models)又称随机效应模型( Random Effect Models) ,它是在二十世纪八十年代 ,由英美教育统计学家基于方差成分分析而提出的统计模型 ,用于研究具有层次结构或嵌套式结构的数据 ,如分层抽样或整群抽样的数据。设个人处于家庭中 ,家庭处于社区中 ,这就构成三个水平 :个人是基本水平 (水平 1) ,家庭是中间水平 (水平 2 ) ,社区则是最高水平 (水平 3 )。多水平模型方法指出 ,数据可以而且应该同时在所有的水平上收集和分析 ,这可避免聚合带来的缺陷 [1 ]。以往通常忽略层次或对高单位设立哑变量 ,这会损失数据所包含…     

基于模型误差的交互式多模型算法

本文考虑了模型与真实模式之间可能存在的差异,分析了由此引发的问题.提出一种基于模型误差的交互式多模型算法,其中模型集合使用最小距离设计方法设计.Monte-Carlo仿真实验表明,新方法比IMM能更好地避免性能恶化,并且当真实模式保持不变时,从全局角度考虑新算法比IMM优越.     

一种改进的ARP协议欺骗检测方法

ARP协议欺骗作为一种交换式局域网中获取数据信息的方法,当用作攻击手段时,给网络安全带来了严重威.胁.本文通过分析ARP协议的漏洞及ARP欺骗的原理,设计并实现了一种基于P地址和物理地址标准对应库的ARP欺骗检测方法,达到了及时有效地检测出网络中存在的ARP欺骗报文的目的,实测表明效果良好,具有实用价值.     

基于多Agent协同的快速入侵检测系统

在多Agent协同入侵检测系统中,不同检测Agent并行地检测网络包中不同的入侵特征,以提高系统的检测效率.使用消息、自定义通信协议等作为系统的协同通信机制,有效地避免了系统中的单点故障,并且,该机制使得各个Agent的检测结果可以有效融合.在分析了入侵的类型、特征后,使用4个检测Agent仿真了入侵检测的过程,并在检测精度、检测误差影响很小的情况下,使检测每条记录的时间大幅度减少.     

基于行为改变轮理论的毒品成瘾防复吸戒治模型构建

复吸行为是禁戒毒工作的一个关键性问题。对戒毒人员开展防复吸戒治,降低其复吸风险,对于促进社会安定和公共卫生安全具有重要的意义。但是,降低戒毒后的复吸是一个复杂的系统性工程,需要进行生理-心理-家庭-社会等多层面的康复治疗干预。行为改变轮理论(Behaviour Change Wheel, BCW),被广泛应用于临床康复训练领域,取得了较好的效果。这一理论综合了个人、环境与社会政策等多方面的因素来改变和影响某一行为问题,与复吸行为的综合戒治要求具有高度一致性,能较好地应用到戒毒人员复吸行为的康复训练之中。本研究基于行为改变轮理论的原理和操作技术,探索构建甲基苯丙胺戒毒人员防复吸戒治模型,对毒品成瘾的防复吸戒治提出新的思考和戒治模式,可为禁戒毒实务部门提供一种新的工作借鉴。     

基于尿药参数的血药浓度检测模型

目的:为血药浓度的检测提供一条简便、无创、相关性高的途径。方法:在经典的药代动力学模型基础上进行扩展,提出血药浓度与尿药参数之间的函数关系式,并给出不同服药模式下血药浓度的测定方法。然后,对该模型的相关性及稳定性进行验证:首先取得一组测定的关于人体片剂服药模式的在不同时间下药物(氨基)导眠能的血药浓度与尿药参数的对应值,将(氨基)导虑能的药代动力学参数、测定的尿药参数及时间代入理论模型算出理论血药浓度值,并与实际测得的血药数据进行相关性对照;然后同理对一组关于人体静脉注射服药模式下相关数据均已测得的药物x进行相关性检验。结果:(氨基)导眠能的理论与实际血药浓度总体方差为10.7%,其准确性已能被临床所接受;药物x的理论与实际血药浓度总体方差为0.183%,两组数据几乎完全吻合。结论:该模型有良好的相关性,可作为独立的一种血药浓度检测手段使用。     

和与积数迷的符号化模型检测

和与积是一个著名的数迷问题.采用公告逻辑对该问题进行建模,将其Kripke模型符号化表示为多智能体有限状态程序,并在其上采用一种基于局部命题解释系统语义的知识逻辑符号化模型检测算法计算该问题的所有解.在时态逻辑模型检测器NuSMV基础上扩展实现了本文算法,然后在相同实验平台上用动态认知建模工具DEMO对该问题进行求解.实验表明,我们的算法不仅结果正确,而且在运行效率上与DEMO相比占有绝对优势.     

LINUX进程间通信的模型检测

模型检测是一种强大的自动分析验证技术.分析了LINUX进程间通信的部分源代码并进行手工形式化建模,使用有限状态自动机描述模型,继而转换成SPIN的输入语言PROMELA,对其进行模型检测,验证了系统的有界性和可终止性,并就进程间通信中容易发生的问题提出了改进方案.     

Antiviral effect of two aryl-oligopeptides, FR41565 and FR48217

Macrophages from mice pretreated with two chemically synthesized immunostimulating aryl-oligopeptides, FR41565 and FR48217, inhibited the multiplication of herpes simplex virus type 1 (HSV-1) and type 2 (HSV-2) in monkey Vero cells, and that of vesicular stomatitis virus (VSV) in murine L929 cells. In addition, the aryl-oligopeptides protected mice against a lethal HSV-1 infection. In particular, when treated with FR48217 at 6 mg/kg, all mice survived, whereas all control mice died from the HSV-1 infection.     

基于EHA的异常处理模型检验方法

本文提出在整个Java程序开发链中通过使用UML Statecharts对异常处理建模,对Statechart进行模型检验,完成代码生成.首先将Statecharts转换为EHA,然后给出其操作语义,根据操作语义映射到一个自动机.使用基于自动机理论的模型检验方法来验证基于EHA的异常处理模型是否满足某些关键性质,最后自动产生相关代码.     

Using Client's Routine Urinalysis Records From Multiple Treatment Systems to Model Five-Year Opioid Substitution Treatment Outcomes

Background: At global, national, and local level, the need for ongoing, timely and cost efficient, comprehensive drug treatment monitoring, and evaluation systems have clearly been well recognized. Objectives: To test the feasibility of linking laboratory data and client intake data and its usefulness for modeling retrospectively, for the first time, 5-year longitudinal drug treatment outcomes in an Irish opiate treatment setting. Methods: A multisite, retrospective, longitudinal cohort study was implemented to evaluate outcomes for opiate users based on 1.7 million routine urinalysis results collected from 4,518 individuals presenting for opioid substitution treatment in Ireland from January 2006 to December 2010. Results: Analysis of opiates, cocaine, benzodiazepine, and cannabis use at treatment intake, 6 months and at 1–5 year follow-ups revealed differences in urinalysis protocols; significant differences in age of first drug use between those using and not using opiates at 5 years; significant decreases in opiate use; increases in benzodiazepine use and significant increasing effects of concurrent cocaine and benzodiazepine use on the odds of using opiates. Time series analysis of weekly proportions opiate positive predicted 16% (95% confidence interval: 7%–25%) of clients would be opiate positive 5 years postinitial intake. ConclusionsImportance: Underutilized urinalysis data can be used to address the need for cost effective, efficient evidence of drug-treatment outcomes across time, place, and systems. Linking and matching the cross-sectional data across sites and times also revealed where improvements in electronic records could be made.     

A new antitumor antibiotic, FR900840. II. Structural elucidation of FR900840

The structure of FR900840, a new antitumor antibiotic produced by a strain of Streptomyces has been deduced as 1 on the basis of spectroscopic and chemical evidence and finally confirmed by synthesis from L-threonine and L-serine.     

混合多策略视图安全模型

传统的MLS策略侧重于信息机密性保护,却很少考虑完整性,也无法有效实施信道控制策略,在解决不同安全级别信息流动问题时采用的可信主体也存在安全隐患.同时,应用环境的多样性导致了安全需求的多样化,而当前的安全模型都只侧重于其中一种或几种安全需求.本文给出的混合多策略模型一MPVSM模型有机组合了BLP,Biba,DTE和RBAC等安全模型的属性和功能,消除了MLS模型的缺陷,提高了信道控制能力和权限分配的灵活度,对可信主体的权限也进行了有力的控制和约束,同时为实现多安全策略视图提供了一个框架.文中给出了MPVSM模型的描述和形式化系统,并给出了几种典型策略的配置实例.     

FR252921, a novel immunosuppressive agent isolated from Pseudomonas fluorescens no. 408813. I. Taxonomy,fermentation, isolation,physico-chemical properties and biological activities of FR252921, FR252922 and FR256523

Novel immunosuppressive agents, FR252921, FR252922 and FR256523 were isolated from the cultured broth of a bacterial strain No. 408813. The strain was identified Pseudomonas fluorescens from morphological and physiological characteristics. FR252921, FR252922 and FR256523, novel compounds containing macrolactone ring, showed immunosuppressive activity against murine splenocyte proliferation stimulated with lipopolysaccharide (LPS) or anti-CD3 mAb in vitro.