两类网络图的边-平衡指数集

在较小次幂圈嵌套网络图的基础上,研究了10次幂嵌套网络图的边-平衡指数集。利用基础图、带齿套圈子图、单点扇形子图设计新思路,降低了构造标号图的复杂程度。当n=10为偶数时,提出了新的变换指数方法,简化了证明过程。确定了m模6余1和余3且m大于等于2时(m为圈数)无限路10次幂圈嵌套图的边-平衡指数集,并且解决了这两类幂圈嵌套图的边-平衡指数集的存在性,给出了具体构造方法和公式证明。     

基于Bigraph理论的动态演化软件相关特性分析与验证方法

软件演化中的行为一致性、相容性以及系统完整性约束,长期以来是动态演化中研究的热点.本文利用Milner等提出的Bigraph理论对软件演化中的特性进行研究.与以往利用Petri Net、演算及进程代数不同,Bigraph融合演算和移动Ambient 演算的优势,其目的为现有的移动和并发理论建立统一的元模型,并且引入环境上下文参与系统的迁移,使系统的描述更为直观和精确,从而适合对动态演化形式化.本文简要介绍Bigraph的基本概念和现状,利用Bigraph建立演化系统的构件模型,并在Bigraph理论基础上给出分析和验证完整性、一致性和相容性相关规则,并通过具体实例验证利用Bigraph对动态演化建模的有效性.     

Bigraph理论在自适应软件体系结构上的应用

现有的软件体系结构形式化方法对体系结构的动态性、自适应性支持有限,并不能很好地验证系统演化过程中的一致性、完整性等动态特征.Bigraph理论融合了,π演算和移动Ambient演算的优势,重点强调计算的位置和连接两方面因素,具有较为完整、可扩展的理论框架.这使得Bigraph不仅在概念上能够满足现有自适应软件对结构和行为的需求,而且还提供了直观、普适的表达能力.文中简要介绍了Bigraph的基本概念和现状,利用Bigraph理论对自适应软件体系结构进行了形式化规约,分析和验证了系统动态演化的性质,并探讨了Bigraph理论在自适应软件体系结构形式化方面的优势和拓展方向.     

一种基于Bigraph理论的软件演化过程模型研究

基于Bigraph理论对软件演化过程模型进行研究, 目的是能更好地对软件演化过程中相关动态变化进行建模。利用Bigraph理论和软件演化过程的思想, 首先提出了一个形式化的软件演化过程模型, 然后用扩展的Bigraph来描述软件演化过程模型的结构, 使用Bigraph反应系统来描述软件演化过程模型的动态变化, 最后对软件演化过程模型动态调整后的完整性进行了验证。     

基于赋时事件图的故障诊断

赋时事件图(TEG)是一类用于描述同步特性的重要的Petri网.本文提出并研究了基于赋时事件图的故障诊断问题.文中定义了两类系统故障类型:变迁失效(Invalidation)故障和变迁时间延迟(Time_lag)故障.基于事件图关联矩阵,通过研究变迁失效故障的可观测传播特性,引入了故障特征向量的概念.基于此,给出了失效故障的可诊断性的充分必要条件.对于时延故障,提出了一种基于变迁触发时间估计进行故障诊断的简单算法.并基于此算法,研究了时延故障的可诊断条件.     

基于数据服务的嵌套视图动态更新方法

数据服务屏蔽了数据访问的复杂性,并且支持用户以可视化方式定义装载异构数据源的嵌套视图.然而,当异构数据源输出的数据发生更新时,该更新需要通过数据服务逐层传播到顶层的嵌套视图,一类挑战性问题是,如何减少更新传播过程中的冗余计算,提高嵌套视图的数据新鲜度.为此文中提出了基于数据服务的嵌套视图动态更新方法,该方法利用指针为嵌套视图中的元组建立嵌套任意层次的数据服务的引用,同时给出了一种记录数据服务更新的日志以及在该日志上的嵌套视图增量更新算法.文中在原型系统中实现了该算法并且进行了实验分析,实验结果表明,该方法减少了70％的嵌套视图的更新时间,提高了60％的嵌套视图的数据新鲜度.     

UML类图层次化自动布图算法

UML类图能够有效地帮助软件工程师理解大规模的软件系统,而优化图元的空间布局可以增强类图的可读性和可理解性.由于类图中继承关系具有明显的层次特性,因此类图自动布局大多采用层次化的布图算法.此外,类图布局需要考虑相关的领域知识以及绘制准则,因而通用嵌套有向图层次化布局算法不能直接用于类图的绘制,它们必须加以扩展.但是,已有的类图层次化方法并没有考虑类图中图元的嵌套关系,这将导致自动布局方法不能处理类图中包与类、接口之间的包含关系.在考虑图绘制美学、UML类图绘制以及软件可视化等相关知识的基础上,选取了一组布     

4类图完美匹配数目的显式表达式

匹配计数理论是图论的核心内容之一,此问题有很强的物理学、计算机科学和化学背景;但是,一般图的完美匹配计数问题却是[NP-]难问题。用划分、求和、再嵌套递推的方法给出了4类图完美匹配数目的显式表达式;所给出的方法,可以计算出相同结构重复出现的许多图的所有完美匹配的数目。     

COM组件的备份和恢复引擎研究

本文在分析COM组件的结构及其基本特性基础上,提出了COM对象的创建及其接口访问中的Singleton模式,并从Abstract Factory模式的角度分析了利用类厂创建对象这一技术的合理性和必要性。叙述了C 语言实现COM对象与接口的两种方式：多继承和嵌套类。最后给出了存储管理软件中备份、恢复引擎的组件化实现的定义。     

随机Koch曲线岛及其分维测定的计算机模拟

获得的＂∧＂生长基础的树形结构和森林结构成为有限嵌套层次随机Ｋｏｃｈ曲线岛计算机模拟的基础。定义了３类随机Ｋｏｃｈ曲线岛，并分析了只有周长——面积法才可能得到第２类和第３类曲线岛的稳定分维值。给出了模拟３类曲线岛及其分维值测定的计算程序。从计算结果，明确了实际测定分维和统计维数时应如何选择小岛，所需测量的小岛对数以及分维和统计维数同嵌套层次的关系，３类曲线岛所对应的ｌｇＰ—ｌｇＡ回归直线的分布及其同嵌套层次的关系。     

A verification environment for bigraphs

We present the BigMC tool for bigraphical reactive systems that may be instantiated as a verification tool for any formalism or domain-specific modelling language encoded as a bigraphical reactive system. We introduce the syntax and use of BigMC, and exemplify its use with two small examples: a textbook “philosophers” example, and an example motivated by a ubiquitous computing application. We give a tractable heuristic with which to approximate interference between reaction rules, and prove this analysis to be safe. We provide a mechanism for state reachability checking of bigraphical reactive systems, based upon properties expressed in terms of matching, and describe a checking algorithm that makes use of the causation heuristic.     

How to delete categorically — Two pushout complement constructions

In category theory, most set-theoretic constructions-union, intersection, etc.-have direct categorical counterparts. But up to now, there is no direct construction of a deletion operation like the set-theoretic complement. In rule-based transformation systems, deletion of parts of a given object is one of the main tasks. In the double pushout approach to algebraic graph transformation, the construction of pushout complements is used in order to locally delete structures from graphs. But in general categories, even if they have pushouts, pushout complements do not necessarily exist or are unique. In this paper, two different constructions for pushout complements are given and compared. Both constructions are based on certain universal constructions in the sense of category theory. More specifically, one uses initial pushouts while the other one uses quasi-coproduct complements. These constructions are applied to examples in the categories of graphs and simple graphs.     

Local Bigraphs and Confluence: Two Conjectures: (Extended Abstract)

The notion of confluence is studied on the context of bigraphs. Confluence will be important in modelling real-world systems, both natural (as in biology) and artificial (as in pervasive computing). The paper uses bigraphs in which names have multiple locality; this enables a formulation of the lambda calculus with explicit substitutions. The paper reports work in progress, seeking conditions on a bigraphical reactive system that are sufficient to ensure confluence; the conditions must deal with the way that bigraphical redexes can be intricately intertwined. The conditions should also be satisfied by the lambda calculus. After discussion of these issues, two conjectures are put forward.     

Matching of Bigraphs

We analyze the matching problem for bigraphs. In particular, we present a sound and complete inductive characterization of matching of binding bigraphs. Our results pave the way for a provably correct matching algorithm, as needed for an implementation of bigraphical reactive systems.     

An inductive characterization of matching in binding bigraphs

We analyze the matching problem for bigraphs. In particular, we present a sound and complete inductive characterization of matching in bigraphs with binding. Our results yield a specification for a provably correct matching algorithm, as needed by our prototype tool implementing bigraphical reactive systems.     

A bigraphical model for specifying cloud-based elastic systems and their behaviour

The few recent years have witnessed the appearance of a new kind of self-adaptive systems called cloud based-elastic systems. These systems are particularly appealing for their ability to maintain a decent quality of service and reduce a system’s operating cost at the same time. They achieve this by dynamically adjusting resources allocation in terms of elasticity. Meanwhile, complexity of structural and behavioural aspects related to cloud-based elastic systems increase the difficulty of designing and developing such systems. In this paper, we address this challenge by proposing a formal approach based on bigraphical reactive systems for modelling both structural and behavioural aspects of cloud-based elastic systems. In particular, we represent their behaviour in terms of client/application interactions and elasticity methods at different levels using bigraphical reaction rules. The feasibility of the proposed approach is illustrated through a motivating example running on the top of an Amazon Elastic Compute Cloud (EC2) infrastructure.     

Modelling IEEE 802.11 CSMA/CA RTS/CTS with stochastic bigraphs with sharing

Stochastic bigraphical reactive systems (SBRS) is a recent formalism for modelling systems that evolve in time and space. However, the underlying spatial model is based on sets of trees and thus cannot represent spatial locations that are shared among several entities in a simple or intuitive way. We adopt an extension of the formalism, SBRS with sharing, in which the topology is modelled by a directed acyclic graph structure. We give an overview of SBRS with sharing, we extend it with rule priorities, and then use it to develop a model of the 802.11 CSMA/CA RTS/CTS protocol with exponential backoff, for an arbitrary network topology with possibly overlapping signals. The model uses sharing to model overlapping connectedness areas, instantaneous prioritised rules for deterministic computations, and stochastic rules with exponential reaction rates to model constant and uniformly distributed timeouts and constant transmission times. Equivalence classes of model states modulo instantaneous reactions yield states in a CTMC that can be analysed using the model checker PRISM. We illustrate the model on a simple example wireless network with three overlapping signals and we present some example quantitative properties.     

Pure bigraphs: Structure and dynamics

Bigraphs are graphs whose nodes may be nested, representing locality, independently of the edges connecting them. They may be equipped with reaction rules, forming a bigraphical reactive system (Brs) in which bigraphs can reconfigure themselves. Following an earlier paper describing link graphs, a constituent of bigraphs, this paper is a devoted to pure bigraphs, which in turn underlie various more refined forms. Elsewhere it is shown that behavioural analysis for Petri nets, π-calculus and mobile ambients can all be recovered in the uniform framework of bigraphs. The paper first develops the dynamic theory of an abstract structure, a wide reactive system (Wrs), of which a Brs is an instance. In this context, labelled transitions are defined in such a way that the induced bisimilarity is a congruence. This work is then specialised to Brss, whose graphical structure allows many refinements of the theory. The latter part of the paper emphasizes bigraphical theory that is relevant to the treatment of dynamics via labelled transitions. As a running example, the theory is applied to finite pure CCS, whose resulting transition system and bisimilarity are analysed in detail. The paper also mentions briefly the use of bigraphs to model pervasive computing and biological systems.     

Parallelism and concurrency of graph manipulations

Graph manipulations are formalized as graph derivations within the framework of graph grammar theory. In this paper we generalize recently published ‘Church–Rosser’ and ‘Parallelism’ Theorems for graph derivations. Given a ‘sequential independent’ sequence of graph derivations G?H ?X the Parallelism Theorem states that there is also a sequential independent sequence via the same productions applied in reverse order, and a direct derivation G ? X via the corresponding parallel production.In our ‘Concurrency Theorem’, the main result of this paper, the assumption of sequential independence is dropped. For each sequence of productions together with dependence relations (allowing later rules to depend on the effects of earlier productions), we construct a single ‘concurrent production’. The Concurrency Theorem states that each graph derivation sequence via the given sequence of productions, which respects all the dependence relations, can be performed in a single direct derivation via the ‘concurrent production’. Moreover this assignment becomes a bijective correspondence.This Concurrency Theorem is formulated and proved in the framework of the algebraic theory of graph grammars using new pushout and pullback lemmas for the 3- and 4- dimensional cubes. As corollaries we obtain the Parallelism Theorem and a theorem reducing the strong to the weak Church–Rosser-property of graph derivations. Applications of these results to various fields in computer science especially to data base systems, are sketched in the introduction.     

Event-driven grammars: relating abstract and concrete levels of visual languages

In this work we introduce event-driven grammars, a kind of graph grammars that are especially suited for visual modelling environments generated by meta-modelling. Rules in these grammars may be triggered by user actions (such as creating, editing or connecting elements) and in their turn may trigger other user-interface events. Their combination with triple graph transformation systems allows constructing and checking the consistency of the abstract syntax graph while the user is building the concrete syntax model, as well as managing the layout of the concrete syntax representation. As an example of these concepts, we show the definition of a modelling environment for UML sequence diagrams. A discussion is also presented of methodological aspects for the generation of environments for visual languages with multiple views, its connection with triple graph grammars, the formalization of the latter in the double pushout approach and its extension with an inheritance concept. This is a revised and extended version of a paper presented at the ICGT’04 conference, see [21].