摘要：LED灯具有长寿命,高效率和环保等优点,能满足不同环境的用户需求。本系统采用STM32F104主控芯片来控制四路恒流源用于驱动四种不同色彩的LED灯,将这种LED灯用在医院病房中,设置为按键控制模式和蓝牙控制模式,在正常情况下,以蓝牙控制为主,以按键控制为辅,病人通过手机蓝牙随时开灯关灯,选择灯的颜色和亮度,少了灯具的工作时间,避免了能源的浪费,而且给病人带来了极大的方便。

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

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