Ar/T-Net:一种面向Artifact的业务过程概念模型

以数据为中心是业务过程管理发展的新趋势,面向Artifact的业务过程管理是一种具有代表性的以数据为中心的业务过程管理技术。概念模型设计是面向Artifact的业务过程设计的关键步骤,但目前还没有成型的建模和分析工具。利用谓词/变迁Petri-Net建模的优势,根据Artifact的特点,用嵌套关系模式定义Artifact的结构;以描述Artifact的嵌套关系模式作为谓词,提出了一种适合于概念模型设计的谓词/变迁Petri-Net,即Ar/T-Net。以可达性分析为例,讨论了Ar/T-Net的功能。

基于加线技术的轨道交通临客开行计划优化模型

基于运行图加线技术构建适于计划性临客开行的运行线铺画方法.以运力与客流匹配度最大化、对原运行图调整最小化为优化目标,考虑行车安全、临客加线位置、开行时间域等约束,构建临客运行线铺画非线性整数规划模型,并对其线性转换以提高求解效率.以北京地铁8号线某大型活动散场大客流为场景进行案例分析,结果表明:所构建方法能够在既有运行图上有效铺画临客运行线,满足不同行车密度及停站模式下的临客开行需求.建议在较高密度行车条件下不采用“空车直达”停站模式.

无源微波遥感用于地震预测及物理机理研究

对不同岩性的岩石进行了无源微波遥感用于地震预测的实验研究，实验在等温过程加载条件下进行．实验得出岩石的微波辐射能量随岩石的应力状态变化而显著变化，这个变化完全由应力引起，与温度无关．将介质所处的应力状态同介质的微波辐射能量变化与物理机理直接地联系了起来，为无源微波遥感观测地球表层应力场分布和预测地震奠定了物理基础，并提供了实验依据．本文提出了无源微波遥感预测地震的两种物理机理，即热能激发机理和机械能激发机理；提出了由无源微波遥感探测结果，反演介质应力状态和温度状态的方法．

一阶谓词逻辑的图形推理法

针对已有一阶谓词逻辑推理方法中存在的推理效率低等问题,研究一种基于谓词/变迁系统的图形推理法。定义了描述谓词间与/或关系的谓词-与/或图,借助谓词-与/或图表示谓词/变迁系统,提出一种实现反向推理的目标制导的图形推理法。该方法推理效率高,较已有的推理方法具有一定的优越性。

转折性天气降水预报检验方法及应用

采用转折性天气降水检验评估方法,从转折天气预报能力的角度评价了模式降水预报能力。对全球中期T213、日本和德国数值预报模式在2006年9月至2008年8月的降水预报检验评估分析表明:转折天气降水预报能力检验是目前降水检验方法的有效补充。3种模式的转折天气降水预报能力随着预报时效的延长,存在逐渐递减的趋势;短期预报能力分析,T213和日本模式春季最好,而德国模式是夏季最好;48h预报分析,T213和日本模式在长江中下游、华北及东北等部分地区、德国模式在四川盆地和华南部分地区预报效果较好。

谓词/变迁系统对一阶谓词公式的建模

研究了利用谓词/变迁系统对一阶谓词公式建模的方法。借助于软件工程中"由粗到细,逐层分解"的思想,定义了对各种逻辑联结词进行处理的基本模型。给出了一阶谓词公式的二叉树表示方法,进而利用二叉树的递归性质,提出了递归构造一阶谓词公式对应的谓词/变迁级的"事实变迁"表示的方法,克服了已有相关建模方法中存在的不足,为一阶谓词公式的自动化建模提出了新的思路。最后,探讨了一阶谓词公式的谓词/变迁系统模型在谓词逻辑推理领域的应用及其意义。

利用谓词/变迁网证明的一阶谓词逻辑命题

研究了证明一般的一阶谓词逻辑命题的方法,根据网逻辑的思想,利用谓词/变迁网对一般形式的一阶谓词逻辑命题进行了图形表示,提出了2种一阶谓词逻辑命题的证明方法:图形证明法和矩阵证明法。举出一个实际的例子来说明证明思路。

基于Petri网的数据库概念设计模型

在数据库概念设计阶段,E-R图虽然广泛使用,但反映不出对数据的处理要求和数据库的完整性要求。提出了用Petri网建立数据库概念设计模型,把数据及其相关的处理集成在统一的网模型中,而且用事实(死变迁)规范了该模型的数据库完整性。

基于 Petri 网和图像识别方法的故障预防系统研究及实施

以国家ＣＩＭＳ工程技术研究中心制造系统为对象，设计并实施了一个制造系统故障预防系统。文中首先提出了制造系统的谓词／变迁网模型，以此为基础设计了基于Ｐｅｔｒｉ网可达性树分析方法和图像识别方法的制造系统故障预防系统，并给出了系统的总体结构图和相应的模块结构图。该故障预防系统已完成实施，在提高制造系统运行的安全性和可靠性方面，发挥了重要作用。

Agent系统软件体系结构形式化建模方法

基于Agent技术为复杂分布式问题提供了求解方法。软件体系结构是控制软件复杂性、提高软件系统质量、支持软件开发和复用的重要手段之一。软件体系结构设计可用于描述Agent与Agent之间的交互和组织结构的规划,因此Agent系统能从良好的体系结构设计中受益。该文整合了图表句法理论和层次谓词变迁网理论,提出一种形式化建模方法,从抽象层(架构)和实现层(动态行为)两方面来构建Agent系统的软件体系结构。模型具有可验证和追踪性,为Agent系统软件体系结构分析与评估提供了良好的基础。

防空导弹C^3I系统谓词/变迁赋色Petri网建模与仿真

介绍了Perti网概念及其标识转移方程的完整动态描述。对复杂的防空导弹C3 I空防对抗过程进行了具体分析 ,描述了某型防空导弹的具体作战过程 ,在有机结合谓词公司Petri网和赋色Petri网基础上 ,建立了基于谓词 /变迁的赋色Petri网模型 ,给出了具体的前置谓词公式。最后对仿真流程进行了描述 ,对战术级指挥控制过程的评估研究有极其重要的意义。

计算网格的抽象定义

计算网格是第三代因特网和高性能并行计算的研究热点,它提供了一个有效的平台,共享资源,支持全球范围内分布异构应用程序的运行,其动机和目标是明显的,并被人们广泛认同和接受。但是目前网格系统尚无一个清楚的定义,因此基于网格语义,通过高层抽象,用谓词/变迁系统给出计算网格的框架模型。

面向Artifact的业务过程模型

提出一种面向Artifact的业务过程形式化模型。利用谓词/变迁Petri网建模的优势,根据Artifact的特点,用半结构化数据描述Artifact,以表示Artifact结构的文档类型定义作为静态谓词,通过一种操作XML的一阶逻辑语言描述变迁。实验表明,该模型能有效分析Artifact的可达性、持久性和唯一性等问题。

基于符号迁移图的互模拟验证算法

符号迁移图是传值进程的一种直观而简洁的语义表示模型。该模型由Hennessy和Lin首先提出 ,随后又被Lin推广至带赋值的符号迁移图。本文不但定义了符号迁移图各种版本 (基 /符号 )的强操作语义和强互模拟 ,提出了相应的强互模拟算法 ,而且通过引入符号观察图和符号同余图 ,给出了其弱互模拟等价和观察同余的验证算法 ,给出并证明了τ 循环和τ 边消去定理 ,在应用任何弱互模拟和观察同余验证算法之前 ,均可利用这些定理对所给符号迁移图进行化简。

离散数学教学实践的探索

立足挖掘离散数学中概念和原理本身的显性和隐性知识,通过导入抽象概念的实际应用背景,强化概念的详细分析和解读,设计能够剖析公式内涵的例题等方法,对提高教学质量实现培养抽象思维和逻辑推理能力的课程教学目的进行了创新探索。

有限构模器的扩展及其在形式化方法中的应用

规约在软件开发和验证中占有重要地位 .对于以一阶逻辑为基础的规约 ,可以利用有限模型构造技术对其执行并测试 .文中研究规约中某些特性的处理 ,包括存在量词以及二元关系的传递闭包 .对已有的一个构模工具进行扩充 。

STGA的变种及其互模拟验证

为刻画和验证无穷值域上的传值进程，Ｈｅｎｎｅｓｓｙ和Ｌｉｎ先后提出符号迁移图（ＳＴＧ）和带赋值符号迁移图（ＳＴＧＡ）作为传值进程的语义表示模型，并给出了相应的强互模拟算法．为将该方法推广至实际应用中更常用的弱互模拟等价和观察同余的验证问题，该文首先引入了ＳＴＧＡ的一个变种，它与原模型的不同之处在于将符号迁移上赋值和符号动作的执行次序颠倒，因而可定义此种ＳＴＧＡ结点间的符号双迁移关系．文中提出了从正则传值进程生成此类ＳＴＧＡ的全部产生规则，并基于Ｌｉｎ的迟强互模拟算法给出了针对此类ＳＴＧＡ的早强互模拟算法．然后利用符号双迁移关系引入了带赋值的早符号观察图（ＥＳＯＧＡ）和早符号同余图（ＥＳＣＧＡ），将上述算法推广至早弱互模拟等价和早观察同余的情况．但符号迁移上赋值的出现有可能导致ＥＳＯＧＡ和ＥＳＣＧＡ为无穷图，从而使本文所给的弱互模拟算法在适用范围和效率上受到一定的局限．最后，作为一种可应用的情况，进一步考虑了符号迁移图的弱互模拟等价和观察同余验证问题．此时由符号双迁移关系生成的符号观察图和迟符号同余图必为有穷图，因而我们的弱互模拟等价算法是可行的．与此同时，文中还给出并证明了符号迁移图上的τ－循环和τ－边消去?

新一代制造控制系统的集成模型

在异构式制造控制系统体系结构的基础上 ,围绕系统分解后各局部自治对象的个体行为怎样与系统总体目标保持一致的问题 ,对制造控制系统的集成模型进行了探讨。在 Dr.Scherr提出的顾客—供应商链模型的基础上 ,构造出系统内局部自治实体间顾客—供应商关系网模型。为进一步强调合作双方在活动中所扮演的角色及其责任 ,建立了描述顾客—供应商之间完整活动过程的谓词 /变迁网模型。为确保系统内个体行为的可控性 ,提出了三层次的异构式控制模型 ,并通过第三方对上述模型进行监督和协调。最后开发了实际应用系统。

形式化B描述测试序列自动生成研究

基于严格数学理论的软件形式化规格说明,经过逐层精化,不仅可以让软件开发过程更加有效精准,而且为测试用例测试序列的自动生成提供了最原始可靠的依据。通过B抽象机操作的规范型,依据测试理论,可以将原操作等价于多个效用谓词(effect predication)的形式。按照路径覆盖得到状态转换图,并对状态图做了确定性处理;运用基于状态图的测试准则,生成有效的测试序列,提高测试的有效性和效率。

面向代数规约测试谓词/变迁网

针对谓词/变迁网缺乏有效的形式化验证分析技术,基于代数规约测试谓词/变迁网方法,给出谓词/变迁网转换成代数规约语言CASOCC-WS表示的基调的规则,提出基于测试充分性准则深度优先遍历谓词/变迁网生成变迁触发序列的算法和由变迁触发序列构造公理等式的启发式规则.案例研究表明:该方法可以有效地解决测试Pr/T网时自动生成测试用例和自动判定测试结果和可行路径的问题.