【摘 要】
：
随着传感网络以及嵌入式系统等的发展，集计算、通信、控制于一体的信息CPS逐渐成为人们关注的热点。未来CPS将会应用到社会生活的各个方面，随着应用的越来越普及，CPS能否满足设计需求对系统设计实施显得至关重要。验证技术在保障和提高系统安全性、可靠性等方面起到了关键的作用，对CPS关键属性的验证也成为研究的焦点。将通用的模型转换为形式化模型进行验证是常用的验证手段，采用HybridUML对CPS进行建
【机 构】
：
东南大学计算机科学与工程学院 南京 211189
【出 处】
：
2011全国软件与应用学术会议(NASAC2011)
论文部分内容阅读
随着传感网络以及嵌入式系统等的发展，集计算、通信、控制于一体的信息CPS逐渐成为人们关注的热点。未来CPS将会应用到社会生活的各个方面，随着应用的越来越普及，CPS能否满足设计需求对系统设计实施显得至关重要。验证技术在保障和提高系统安全性、可靠性等方面起到了关键的作用，对CPS关键属性的验证也成为研究的焦点。将通用的模型转换为形式化模型进行验证是常用的验证手段，采用HybridUML对CPS进行建模，并提出一种由HybridUML向Hybrid Programs 模型进行转换的方法。Hybrid Programs是基于微分动态逻辑的定理证明方法的操作模型。最后利用转换得到的Hybrid Programs对系统实例进行验证。
其他文献
本文介绍了在7.63m焦炉投产前期、生产调整中为提高焦炭质量进行的研究探索工作，通过前期资源研究、过程质量管理精细化、配套实施新工艺技术，实现了7.63m焦炉生产工艺稳定、产品质量大幅度提高，为炼铁高炉顺行创造条件。
利用风口焦炭取样机在首钢4号高炉、迁钢高炉、首秦高炉、京唐高炉进行了风口焦炭取样，取样深度超过高炉炉缸半径。通过对入炉焦炭质量、高炉技术经济指标的分析得出焦炭劣化度与煤比、风速，焦炭质量指标之间的关系。根据4号高炉焦炭取样的研究结果，分析了回旋区焦炭带的长度与实际风速、风口焦炭粒度及焦炭质量的关系；探讨了煤比与渣量及回旋区焦炭带的长度的关系；探索了高炉透气性指数与实际风速、煤比、风口焦炭粒度及高炉
当前，发展煤制气一气基竖炉已成为我国直接还原铁发展的主导方向。气基竖炉直接还原对球团矿性能的要求较为严格，基于国内铁矿原料条件，生产满足气基竖炉工艺要求的铁矿球团，探求其合理的生产工艺参数及冶金性能，是我国发展气基竖炉直接还原的前提条件。本研究以国内三种不同地区生产的铁精矿粉为原料，配加合理的粘结剂，制备铁矿氧化球团，研究三种成品球团的物性及冶金特性指标，并与相关标准进行比较。研究结果表明，基于国
软件资源库是对可复用软件资源进行管理、支持软件复用的重要基础设施。近年来，随着Internet的飞速发展，越来越多的软件资源库以网站的形式向使用者提供服务。这使得软件开发人员在使用软件资源库时不得不面临着IDE(集成开发环境)与使用资源库的浏览器环境相互独立的事实。为此，本文提出了一种面向IDE的软件资源库访问机制，它支持在IDE环境下对软件资源库的访问，辅助用户在IDE中实现对软件资源的封装、发
FLAMES是一种广泛使用于作战指挥流程仿真的战斗对抗系统。在面向FLAMES的作战指挥流程设计过程中，由于目前缺乏有效的描述方法来支持作战指挥流程可视化建模，导致业务人员之间沟通困难，作战指挥流程模型不易理解和维护。针对FLAMES平台给出了作战指挥流程的定义，建立了相应的元模型，为了能够支持作战指挥流程建模，基于给出的元模型定义了一种可视化作战指挥流程建模语言，分别从设计要求、语言定义和语言实
构件/组件是现代软件体系结构和软件工程的基石，业务构件化则是大规模软件生产、大粒度软件复用实践的一条有效途径。本文系统性提出一个业务构件化模型BCM来刻画具有高内聚、松耦合、可扩展特征的业务构件；以及一个可扩展的业务构件化应用框架xBCAF来支持应用软件全生命周期业务组织、管理和复用。并通过xBCAF的一体化设计与实现，展现如何通过业务构件化的方法途径，使规模化软件生产、软件复用和软件治理达成有机
在回归测试中，原有测试用例集往往不能满足软件修改带来的新需求而需要新增测试用例。与传统测试用例生成相比，测试用例集扩增在分析软件修改影响的基础上有针对性地产生新测试用例以提高测试效率。提出了一种基于谓词自适应随机测试(Predicate-Adaptive-Random-Testing，P-ART)技术的测试用例集扩增方法。该方法的主要创新在于结合软件修改分析的白盒测试技术与自适应随机测试(Adap
为了提高Web服务组合的可靠性，提出了一种时间异步Web服务交互的失配检测方法。首先采用基于时序逻辑的软件体系结构描述语言XYZ/ADL描述Web服务组合，并建立了一个可以精确刻画异步交互行为和时间属性的时间异步服务模型(TASM)，然后将XYZ/ADL描述转换为TASM，最后利用模型检测工具UPPAAL实现了异步Web服务的交互失配检测。
提出了基于体系结构失效传播的软件安全性分析方法。建立了新的面向失效传播的组件故障和失效特征模型，从组件层面对软件安全性进行量化分析；在体系结构设计早期从用户角度评估潜在失效的严重程度，并确定系统的安全性敏感点。
针时AUTOSAR OS在定时保护方面的功能需求，分析确定了定时保护的若干监测对象以及需要采取的保护性操作。为了避免基于OSEK OS报警机制的实现方案的缺陷，降低操作系统在执行监测时对CPU的额外开销，基于特定的嵌入式微处理器，充分利用其系统定时器模块的硬件特性，设计实现了一种改进的定时保护策略。应用实例证明，该实现能够有效运行，满足AUTOSAR OS对于定时保护的功能需求，并能有效降低对CP