摘要:物联网设备的使用范围正在不断扩张. 模型检测是提升这类设备可靠性和安全性的有效手段, 但常用的模型检测方法不能很好地刻画这类设备常见的跨空间移动和通信行为. 为此, 提出一种面向物联网设备移动与通信行为的建模及验证方法, 以实现对这类设备时空相关性质的验证. 通过将推拉动作和全局通信机制融入ambient calculus, 提出全局通信移动环境演算(ACGC)并给出了ACGC对ambient logic的模型检测算法; 在此基础上, 提出描述物联网设备移动和通信行为的移动通信建模语言(MLMC), 并给出将MLMC描述转换为ACGC模型的方法; 进一步地, 实现模型检测工具ACGCCk以验证物联网设备的性质是否得到满足, 并通过一些优化加快检测速度; 最后, 通过案例研究和实验分析阐明所提方法的有效性.

摘要:信息物理融合系统（cyber-physical systems，简称CPS）是深度融合了计算进程和物理进程的统一体，是集计算、通信与控制于一体的下一代智能系统，具有广阔的应用前景.CPS的行为具有混成性、随机性等特征，建模及仿真CPS的动态行为对于开发高质量的CPS系统至关重要.但是目前缺乏面向CPS的领域建模方法及建模CPS的领域建模语言，也迫切需要支持仿真CPS领域模型的仿真工具.针对以上问题，提出一种面向CPS领域的随机混成建模语言（stochastic hybrid modeling language，简称SHML）以支持建模CPS系统的行为.首先，根据CPS的领域特征定义了SHML的元模型作为其抽象语法，并定义了SHML的具体语法和操作语义；其次，基于GEMOC框架实现了SHML的可视化建模工具.此外，集成GEMOC的序列化执行引擎和Scilab的连续行为仿真引擎，实现仿真CPS的混成行为.提出了一种面向CPS领域的建模及仿真方法，设计并实现了一个集成的面向CPS行为的建模与仿真平台，为CPS的建模及仿真提供了一种有效的方法及工具支撑.

摘要:随着智能机以及平板电脑的普及，安卓应用逐渐成为日常生活中不可或缺的重要元素之一，其复杂度也呈几何倍数增长.安卓平台存在的多设备类型、多操作系统版本问题，使得应用的设计和开发更为复杂.在这一现状下，提倡在安卓应用开发中使用模型来描述其开发需求与设计，以帮助开发人员更好地将注意力集中于应用，加深对开发意图的理解，更好地进行后续的开发工作.然而，当前对安卓应用的建模都采用了传统模型，无法满足安卓应用事件驱动和注重图形用户界面的特点.为此，将注重前端展示以及事件交互的交互流建模语言（IFML）应用于安卓应用的建模，描述应用中的GUI结构以及其中工作流的传递，从而指导应用的开发工作.考虑到安卓平台的特点，对IFML进行了相应的面向安卓的扩展，提高了其可用性与对安卓应用的适用性，并对IFML模型进行了形式化定义，使得IFML模型能以丰富而又精确的语义来刻画开发者对于安卓应用的设计，并在应用的实现和演化中不断发挥指导作用.另外，进一步探索了IFML模型在应用测试这一场景中的作用.基于模型的测试方法能够检验设计和实现的一致性，还能在应用的演化过程中避免测试用例的重复编写.在案例研究中，针对5个安卓应用进行了IFML建模与测试.实验结果表明，扩展后的IFML在安卓应用的建模上可行、有效，所建立的IFML模型可直接用于测试工作，用于检测应用实现与设计是否保持一致，从而保证应用的开发质量.

摘要:非形式化仿真模型验证方法易受主观因素的影响且具有不完备性,而传统的形式化模型检验方法由于受到状态空间爆炸问题的影响,很难处理大规模的仿真模型.并行模型检验方法以其完备性、高效性已经在工业界中得到了成功的应用,但是由于涉及到形式化规约、逻辑学以及并行计算等多项技术,应用难度较大.针对上述问题,提出了基于事件图的离散事件仿真模型并行检验方法.该方法首先对事件图在模型同步方面进行了扩展,给出了扩展事件图的形式化定义、语法及语义;然后将扩展事件图模型转换到分布并行验证环境的DVE 模型,成功地将并行模型检验方法应用于仿真模型验证领域.该方法使得仿真人员无须学习新的形式化验证语言就能采用并行模型检验方法对仿真模型进行形式化验证,可降低模型并行验证的难度,从而有效提高模型验证的效率和完备性.实验结果表明了该方法的有效性,有利于扩展并行模型检验方法在仿真领域中的应用.

摘要:提出了一种大类图拆分方法。首先通过度量工具计算类图中类目(类及接口)间的耦合度。根据面向对象设计中高内聚低耦合的设计原则，将紧耦合的类目划入同一个类图，而耦合度低的类目间实现分离。为了确保生成的类图大小合适，拆分方法对每个类图的大小进行限定，将每个类图的大小限定在预先定义的合理区间内。通过在实际系统中的应用，拆分方法的合理性和有效性得到验证。该大类图拆分方法有利于逆向工程的进一步完善，有利于提高软件模型的可读性和可理解性。

摘要:随着UML(unified modeling language)与MDA(model driven architecture)的兴起和流行,模型已经成为软件开发的核心制品,而模型重要性的提升使得建模语言以及定义建模语言的元模型逐渐成为软件开发中的一个核心要素.软件开发往往涉及多个领域,而不同的领域往往需要不同的建模语言及其建模工具.但是,手工地为不同的建模语言开发建模工具代价高昂.元建模技术是解决这个问题的方法之一,通过元建模,可以根据领域需要定制合适的元模型以定义领域建模语言,进而自动生成支持该建模语言的建模工具.大量的工程实践表明,与领域建模以及MDA相结合,元建模可以大幅度地提高软件开发效率,基于元建模的MDA比基于通用建模语言的MDA更具潜力.在最近的几年中,元建模及其相关技术发展迅猛,不但在技术上取得了长足的进步,而且在产业界也开始出现大规模的商业应用.总结了元建模的现有研究成果,分析和比较了现有元建模工具,探讨了元建模的可能发展方向.对元建模中存在的问题进行分析,并指出了可能的解决途径.

摘要:对于图形化的建模语言,为定义其表示法一般需要解决3个问题:如何定义每个建模元素的图形符号,如何定义图形符号之间的位置关系以及如何将表示法映射到抽象语法.为了方便进行模型转换和代码生成,还需要使用模型化的方式描述建模语言的表示法.通过对UML及其语言家族中的表示法进行总结、分析和归纳,提出了一种表示法定义元模型(notation definition metamodel,简称NDM).针对定义表示法所面临的3个问题,NDM被分成基本图元及其布局、基本位置关系和抽象语法桥三部分.使用NDM定义好的表示法模型还可以通过代码生成技术生成可使用的源代码.将NDM与其他几种定义表示法的方法进行了比较,结果表明,NDM与其他方法相比具有优势.NDM已经在元建模工具PKU MetaModeler中实现.介绍了NDM在实际应用中的几个案例.

摘要:软件体系结构设计是软件过程中最为重要的环节之一.在设计阶段完成对软件体系结构非功能属性的评估,对于高质量软件产品的开发非常重要.通过对统一建模语言(UML)的扩展,提出了建模样式用于在软件设计阶段对软件体系结构非功能属性进行评估,并结合可用性链建模样式在分析软件体系结构单消息分发-多消息处理可用性中的应用,给出了建模样式的使用示例.同时,针对建模样式的应用,还提出了建模知识库用于管理和维护建模样式,提供各建模样式中标签的参考值.基于UML的建模样式以及建模知识库的使用,可以简化对软件体系结构非功能属性评估的复杂度和工作量,使其可以为软件开发人员所用,并融入到高质量软件开发过程中.

摘要:软件统计测试要求基于软件使用模型产生测试例对软件系统进行测试,并根据测试结果评价软件可靠性,是高可靠软件测试的重要组成部分.由于统一建模语言(unified modeling language,简称UML)已经成为事实上的面向对象标准建模语言,因此,从软件UML模型构造软件使用模型就成为面向对象软件统计测试的关键.为此,定义了加入统计测试约束的UML用例图、序列图以及用例执行顺序关系,为基于UML的软件统计测试提供了一个形式化描述基础.在此基础上,给出一个从软件UML模型构造软件Markov链使用模型的算法,并给出了自动化支持工具UMGen的类图结构,基于一个卫星控制系统,说明了所提出方法的有效性.

摘要:过程支撑环境PSE(process supporting environment)是一种支持软件过程元过程的计算机环境,PSE通过运作一个事先定义好的软件过程模型SPM(software process model)来控制和指导实际软件开发过程.SPM使用的控制方式分为主动式(proactive)和反应式(reactive)两种.由于主动式不能很好地支持软件过程的演化,反应式渐渐受到人们的重视.提出了一种反应式SPM以及建立这种模型所使用的图形化的软件过程建模语言,同时,对于所建立的SPM,提出用时序逻辑语言XYZ/E表示它的行为视图动态语义的方法.这为模型提供了明确的动态语义,为其运作和分析提供了形式化基础.