Research And Application Of Bigraphs Theory

Since information technology pervades our lives and information space is merging into physical space, informatics is transforming our environment. In the meanwhile, the dependency upon informatics will be to the nth degree in future and the need for this science and its mathematical foundations becomes more and more important. How to provide a model of computation on a large scale and complicated system such as Internet and the ubiquitous computing, moreover, it not only can analysis systems that already exist, but also it can guide the specification, design and programming of these systems and guide future adaptation of them in order that systems do not deteriorate when these adaptations are implemented.In addition, existing process calculus have made great progress with interconnected concurrent processes, with processes having mobile connectivity and with processes hav-ing notions of spatial location and mobility. Although there is some agreement among all these approaches especially in their basic notions and in their theories,a uniform of them is absent and then there is no settled way to combine various kinds of mobility. How to found a meta model for process calculi is a great challenge.Bigraphs theory, due to Robin Milner and coworkers, responds to the twin chal-lenges from application and existing process theory. It is a formal theory based on graphical model that focuses simultaneously on two aspects of mobile distributed sys-tems:mobile connectivity and mobile locality. As such, the theory is more general than traditional calculi for mobile processes. In order to better utilize bigraphs theory as meta model of process calculi and as an abstract machine of ubiquitous computing, many researchers propose some variants of bigraphs model. In this thesis, considering the nesting relationship among controls in place graph and type matching of points in link graph,we present an extended bigraphical model called typing bigraphs and then discuss its applications. The contributions of this dissertation include:1.Typing bigraph which is a pair of a controls nesting place graph denoted by BGsortP and a points matching linking graph denoted by BGsortL is proposed.For controls nesting place graphs, we define controls nesting place graphs based on an index category of controls Scat(Κ). Some characters especially the construction of relative pushout and consistent conditions of idem pushout in controls nesting place graphs are presented, furthermore ,proofs of corresponding propositions and theorem are glven.●For points matching linking graphs, we assign type to points of linking graphs and give the matching discipline of the linking and then define points matching linking graphs formally. As the controls nesting place graphs, we discuss relative important characters also.●For typing bigraphs, besides comparing with correlative notions of pure bigraphs we illustrate those key definitions and propositions.2.As a meta model typing bigraphs can be applied to oriented-behavior software requirements description language so called BDL. This investigation brings forth the ability to characterize the calculi of requirements and can be as a foundation for research of software requirements underlying bigraphs theory.●In order to translate BDL into bigraphs effectively we refine it and define normal form and bisimilarity of BDLRef.●We define the sorting discipline both controls nesting and points matching of finite BDLRef in bigraphs. Both BehExfmap and Mmap are illuminated which translate finite BDLRef into BG-BDLRef, and then, bigraphical reactive systems and derived labeled transition systems are discussed also.●The behavior constant BehCons in BDLRef is treated by growth theory repre-senting recursive definition in bigraphs.3.To demonstrate the expressivity of typing bigraphs, we discuss its application for modeling context-aware systems in ubiquitous computing.●With typing bigraph setting, We define unfolding bigraphical reactive systems which performs calculation and then argue its some characters such as orthogonal and confluence. Based on this, a calculational BRS is the one which an unfolding BRS is em-bedded into a general BRS. We not only give the definition of calculational BRS formally but also provide guarantees about the interplay of unfolding and liberal reaction.●The approach of modeling context-aware systems is investigated by calculational bigraphical reactive systems, and then we compare our approach with Plato-graphical model which is other bigraphical model of context aware systems through modeling the classical example.