摘要：针对软件开发过程中安全性分析与设计不足的问题,在研究现有软件安全性建模及形式化验证技术的基础上,提出了一种适用于面向对象的软件安全性建模与验证方法.建立软件安全属性的非形式化UML模型,采用安全扩展有限自动机创建其形式化模型,并使用线性时序逻辑描述安全属性,将形式化模型与安全属性共同作为模型检测器的输入,得到模型是否满足性质的验证结果,从而实现了软件安全设计与验证技术的有机结合.实验结果表明,该方法能够在软件设计初期对所涉及的安全性进行有效分析与验证.

摘要：从优化制造企业内部物流配送管理模式考虑,提出了一种呼叫应答式物料索取配送方式,设计实现了一种基于单片机ATmega128的物料索取系统。详细分析了物料索取系统的设计思想及系统架构,阐述了物料索取系统索取端与配送端的设计及实现,论述了索取端和配送端之间以及与上位机之间的通信。

摘要：目的为在软件设计与开发早期阶段对软件安全模型进行有效分析和验证。方法软件安全分析验证法与形式化建模方法。结果提出了一种安全扩展确定有限自动机(safety extended deterministic finite automata,SEDFA)。在使用UMLsec建立软件安全相关的非形式化模型基础上,通过SEDFA准确的描述能够表达安全交互的序列图。首先创建序列图中单个对象的自动机,其次构造对象积自动机,从而得到表示系统整体交互的SEDFA。结论为系统安全属性的验证提供了基础,可作为下一步生成软件安全测试用例。