基于纳什均衡的智能合约缺陷检测

本文研究区块链智能合约的缺陷检测问题,即检测合约中是否存在部分合约方无论选择什么动作,均无法避免损失的状态.将智能合约问题转换成合约状态迁移图上的博弈策略选择问题,提出了基于纳什均衡理论的合约缺陷自动检测方法,以及为了提高检测效率,提出了针对合约状态变迁图和博弈策略形式的一系列化简方法.最后,实现了一个智能合约建模、分...     

Probabilistic contracts for component-based design

We define a framework of probabilistic contracts for constructing component-based embedded systems, based on the formalism of discrete-time Interactive Markov Chains. A contract specifies the assumptions a component makes on its context and the guarantees it provides. Probabilistic transitions represent allowed uncertainty in the component behavior, for instance, to model internal choice or reliability. Action transitions are used to model non-deterministic behavior and communication between components. An interaction model specifies how components interact with each other. We provide the ingredients for a component-based design flow, including (1) contract satisfaction and refinement, (2) parallel composition of contracts over disjoint, interacting components, and (3) conjunction of contracts describing different requirements over the same component. Compositional design is enabled by congruence of refinement.     

Design by Contract to Improve Software Vigilance

Design by contract is a lightweight technique for embedding elements of formal specification (such as invariants, pre and postconditions) into an object-oriented design. When contracts are made executable, they can play the role of embedded, online oracles. Executable contracts allow components to be responsive to erroneous states and, thus, may help in detecting and locating faults. In this paper, we define vigilance as the degree to which a program is able to detect an erroneous state at runtime. Diagnosability represents the effort needed to locate a fault once it has been detected. In order to estimate the benefit of using design by contract, we formalize both notions of vigilance and diagnosability as software quality measures. The main steps of measure elaboration are given, from informal definitions of the factors to be measured to the mathematical model of the measures. As is the standard in this domain, the parameters are then fixed through actual measures, based on a mutation analysis in our case. Several measures are presented that reveal and estimate the contribution of contracts to the overall quality of a system in terms of vigilance and diagnosability     

语义规则驱动的中国古代建筑造型

根据中国古代建筑具有完整的营造规则约束的特点，提出了一种语义规则驱动的快速建模方法．根据中国古代建筑的建造规范，从中提取出若干造型规则，并且参数化表示主要的建筑结构特征，利用它们来控制模型的生成．定义了模型的构造模块——组件，通过迭代解释造型规则来控制组件的变换和组合，从而构造出一系列的中国古代建筑模型．通过扩充纹理库，可以得到不同效果的建筑模型．     

Solutions to four open problems concerning controlled pure grammar systems

In this paper, we address several open problems concerning pure grammar systems (pGSs) and their controlled versions. More specifically, we prove the following four results. (I) Regular-controlled pGSs having a single component define the family of regular languages. (II) pGSs having two components controlled by infinite regular languages define the family of recursively enumerable languages. (III) Regular-controlled pGSs without any erasing rules define the family of regular languages not containing the empty string. (IV) pGSs define a proper subfamily of the family of regular languages.     

Contracts,Games, and Refinement

We consider the notion of a contract that governs the behavior of a collection of agents. In particular, we study the question of whether a group among these agents can achieve a given goal by following the contract. We show that this can be reduced to studying the existence of winning strategies in a two-person game. A notion of correctness and refinement is introduced for contracts and contracts are shown to form a lattice and a monoid with respect to the refinement ordering. We define a weakest precondition semantics for contracts that permits us to compute the initial states from which a group of agents has a winning strategy to reach their goal. This semantics generalizes the traditional predicate transformer semantics for program statements to contracts and games. Ordinary programs and interactive programs are special kinds of contracts.     

Build-level components

Reuse between software systems is often not optimal. An important reason is that while at the functional level well-known modularization principles are applied for structuring functionality in modules, this is not the case at the build level for structuring files in directories. This leads to a situation where files are entangled in directory hierarchies and build processes, making it hard to extract functionality and to make functionality suitable for reuse. Consequently, software may not come available for reuse at all, or only in rather large chunks of functionality, which may lead to extra software dependencies. In this paper, we propose to improve this situation by applying component-based software engineering (CBSE) principles to the build level. We discuss how existing software systems break CBSE principles, we introduce the notion of build-level components, and we define rules for developing such components. To make our techniques feasible, we define a reengineering process for semiautomatically transforming existing software systems into build-level components. Our techniques are demonstrated in two case studies where we decouple the source tree of Graphviz into 46 build-level components and analyze the source tree of Mozilla.     

一种高级智能合约转化方法及竞买合约设计与实现

智能合约是运行在区块链上的数字协议,智能合约的开发涉及计算机、金融、法律等多个领域,近年来高级智能合约语言已被提出用于解决不同领域人员阅读、交流与协同开发难的问题,然而上述语言与可执行智能合约语言之间仍缺少有效的转化方法.针对这一问题,本文设计了一种SPESC到目标程序语言(Solidity)的转化规则,并提出了一种包括高级智能合约层、智能合约层和机器代码执行层的三层智能合约系统框架.首先,转化规则给出了根据SPESC合约当事人定义生成目标语言当事人子合约、以及SPESC其余部分生成目标语言主体子合约之间的对应关系;其次,除程序框架与存储结构外,目标语言程序还包含当事人人员管理、程序时序控制、异常检测等机制,这些机制能辅助编程人员半自动化地编写智能合约程序;进而,通过两个实验验证了上述高级智能合约框架的易读性以及转换的正确性,第一个实验邀请了计算机与非计算机人员分组阅读Solidity和SPESC的智能合约并回答问卷,结果表明阅读SPESC的速度约为阅读Solidity两倍,准确率也更高.然后以竞买合约为实例,给出了根据上述转化规则从SPESC合约转化到可执行Solidity合约语言程序,并通过以太坊私链部署运行来验证转化过程的正确性.实例表明上述转化规则和系统框架可简化智能合约的编写、规范智能合约的程序结构、辅助编程人员验证代码的正确性.     

Verification and enforcement of access control policies

Access control mechanisms protect critical resources of systems from unauthorized access. In a policy-based management approach, administrators define user privileges as rules that determine the conditions and the extent of users’ access rights. As rules become more complex, analytical skills are required to identify conflicts and interactions within the rules that comprise a system policy—especially when rules are stateful and depend on event histories. Without adequate tool support such an analysis is error-prone and expensive. In consequence, many policy specifications are inconsistent or conflicting that render the system insecure. The security of the system, however, does not only depend on the correct specification of the security policy, but in a large part also on the correct interpretation of those rules by the system’s enforcement mechanism. In this paper, we show how policy rules can be formalized in Fusion Logic, a temporal logic for the specification of behavior of systems. A symbolic decision procedure for Fusion Logic based on Binary Decision Diagrams (BDDs) is provided and we introduce a novel technique for the construction of enforcement mechanisms of access control policy rules that uses a BDD encoded enforcement automaton based on input traces which reflect state changes in the system. We provide examples of verification of policy rules, such as absence of conflicts, and dynamic separation of duty and of the enforcement of policies using our prototype implementation (FLCheck) for which we detail the underlying theory.     

Semantic-based authorization architecture for Grid

There are a few issues that still need to be covered regarding security in the Grid area. One of them is authorization where there exist good solutions to define, manage and enforce authorization policies in Grid scenarios. However, these solutions usually do not provide Grid administrators with semantic-aware components closer to the particular Grid domain and easing different administration tasks such as conflict detection or resolution. This paper defines a proposal based on Semantic Web to define, manage and enforce security policies in a Grid scenario. These policies are defined by means of semantic-aware rules which help the administrator to create higher-level definitions with more expressiveness. These rules also permit performing added-value tasks such as conflict detection and resolution, which can be of interest in medium and large scale scenarios where different administrators define the authorization rules that should be followed before accessing a resource in the Grid. The proposed solution has been also tested providing some reasonable response times in the authorization decision process.     

Making components contract aware

Components have long promised to encapsulate data and programs into a box that operates predictably without requiring that users know the specifics of how it does so. Many advocates have predicted that components will bring about widespread software reuse, spawning a market for components usable with such mainstream software buses as the Common Object Request Broker Architecture (CORBA) and the Distributed Component Object Model (DCOM). In the Windows world, at least, this prediction is becoming a reality. Yet recent reports indicate mixed results when using and reusing components in mission-critical settings. Such results raise disturbing questions. How can you trust a component? What if the component behaves unexpectedly, either because it is faulty or simply because you misused it? Before we can trust a component in mission-critical applications, we must be able to determine, reliably and in advance, how it will behave. In this article the authors define a general model of sofware contracts and show how existing mechanisms could be used to turn traditional components into contract-aware ones     

European conflict rules concerning international online consumer contracts1

With the drawing up of—what finally became—the Regulation (EC) 44/2001 of the Council of 22 December 2000 on jurisdiction and the recognition and enforcement of judgements in civil and commercial matters, there had already been a fierce debate in Europe on whether special private international rules for online consumer contracts were necessary and desirable. Although it was decided in favour of special jurisdiction rules which expressly include international online consumer contracts, as for applicable law the discussion is still unsettled, with the prospect of a revised Rome Convention of 1980. This article argues that the European legislator should provide legal certainty with respect to the applicability of European conflict rules to international online consumer contracts in the sense that the scope of especially article 5 of the Rome Convention—and thus the protection it provides to consumers—should explicitly be extended to such contracts, and at the same time leaves room for online suppliers to explicitly restrict their online offer(s) to consumers in certain countries or to professionals in order to control the applicable law risk.     

一类具有时态约束的关联规则的知识发现问题

本文探讨了一类具有时态约束的关联规则的有关问题。首先,我们引入了时态型的定义以及相关的概念。接下来,我们给出了一种时态事件模型,用以描述基于时态型的不同属性的各种状态的事件,也定义了一类具有时态约束的关联规则,它能在诸如股票波动、天气预报、商品销售等领域提供短期的预测和决策。最后,我们给出了发现具有时态约束的关联规则算法的主要步骤。     

Specifying and verifying contract-driven service compositions using commitments and model checking

The paper proposes a novel model checking-based approach towards verifying the compliance of intelligent agent-based web services with contracts regulating their compositions specified in the Business Process Execution Language (BPEL). Unlike the existing approaches in the literature, the main contribution and impact of the introduced approach is the ability to verify intelligent and autonomous composite web services by capturing and describing in details both compliance and violation behaviors, how the system can distinguish between them, and how the system reacts and can be recovered after each violation. The approach encompasses three contributing parts, namely: 1) the marking process of an extended BPEL; 2) the transformation of the extended and marked BPEL to an automata model; and 3) the encoding of the resulting automata model into the Interpreted Systems Programming Language (ISPL), the input language of the MCMAS model checker for intelligent and autonomous multi-agent systems. In the first part, we extend BPEL that specifies the business process of the composition by creating custom activities called labels. We use those labels as means to represent the specifications and mark the points the developer aims to verify. A significant advantage of this labeling is the ability to highlight specific points in the design to be verified and to distinguish compliance behaviors from violations, which makes this verification focused and highly efficient. In the second part, we introduce new transformation rules to transform the extended and marked BPEL to an automata model. This transformation requires a prior modeling of agent-based web services composition using automata definitions. In the third part, we introduce algorithmic translation rules encoding the resulting automata model into ISPL. This translation makes model checking the behavior of our contract-driven compositions possible. A novel characteristic of the proposed approach is the automatic generation of the properties against which the system is verified from the composition’s implementation, which is technically challenging. The verification properties are expressed in the Computation Tree Logic of Commitments (CTLC). Technically, CTLC provides a powerful representation to formally model 1) interactions among multi-agent based web services and 2) compliance and violation behaviors within composite business contracts by making use of communicative commitment operators. CTLC also includes a fulfillment operator which helps formally check the compliance with business contracts and specify the system recovery. A detailed case study from expert and intelligent systems domain along with experimental results are also reported in the paper. Finally, the main impact and significance of the paper on expert and intelligent systems is the ability to use these systems safely since there is a way to verify if the intelligent components behave according to and in compliance with the underlying regulating contracts.     

基于分水岭算法的医学图像分割

本文采用分水岭算法对医学图像进行分割,针对医学图像的特点以及该算法存在的过分割问题,首先将原图像转换为形态梯度图像,并对形态梯度图像定义一组形态开闭滤波器进行处理,以获得较好的参考图像;然后采用基于连接像素的分水岭算法进行分割。为了获得整体目标,还定义了一个基于分割区域边界平均灰度及其面积的检验准则,并将其作为区域合并的根据。该方法应用于医学图像分割的结果表明,形态滤波器组的引入很好地防止了过分割,基于分割区域边界平均灰度及其面积的准则对分割区域进行合并是行之有效的。     

Automatically running experiments on checking multi-party contracts

Contracts play an important role in business management where relationships among different parties are dictated by legal rules. Electronic contracts have emerged mostly due to technological advances and electronic trading between companies and customers. New challenges have then arisen to guarantee reliability among the stakeholders in electronic negotiations. In this scenario, automatic verification of electronic contracts appeared as an imperative support, specially the conflict detection task of multi-party contracts. The problem of checking contracts has been largely addressed in the literature, but there are few, if any, methods and practical tools that can deal with multi-party contracts using a contract language with deontic and dynamic aspects as well as relativizations, over the same formalism. In this work we present an automatic checker for finding conflicts on multi-party contracts modeled by an extended contract language with deontic operators and relativizations. Moreover a well-known case study of sales contract is modeled and automatically verified by our tool. Further, we performed practical experiments in order to evaluate the efficiency of our method and the practical tool.

     

Component Contracts in Service-Oriented Architectures

For SOAs to reach their full potential, the basic interoperable framework must accommodate meaningful quality-of-service contracts. Work on both industry-specific standards and semantic Web services is still needed to fully meet that goal. At the core of service-oriented architectures (SOAs) are distributed software components provided or accessed by independent third parties. Because access is not limited to a specific organization, explicit component contracts and universally adopted standards must support third-party access. Although such contracts could cover any technical or business aspect of service interaction, the current focus is on quality-of-service (QoS) policies. From an SOA point of view, we must consider two separate aspects of the use of QoS policies: interoperability between components, which is the subject of the Web services specifications stack; and composition, which composition models, such as the service component architecture (SCA).     

混合关联规则及其挖掘算法

在项目集中引入了负项目，据此定义了关联规则的一种泛化模型——混合关联规则，分析了它的价值，引入了它的挖掘问题的形式描述，并定义了挖掘中的几个关键算法．     

Beyond contracts for concurrency

SCOOP is a concurrent programming language with a new semantics for contracts that applies equally well in concurrent and sequential contexts. SCOOP eliminates race conditions and atomicity violations by construction. However, it is still vulnerable to deadlocks. In this paper we describe how far contracts can take us in verifying interesting properties of concurrent systems using modular Hoare rules and show how theorem proving methods developed for sequential Eiffel can be extended to the concurrent case. However, some safety and liveness properties depend upon the environment and cannot be proved using the Hoare rules. To deal with such system properties, we outline a SCOOP Virtual Machine (SVM) as a fair transition system. The SVM makes it feasible to use model-checking and theorem proving methods for checking global temporal logic properties of SCOOP programs. The SVM uses the Hoare rules where applicable to reduce the number of steps in a computation. P. J. Brooke, R. F. Paige and Dong Jin Song This work was conducted under an NSERC Discovery grant.