模型驱动的嵌入式系统设计安全性验证方法研究

基于模型的嵌入式系统安全性分析与验证方法是近年来在安全攸关系统工程领域中出现的一个重要研究热点。提出一种基于模型驱动架构的面向SysML/MARTE状态机的系统安全性验证方法,具体包括:构建了具备SysML/MARTE扩展语义的状态机元模型,以及安全性建模与分析语言AltaRica的语义模型GTS的元模型;然后建立了从SysML/MARTE状态机模型分别到时间自动机模型以及AltaRica模型的语义映射模型转换规则,并基于AMMA平台和时间自动机验证工具UPPAAL设计实现了对SysML/MARTE状态机的模型转换与系统安全性形式化验证的框架。最后给出了一个飞机着陆控制系统设计模型的安全性验证实例分析。     

基于Ansys和Nastran的太阳电池阵建模及模态分析

用Ansys与Nastran两种求解器对同一个太阳电池阵模型进行求解，详细介绍模型创建、网格特性检查和单元属性设置的方法。通过模态分析并比较计算结果，验证同一个模型在不同求解器下参数设置的正确性，为有限元模型格式的转化提供参考。     

基于Petri网的一种时序分析方法

Ｐｅｔｒｉ网由于有强大的建模能力和成熟的理论支持,被广泛应用于各种系统的建模．本文通过把Ｐｅｔｒｉ网转换成转移系统,利用转移系统和Ｋｒｉｐｋｅ结构给出时序逻辑语义的解释,从而建立了一种在Ｐｅｔｒｉ网上进行时序分析的方法．这种方法是根据不动点理论,用模型检查验证公式正确性．通过对Ａｄａ程序会合性质进行模型检查,验证了这种方法的有效性．     

Isabelle在分析安全操作系统状态机模型中的应用

为了解决已有的状态机模型的形式化框架在分析安全操作系统状态机模型时不够直观、简洁的问题,提出了一套使用Isabelle工具对安全操作系统模型状态中的类型、变量、常量、关系、映射、函数,以及模型中的安全不变量和状态迁移规则进行形式化描述的新方法.通过实际验证一种典型的安全操作系统状态机模型--可信进程模型,总结出了有效地使用Isabelle辅助形式化设计、分析、验证模型的策略.     

模型检测迷惑二进制恶意代码

对二进制恶意代码进行形式化建模,开发了一个检查迷惑恶意代码的模型检查器。生成迷惑前的二进制恶意代码的有限状态机模型,再使用模型检查器检测迷惑二进制恶意代码,如果迷惑二进制恶意代码能被有限状态机模型识别,可判定其为恶意代码。实验结果表明模型检查迷惑二进制恶意代码是一种有效的静态分析方法,可以检测出一些常用的迷惑恶意代码。     

基于SMT的区域控制器同步反应式模型的形式化验证

在安全关键系统的软件开发过程中,形式化验证是一种经检验的提高软件质量的技术.然而,无论从理论上还是从应用角度来看,软件的验证都必须是完整的,数据流验证应该是对实现层软件模型进行验证的必要体现.因此,环境输入、泛型函数、高阶迭代运算和中间变量对于分析形式化验证的可用性至关重要.为了验证同步反应式模型,工程师很容易验证控制流模型(即安全状态机).现有工作表明,这类工作无法全面地验证安全关键系统的同步反应式模型,尤其是数据流模型,导致这些方法没有达到工业应用的要求,这成为对工业安全软件进行形式化验证的一个挑战.提出了一种自动化验证方法.该方法可以实现对安全状态机和数据流模型的集成进行验证.采用了一种基于程序综合的方法,其中,SCADE模型描述了功能需求、安全性质和环境输入,可以通过对Lustre模型的程序综合,采用基于SMT的模型检查器进行验证.该技术将程序合成作为一种通用原理来提高形式化验证的完整性.在轨道交通的工业级应用(近200万行Lustre代码)上评估了该方法.实验结果表明,该方法在大规模同步反应式模型长期存在的复杂验证问题上是有效的.     

基于Web应用的SCXML到自动机的转换

为了对Web应用进行验证,保证Web应用的可靠性和质量,提出了将Web应用的SCXML描述提取出通用状态机的算法.在对Web服务应用的语言SCXML的各构成要素进行深入分析的基础上,该算法实现了将SCXML描述转化为相应的自动机,为对Web应用进行模型检查打下基础.对Web应用游戏系统的SCXML文件转换得到了对应的自动机实例,实验结果表明了该算法的正确性和有效性.     

有界模型检查可执行文件的安全属性

引入模型检查方法对可执行文件进行脆弱性分析.对可执行文件形式化建模,采用有界模型检查技术验证可执行文件的安全属性,并在X86体系结构上开发了一个用于可执行文件的模型检查器.实验以内存泄漏和栈溢出漏洞为例,将其属性描述为线性时序逻辑公式,在可执行文件的状态迁移系统模型中验证公式是否能满足,实验结果表明对可执行文件的有界模型检查是一种有效的静态分析方法.     

基于SMV的网络协议形式化分析与验证

提出了采用模型检验方法对网络协议进行形式化分析及自动验证,建立了一个特定网络协议PAR的有限状态机模型,并用模型检验工具SMV验证其正确性,发现了该协议存在的一些缺陷。结果表明,利用符号模型检验方法分析检验网络协议是可行的。     

分布式软件系统交互行为建模、验证与测试

为了确保分析与设计阶段分布式软件系统中模块之间交互行为的正确性,提出了一种分布式软件系统模块交互的抽象方法,分别通过系统状态机图和对象状态机图对各模块状态变迁进行建模,使用UML2．0序列图对模块之间交互行为进行描述．采用基于命题投影时序逻辑的模型检测技术,将对象状态机图转换为 Promela 模型,系统交互性质转换为命题投影时序逻辑公式,通过模型检测器验证交互模型是否满足于系统的性质,若不满足于该性质,则能够获得反例执行的路径．给出了一个分布式软件系统测试框架,在验证后的序列图模型基础上,使用基于模型的测试用例自动生成方法得到测试用例集合,该集合能够实现对交互行为的有效测试．实例结果表明,该方法可以提高分布式软件系统中模块交互行为的有效性和可靠性．     

模型驱动的产品应用服务建模方法

为了将应用服务需求转换成模型,最终指导和实现产品应用服务系统的快速构建,提出一种模型驱动的产品应用服务建模方法。在元对象机制的元模型层建立可拓物元形式化描述与面向对象元模型元素的映射关系,给出UML可拓扩展机制,形成适合描述产品应用服务的可拓UML复合语言;分析产业链业务协作过程中的产品资源与组成服务要素,建立面向产品应用服务的四层模型驱动架构,研究架构的四层驱动模型之间的转换关系;通过案例验证了所提方法的可行性和有效性。     

UML类图中面向非功能属性的描述和检验

为系统构建模型是软件开发中的一项关键活动.一个高质量的模型不仅要包含系统的功能属性,即系统能够做什么,同时还应包含系统的非功能属性,即系统的质量如何.目前,通用的建模方法和工具对功能属性建模支持良好,而对如何为非功能属性建模关注得不多,特别是如何将二者统一起来并对描述的非功能属性的有关性质进行检验.通过在UML类图中增加非功能属性标注和约束关系表等建模元素来扩展UML类图,使其能够描述非功能属性.在此基础上,又提供了对扩展UML类图中非功能属性的一致性和可满足性进行检验的方法.通过实例对上述的面向非功能属     

基于UML的软件使用模型的研究与实现

UML作为事实上的工业标准,在软件开发中得到了日益广泛的应用。软件可靠性测试是高可靠软件质量保证的重要过程。研究基于UML的软件可靠性测试具有很强的现实意义。软件使用模型是进行软件可靠性测试的基础,可利用在软件开发早期阶段生成的UML模型,如用况图、顺序图、活动图,自动生成软件使用模型。     

基于UML实时系统的分析和设计

介绍了统一建模语言的最新版本UML2及应用UML2进行实时系统设计的作用及意义.探讨了UML2中用在实时系统设计中的概念.结合一个使用UML2为家庭安全系统设计的例子,着重分析了系统的静态结构和动态行为,通过类图、顺序图、状态图等UML图描述系统的方法从整体上对系统建模,说明实时系统分析与设计过程.使用UML分析和设计系统能够提高软件设计的效率和质量增强软件的维护性和复用性.     

基于UML的电子商务系统的分析和设计

随着商业软件的发展，传统的系统分析设计的方法已不能很好地适应现在的要求。该文通过介绍eBox电子商务系统的分析和设计，介绍了UML的概念和如何在系统分析设计中应用UML，实践表明在应用软件开发中应用UML对提高应用软件的开发效率和质量有很大的帮助，它很好地解决了现存的问题。UML在软件开发中具有很广阔的应用前景。     

基于UML顺序图的安全苛求软件安全性分析

安全性分析对于确保开发出符合安全性需求的软件系统非常重要。该文从安全苛求软件的建模特点出发,分析现有的安全性分析方法和UML建模语言在安全苛求软件方面的应用及优缺点。针对UML面向安全性需求建模的不足,对顺序图增加了安全性描述方法。通过车载ATP系统的建模应用验证其可行性与有效性。     

UML模型检测方法的研究

统一建模语言（UML）是设计和分析软件系统最常用的方法，如何保证UML模型满足某些特性是一个非常重要的问题，而模型检测是一种能够有效提高系统可靠性的自动化技术。研究了使用简单进程元语言解释器（SPIN）对UML模型进行检测的方法。首先对UML模型进行形式化描述，使用层次自动机来描述状态图，然后根据层次自动机的操作语义将状态图和类图的部分信息转化为SPIN的输入语言PROMELA，使用SPIN来验证模型是否满足给定的线性时序逻辑所描述的系统约束，通过LTL公式描述顺序图的方式来验证与状态图之间的一致性问题。项目组基于此方法还开发了一套模型检测工具UMLChecker。     

Research on the measure method of complaint theme influence on online social network

Consumer complaints on online social network quickly become online groups complaints through many people’s aggregation and looking on, interaction and word-of-mouth communication. Therefore, assessing and managing online complain influence has become a new problem for enterprise to listen to and manage online group complaints. This paper analyzed the complaint information feature of consumer group on online social network, from three-dimensional perspective of complaint text’s quality, transmission timeliness and user interaction degree. We built the influence measure model of online complaint theme based on entropy weight model by monitoring and analyzing real-time the static and dynamic properties of complaint information, explored the measure method of complaint theme influence, employed empirical method to verify the validity and provided scientific decision-making tools and methods for enterprise listening to and managing online group complains.     

Verification of problem-based learning systems using modified petri nets

In this paper, we intend to verify a web-based system on problem-based learning (PBL). To consider the design flow of the web-based PBL system, it is essential to avoid the potential hazard introduced by a logically incorrect system design. In order to eliminate the potential hazard, we define a new class of Petri net, namely, an Activity Flow (AF) net, which is suitable to be converted from a UML (Unified Modeling Language) activity diagram. Through the siphon-based deadlock detection of the AF net, we can find whether there is a process hazard in the UML activity diagram or not. This is helpful to implement the PBL system and to ensure the correct activities and the right control flow. In addition, we attempt to enhance the quality of the system verification by using a questionnaire. Thus we can interpret the user’s level of satisfaction with the designed PBL system. These two verification approaches bring us to achieve an adequately positive response to the web-based PBL system.     

基于威胁模型的软件安全性测试

相对于传统测试主要关注软件的肯定需求,安全性测试则主要关注软件的否定需求。基于威胁模型的软件安全性测试是从攻击者的角度对软件进行测试。使用UML顺序图对安全威胁进行建模,从威胁模型中导出消息序列,从消息序列中导出威胁行为轨迹。程序编码完成后,对代码进行插桩以记录程序运行时的方法调用和执行的轨迹。设计测试用例,执行插桩后的程序并记录程序运行时的执行轨迹,将记录的程序执行轨迹与模型中导出的威胁行为轨迹进行比较,以确定程序中是否存在违反安全策略的威胁行为。