摘要：随机 Petri网的模型技术有多种不同的方法 .简单地使用模型技术去模拟复杂的系统 ,势必造成状态空间的爆炸 ,而无法分析系统性能 .模型精化技术可以开发出紧凑的模型 ,暴露出原模型中子模型的独立性和相互依存关系 ,为模型的分解求解奠定基础 .该文以多服务器多队列系统模型的精化设计为例 ,展示利用变迁可实施谓词和随机开关进行模型精化的方法 .文章还讨论了多服务器多任务系统的调度、选择控制方案 ,并提供了这些方案的随机 Petri网模型 .

摘要：系统差之和∑si≠0时,利用附加系统差之和∑si=0的半参数模型往往得不到较好的数据处理结果,文中从理论上对系统差附加条件进行了改进,并基于改进前、改进后的半参数模型以及经典最小二乘平差模型对系统差之和∑si≠0时的算例进行处理。结果表明,改进后的半参数模型大大提高了数据处理精度。

摘要：机载软件被广泛应用于航空航天领域,大幅提升了机载设备的性能.随着机载软件规模逐渐增大、功能逐渐增多,给软件的开发带来了难度.如何保障机载软件的正确性和安全性,也成为一个难题.基于模型的开发可以有效提升开发效率,而形式化方法能够有效保障软件的正确性.为了降低开发难度,同时保障机载软件的正确性、安全性,提出一种基于SysML状态机图子集的机载软件分层精化建模与验证方法.首先,使用SysML状态机图对机载软件的动态行为进行建模,根据提出的精化规则对初始模型进行手动逐层精化,得到精化设计模型;然后,针对软件模型动态变化的特性,将SysML状态机模型自动转换为时间自动机网络,并从软件需求中手动提取形式化TCTL性质进行模型检验.其次,为了实现编码自动化,将SysML模型自动转换至Simulink,利用Simulink Coder生成源代码.最后,以一个自动飞行控制软件为例进行了开发和验证,实验结果表明了该方法的有效性.

摘要：从软件设计实践出发,针对基于Web应用服务和设计模式的软件设计方法,提出了一种新的模型驱动开发理论框架.该框架以类型范畴理论为基础,以服务构件标识为范畴对象,以服务构件之间的交互和依赖关系为范畴态射,从而用范畴图表给出了软件体系结构模型的框架描述.设计模式看成是构件规范的模板,模板的实例化和规范的集成过程就是软件设计和实现的过程,从而建立起了模型转换和精化中特性描述和一致性研究的统一框架.应用研究表明,该框架符合模型驱动软件设计的本质要求,为模型转换和模型驱动的Web应用服务开发提供了新的认知、分析和研究的指导架构.

摘要：UML由于其广泛的应用和直观的图形化符号,成为了模型驱动工程的重要组成部分。但UML本身缺乏精确的形式语义定义,缺少对其模型精化关系的形式化规范定义,对UML模型进行形式验证变得尤为困难。UML类图作为描述系统结构的静态模型,不具备完整的形式语义。从UML类图的机械语义中抽取出形式规约,将UML类图中的结构和形式规约转换成定理证明器Coq中的机械语义定义。此外,还提出了类图的结构精化操作,将模型间的精化关系在Coq中进行形式化定义,并且对精化操作的原子操作进行机械验证,保证其精化前后系统的结构和语义保持一致。将UML和形式化方法相结合,为可验证的软件设计精化框架提供了理论依据。