带口令的安全盒子环境演算

带口令的安全盒子环境演算是对原有的移动环境演算的改进，避免了移动环境演算中open操作所带来的干扰，加强了环境对其自身边界的控制能力，实现了对环境的回收。文中给出了SBAP的语法和语义定义，用SBAP对Pi-演算中的匹配算子进行了改写，并对电子邮件系统进行了描述和仿真。     

Applying a testing approach to the Calculus of Fair Ambients

We apply a testing approach to the Calculus of Fair Ambients and investigate the resulting testing equivalence. We prove that variant conditions on its definition do not change its discriminating power, and it is congruent on finite processes. On a proper subset of processes, open bisimilarity is strictly included in testing equivalence. It is also proved that the translation from Pi-Calculus to Fair Ambients is fully abstract with respect to testing equivalence.     

Probabilistic Mobile Ambients

The calculus of Mobile Ambients has been introduced for expressing mobility and mobile computation. In this paper we present a probabilistic version of Mobile Ambients by augmenting the syntax of the original Ambient Calculus with a (guarded) probabilistic choice operator. To allow for the representation of both the probabilistic behaviour introduced through the new probabilistic choice operator and the nondeterminism present in the original Ambient Calculus we use probabilistic automata as the underpinning semantic model. The Ambient logic is a logic for Mobile Ambients that contains a novel treatment of both locations and hidden names. For specifying properties of Probabilistic Mobile Ambients, we extend this logic to specify probabilistic behaviour. In addition, to show the utility of our approach we present an example of a virus infecting a network.     

情境感知研究现状

移动互联网的迅速普及为情境感知的发展奠定了技术基础,情境感知领域的相关研究逐渐成为了计算机领域里的一个热点,文章将从情境感知的起源开始,介绍情境感知的定义及相关研究方向,梳理出目前情境感知研究的脉络。     

移动进程的蛰伏性及空间逻辑

界程逻辑(Ambient Logic)定义了一个示范性的空间逻辑来描述移动界程演算中移动进程的空间性质.然而在某些移动计算系统中,界程逻辑对移动进程空间性质的描述粒度是不够的.分析移动进程的蛰伏性质,用蛰伏和活跃来描述移动进程的存在状态,由此给出一种界程逻辑的扩展,称为状态空间逻辑.该逻辑能够描述移动进程的蛰伏性,进而更细粒度地刻画进程空间性质,且其在移动界程演算上的满足性是可判定的.同时还给出了状态空间逻辑公式的形式解释和蛰伏空间公式的逻辑推导规则.     

移动界程模型检测

首次将嵌套谓词等式系应用到带递归的谓词界程逻辑模型检测中,提出了第1个时间复杂性与逻辑公式的交错嵌套深度呈指数关系的局部模型检测算法,这也是目前已知的第2个带递归的谓词界程逻辑模型检测算法.所做的工作有：①讨论了谓词界程逻辑公式与嵌套谓词等式系间语义的等价性,给出了谓词界程逻辑公式转换成嵌套谓词等式系的方法;②讨论了谓词界程逻辑模型检测问题,给出了具体算法,并分析了算法的复杂性.     

Context-aware communication

Describes the Mercury system, whereby a user of an electronic message service receives messages on a device and in a format appropriate to his context (travelling, in a meeting, etc.); and ConChat, whereby besides transmitting his message he automatically transmits contextual information such as his location, the number and identities of other people in the room, the room's ambient temperature, lighting, and sound, other applications and devices running in the room, his mood, his personal status (on the 'phone, out to lunch, etc), and any activity in the room.     

Typed Mobile Ambients in Maude

Maude has revealed itself as a powerful tool for implementing different kinds of semantics so that quick prototypes are available for trying examples and proving properties. In this paper we show how to define in Maude two semantics for Cardelli and Gordon's Ambient Calculus. The first one is the operational (reduction) semantics which requires the definition of Maude strategies in order to avoid infinite loops. The second one is a type system defined by Cardelli and Gordon to avoid communication errors. The correctness of that system was not formally proved. We enrich the operational semantics with error rules and prove that well-typed processes do not produce such errors. The type system is highly non-deterministic. We show here one possible way of implementing such non-determinism in the rules.     

On abstract interpretation of Mobile Ambients

We introduce an abstract interpretation framework for Mobile Ambients, based on a new semantics called normal semantics. Then, we derive within this setting two analyses computing a safe approximation of the run-time topological structure of processes. Such a static information can be successfully used to establish interesting security properties.     

Barbs and Congruences for Safe Mobile Ambients

The Ambient Calculus offers many ways in which processes can interact and be observed. In the context of Levi and Sangiorgi's Safe Mobile Ambients (SA), the extra co-capabilities required for interaction complicate the fundamental observations. We show that different formulations of barbs lead to the same barbed congruence. We prove this by following Honda and Yoshida's approach for the π-calculus by defining the insensitive terms of SA.     

Information Flow Security for Boxed Ambients

We study the problem of secure information flow for Boxed Ambients in terms of non-interference. We develop a sound type system that provides static guarantees of absence of unwanted flow of information for well typed processes. Non-interference is stated, and proved, in terms of a typed notion of contextual equivalence for Boxed Ambients akin to the corresponding equivalence defined for Mobile Ambients.     

Translating Mobile Ambients into P Systems

We present a translation of the mobile ambients without communication and replication into P systems with mobile membranes. We introduce a set of developmental rules over membranes, and describe the correspondence between the behaviour of an ambient and the evolution of its translated membrane system. We give an operational correspondence result between the mobile ambients and P systems.     

On the Expressiveness of Pure Mobile Ambients

We consider the Pure Ambient Calculus, which is Cardelli and Gordon's Ambient Calculus (or more precisely its safe version by Levi and Sangiorgi) restricted to its mobility primitives, and we focus on its expressive power. Since it has no form of communication or substitution, we show how these notions can be simulated by mobility and modifications in the hierarchical structure of ambients. As an example, we give an encoding of the synchronous π-calculus into pure ambients and we state an operational correspondence result. In order to simplify the proof and give an intuitive understanding of the encoding, we design an intermediate language: the π-Calculus with Explicit Substitutions and Channels, which is a syntactic extension of the π-calculus with a specific operational semantics.     

The Displacement Calculus

If all dependent expressions were adjacent some variety of immediate constituent analysis would suffice for grammar, but syntactic and semantic mismatches are characteristic of natural language; indeed this is a, or the, central problem in grammar. Logical categorial grammar reduces grammar to logic: an expression is well-formed if and only if an associated sequent is a theorem of a categorial logic. The paradigmatic categorial logic is the Lambek calculus, but being a logic of concatenation the Lambek calculus can only capture discontinuous dependencies when they are peripheral. In this paper we present the displacement calculus, which is a logic of intercalation as well as concatenation and which subsumes the Lambek calculus. On the empirical side, we apply the new calculus to discontinuous idioms, quantification, VP ellipsis, medial extraction, pied-piping, appositive relativisation, parentheticals, gapping, comparative subdeletion, cross-serial dependencies, reflexivization, anaphora, dative alternation, and particle shift. On the technical side, we prove that the calculus enjoys Cut-elimination.     

一种基于事件的情境感知框架

为更好地满足用户的个性化需求、支持情境感知服务,提出一种基于事件的情境感知框架。该框架包括传感器层、事件总线和应用服务层,采用事件触发的方式调用应用服务与用户交互,并建立基于规则的事件过滤机制,对无效事件进行屏蔽。应用结果表明,该框架可提高系统的感知性能和重用性。     

Context-aware counter abstraction

The trend towards multi-core computing has made concurrent software an important target of computer-aided verification. Unfortunately, Model Checkers for such software suffer tremendously from combinatorial state space explosion. We show how to apply counter abstraction to real-world concurrent programs to factor out redundancy due to thread replication. The traditional global state representation as a vector of local states is replaced by a vector of thread counters, one per local state. In practice, straightforward implementations of this idea are unfavorably sensitive to the number of local states. We present a novel symbolic exploration algorithm that avoids this problem by carefully scheduling which counters to track at any moment during the search. We have carried out experiments on Boolean programs, an abstraction promoted by the success of the Slam project. The experiments give evidence of the applicability of our method to realistic programs, and of the often huge savings obtained in comparison to plain symbolic state space exploration, and to exploration optimized by partial-order methods. To our knowledge, our tool marks the first implementation of counter abstraction to programs with non-trivial local state spaces, resulting in a Model Checker for concurrent Boolean programs that promises true scalability.     

Flow-sensitive Leakage Analysis in Mobile Ambients

In this paper, we present a refinement of a Control Flow Analysis aimed at studying information flow security in the the calculus of Mobile Ambients. The improvements are achieved by making the analysis be flow-sensitive: the analysis is able to keep track of temporal dependencies of capabilities application when computing a safe approximation of the run-time topology of Mobile Ambient processes.     

On the Expressiveness of Pure Mobile Ambients

We consider the Pure Ambient Calculus, which is Cardelli and Gordon's Ambient Calculus (or more precisely its safe version by Levi and Sangiorgi) restricted to its mobility primitives, and we focus on its expressive power. Since it has no form of communication or substitution, we show how these notions can be simulated by mobility and modifications in the hierarchical structure of ambients. As an example, we give an encoding of the synchronous π-calculus into pure ambients and we state an operational correspondence result. In order to simplify the proof and give an intuitive understanding of the encoding, we design an intermediate language: the π-Calculus with Explicit Substitutions and Channels, which is a syntactic extension of the π-calculus with a specific operational semantics.     

A Calculus for Cryptographic Protocols: The Spi Calculus

We introduce the spi calculus, an extension of the pi calculus designed for describing and analyzing cryptographic protocols. We show how to use the spi calculus, particularly for studying authentication protocols. The pi calculus (without extension) suffices for some abstract protocols; the spi calculus enables us to consider cryptographic issues in more detail. We represent protocols as processes in the spi calculus and state their security properties in terms of coarse-grained notions of protocol equivalence.