摘要：心冲击(BCG)信号是无损监督心脏健康状态的重要依据,为了获得准确的心脏搏动特征需要从采集到的生理信号分离出心冲击信号和呼吸信号。本文设计了一个基于压电薄膜的床垫式BCG信号采集与分析系统,提出基于变分模态分解(VMD)的呼吸信号与心冲击信号分离方法。该方法根据BCG信号的统计特征设置VMD分解算法参数,使之适用于低信噪比BCG信号特征,从而实现呼吸信号的分离和心冲击信号的提取。该实验为“随机信号处理”课程实验项目,采用MATLAB工具实现BCG信号的分析与提取,既可促进学生对随机信号处理理论的掌握,也有助于提高他们解决实际随机信号处理中复杂工程问题的能力。

摘要：在一个基于霍尔逻辑和形状图逻辑的C语言自动验证器中,设计并实现了对形状图中所含易变数据结构的形状检查方法.本工作在验证器的形状系统中实现了显式形状检查与隐式形状检查,并通过引入不同的形状级别,使验证器能够根据不同的严格程度及时发现程序中不符合形状定义的易变数据结构,避免对形状图逻辑的相关演算造成影响.此外,为分解易变数据结构中不同指针域带来的复杂性,形状检查方法引入了三阶段处理框架:形状分割、形状分析及形状推断,分别实现形状图的预处理,针对指针指向与节点类型等方面进行分析,以及根据相关规则推断易变数据结构的形状级别.

摘要：程序性质的自动验证有时需要验证者提供相关的归纳引理,程序验证的结果可靠与否依赖于验证者所提供的归纳引理正确与否。本文围绕操作易变数据的程序的自动验证,设计并实现一个相关引理的自动证明器,作为程序自动验证器中检查验证者所提供的归纳引理是否正确的工具。该证明器分析所有待证归纳引理,构建引理之间的依赖关系图,得出引理的证明顺序。对每个引理,分析得出它的归纳变元和应采用的归纳方法,把归纳证明的各步交给自动定理证明器Z3进行证明。该证明器的原型已嵌入一个基于演绎推理的安全C语言自动验证系统中,并成功验证了有序链表、二叉搜索树、AVL树、伸展树等数据结构的性质。