-
题名LTL概率模型检验工具的实现与优化
- 1
-
-
作者
林哲超
董威
-
机构
国防科学技术大学计算机学院
-
出处
《计算机工程与科学》
CSCD
北大核心
2017年第5期892-896,共5页
-
文摘
概率模型检验建立在非概率模型检验技术的基础上,不仅能够对系统进行定性的验证,还能够定量判断系统满足相关性质的概率,具有广泛的适用性。LTL概率模型检验算法的复杂度较高,达到双重指数级别,现有的工具如PRISM与MRMC均不支持对LTL性质的验证。针对这个问题,通过对原有的LTL概率模型检验算法进行优化,实现了一个高效的LTL概率模型检验工具。通过对比实验验证了该工具的有效性。
-
关键词
LTL
概率模型检验
优化
-
Keywords
LTL
probabilistic model checking
optimization
-
分类号
TP311.5
[自动化与计算机技术—计算机软件与理论]
-
-
题名基于动态二进制翻译和插桩的函数调用跟踪
被引量:3
- 2
-
-
作者
卢帅兵
张明
林哲超
李虎
况晓辉
赵刚
-
机构
信息系统安全技术国家重点实验室(军事科学院)
-
出处
《计算机研究与发展》
EI
CSCD
北大核心
2019年第2期421-430,共10页
-
文摘
动态函数调用跟踪技术是调试Linux内核的重要手段.针对现有动态跟踪工具存在支持平台有限、运行效率低的问题,基于二进制翻译,设计并实现支持多种指令集的动态函数调用跟踪工具.首先,使用二进制翻译进行系统加载、分析内核镜像,识别基本块的分支指令类型.然后,根据不同平台指令集,设计桩代码并在函数调用与返回指令翻译时插入桩指令,进而在程序执行和内核启动时实时获取时间戳、进程标识、线程标识、函数地址等信息.最后,内核加载完毕后,处理获取的信息,生成过程函数调用图.只需要根据平台指令集特点设计对应的信息获取桩代码并插入到函数调用指令翻译代码中,实现简单,易于移植支持多种平台.该方法基于二进制翻译,直接对程序或内核镜像中的指令段、代码段、符号表进行分析,不依赖源码.拓展的中间代码和额外的目标码,不影响基本块连接、冗余代码消除、热路径分析等二进制翻译的优化方法,降低了开销.基于QEMU的实验结果表明:跟踪分析结果与源代码行为一致,桩代码执行信息记录产生了15.24%的时间开销,而信息处理并输出到磁盘文件产生了165.59%的时间开销,与现有工具相比,性能有较大提升.
-
关键词
动态二进制翻译
代码插桩
函数调用跟踪
Linux内核分析
跨平台
-
Keywords
dynamic binary translation
instrumentation code
function call tracing
Linux kernel analysis
cross platform
-
分类号
TP391
[自动化与计算机技术—计算机应用技术]
-
-
题名基于睾丸微石症探讨男性不育肾藏精理论“藏”字新知
- 3
-
-
作者
林哲超
李海松
王继升
-
机构
北京中医药大学第一临床医学院
-
出处
《中国男科学杂志》
CAS
2024年第2期134-137,共4页
-
基金
北京市自然科学基金青年项目(7244488)。
-
文摘
多年来,广大学者对于中医肾藏精理论在男性不育症中的研究颇多,然大多只注重“精”,而忽视“藏”,笔者认为“藏”有两重含义,即蛰藏太过和封藏不及,其中瘀血阻络病机对于“藏”的影响重大。男性不育症往往与男性精液质量有关,然西医病因多不明确,笔者从肾藏精理论中“藏”的角度出发,结合现代多种男科疾病的发病机理以及中医瘀血阻络病机,以睾丸微石症为切入点,以期从新的角度解释男性不育症的发生,提供男性不育症治疗的新思路。
-
关键词
不育
男性
睾丸微石症
肾藏精
瘀血阻络
-
Keywords
infertility,male
testicular microlithiasis
kidney storing essence
blood stasis blocking collaterals
-
分类号
R698.2
[医药卫生—泌尿科学]
R697.22
[医药卫生—泌尿科学]
R22
[医药卫生—中医基础理论]
-