CRDT协议的TLA+描述与验证

无冲突复制数据类型(conflict-free replicated data types,简称CRDT)是一种封装了冲突消解策略的分布式复制数据类型,它能够保证分布式系统中副本节点间的强最终一致性,即执行了相同更新操作的副本节点具有相同的状态.CRDT协议设计精巧,不易保证其正确性.旨在采用模型检验技术验证一系列CRDT协议的正确性.具体而言,构建了一个可复用的CRDT协议描述与验证框架,包括网络通信层、协议接口层、具体协议层与规约层.网络通信层描述副本节点之间的通信模型,实现了多种类型的通信网络.协议接口层为已知的CRDT协议(分为基于操作的协议与基于状态的协议)提供了统一的接口.在具体协议层,用户可以根据协议的需求选用合适的底层通信网络.规约层则描述了所有CRDT协议都需要满足的强最终一致性与最终可见性(所有的更新操作最终都会被所有的副本节点接收并处理).使用TLA+形式化规约语言实现了该框架,然后以Add-Wins Set复制数据类型为例,展示了如何使用框架描述具体协议,并使用TLC模型检验工具来验证协议的正确性.     

Specifying and verifying requirements of real-time systems

An approach to specification of requirements and verification of design for real-time systems is presented. A system is defined by a conventional mathematical model for a dynamic system where application specific states denote functions of real time. Specifications are formulas in duration calculus, a real-time interval logic, where predicates define durations of states. Requirements define safety and functionality constraints on the system or a component. A top-level design is given by a control law: a predicate that defines an automation controlling the transition between phases of operation. Each phase maintains certain relations among the system states; this is analogous to the control functions known from conventional control theory. The top-level design is decomposed into an architecture for a distributed system with specifications for sensor, actuator, and program components. Programs control the distributed computation through synchronous events. Sensors and actuators relate events with system states. Verification is a deduction showing that a design implies requirements     

Specifying and enforcing access control policies for XML document sources

The Web is becoming the main information dissemination means in private and public organizations. As a consequence, several applications at both internet and intranet level need mechanisms to support a selective access to data available over the Web. In this context, developing an access control model, and related mechanisms, in terms of XML (eXtensible Markup Language) is an important step, because XML is increasingly used as the language for representing information exchanged over the Web. In this paper, we propose access control policies and an associated model for XML documents, addressing peculiar protection requirements posed by XML. A first requirement is that varying protection granularity levels should be supported to guarantee a differentiated protection of document contents. A second requirement arises from the fact that XML documents do not always conform to a predefined document type. To cope with these requirements, the proposed model supports varying protection granularity levels, ranging from a set of documents, to a single document or specific document portion(s). Moreover, it allows the Security Administrator to choose different policies for documents not covered or only partially covered by the existing access control policies for document types. An access control mechanism for the enforcement of the proposed model is finally described. This revised version was published online in August 2006 with corrections to the Cover Date.     

Specifying and verifying a broadcast and a multicast snooping cachecoherence protocol

We develop a specification methodology that documents and specifies a cache coherence protocol in eight tables: the states, events, actions, and transitions of the cache and memory controllers. We then use this methodology to specify a detailed, modern three-state broadcast snooping protocol with an unordered data network and an ordered address network that allows arbitrary skew. We also present a detailed specification of a new protocol called multicast snooping (Bilir et al., 1999) and, in doing so, we better illustrate the utility of the table-based specification methodology. Finally, we demonstrate a technique for verification of the multicast snooping protocol, through the sketch of a manual proof that the specification satisfies a sequentially consistent memory model     

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.     

Specifying and enforcing application-level Web security policies

Application-level Web security refers to vulnerabilities inherent in the code of a Web-application itself (irrespective of the technologies in which it is implemented or the security of the Web-server/back-end database on which it is built). In the last few months, application-level vulnerabilities have been exploited with serious consequences: Hackers have tricked e-commerce sites into shipping goods for no charge, usernames and passwords have been harvested, and confidential information (such as addresses and credit-card numbers) has been leaked. We investigate new tools and techniques which address the problem of application-level Web security. We 1) describe a scalable structuring mechanism facilitating the abstraction of security policies from large Web-applications developed in heterogeneous multiplatform environments; 2) present a set of tools which assist programmers in developing secure applications which are resilient to a wide range of common attacks; and 3) report results and experience arising from our implementation of these techniques.     

Specifying and enforcing high-level semantic obligation policies

Obligation policies specify management actions that must be performed when a particular kind of event occurs and certain conditions are satisfied. Large scale distributed systems often produce event streams containing large volumes of low-level events. In many cases, these streams also contain multimedia data (consisting of text, audio or video). Hence, a key challenge is to allow policy writers to specify obligation policies based on high-level events, that may be derived after performing appropriate processing on raw, low-level events. In this paper, we propose a semantic obligation policy specification language called Eagle, which is based on patterns of high-level events, represented as RDF graph patterns. Our policy enforcement architecture uses a compiler that builds a workflow for producing a stream of events, which match the high-level event pattern specified in a policy. This workflow consists of a number of event sources and event processing components, which are described semantically. We present the policy language and enforcement architecture in this paper.     

使用控制授权模型的安全性研究*

在基于策略的模型中,研究了使用控制授权模型的安全特性,首先分析了在一般使用控制授权模型中安全问题的不确定性;然后在限定属性值范围和无生成策略的条件下,说明了安全问题的确定性;最后通过释放生成策略的限制,在非连通的属性生成图和包含生成父属性的属性更新图中,证明了安全问题的确定性.     

基于TLA＋的BRP协议规约及验证

BRP协议是为不可靠信道上传送大数据包文件设计的工业协议。该协议的正确性依赖于各部件实时方面的假设。本文主要阐述了使用时序规约语言TLA＋对BRP协议进行规约和验证的过程。首先通过自然语言非形式化地描述BRP协议的基本原理和需求，在此基础上建立了BRP的形式化模型，利用TLA＋先对不考虑实时要求的BRP进行规约，然后添加实时约束获得BRP完整的规约，最后使用模型检验器TLC验证BRP协议的各种性质。     

Specifying a safety-critical control system in Z

The paper presents a formal specification in the Z notation for a safety-critical control system. It describes a particular medical device but is quite generic and should be widely applicable. The specification emphasizes safety interlocking and other discontinuous features that are not considered in classical control theory. A method for calculating interlock conditions for particular operations from system safety assertions is proposed; it is similar to ordinary Z precondition calculation, but usually results in stronger preconditions. The specification is presented as a partially complete framework that can be edited and filled in with the specific features of a particular control system. Our system is large but the specification is concise. It is built up from components, subsystems, conditions and modes that are developed separately, but also accounts for behaviors that emerge at the system level. The specification illustrates several useful idioms of the Z notation, and demonstrates that an object-oriented specification style can be expressed in ordinary Z     

Specification and Verification of the Zab Protocol with TLA+

ZooKeeper Atomic Broadcast (Zab) is an atomic broadcast protocol specially designed for ZooKeeper, which supports additional crash recovery. This protocol actually has been widely adopted by famous Internet companies, but there are few studies on the correctness and credibility of the Zab protocol, and thus we utilize formal methods to study the correctness. In this paper, Zab, Paxos and Raft are all analyzed and compared to help better understand the Zab protocol. Then we model the Zab protocol with TLA+ and verify three properties abstracted from the specification by the model checker TLC, including two liveness properties and one safety property. The final experimental results can prove that the design of the protocol conforms to the original requirements. This paper makes up for the analysis of formal methods in the Zab protocol.

     

Specifying control and data in the design of educational software

When using the computer as a tool for learning, it is useful to distinguish between the contents and the realization aspects of an interactive session. We describe an approach which makes this distinction explicit to the author by viewing the programming process as one of giving independent specifications of: (a) data. i.e. what is to be learned, and (b) control, i.e. the particulars of the dialogue.A system. MEDICS, for training medical students in clinical decision making is presented as an illustration of the approach. We stress the importance of providing an interactive environment supporting powerful editing operations as the primary tool for the author. The paper specifically describes the MEDICS environment for construction of medical simulations and how control of execution is specified.     

Learning policies for battery usage optimization in electric vehicles

The high cost, limited capacity, and long recharge time of batteries pose a number of obstacles for the widespread adoption of electric vehicles. Multi-battery systems that combine a standard battery with supercapacitors are currently one of the most promising ways to increase battery lifespan and reduce operating costs. However, their performance crucially depends on how they are designed and operated. In this paper, we formalize the problem of optimizing real-time energy management of multi-battery systems as a stochastic planning problem, and we propose a novel solution based on a combination of optimization, machine learning and data-mining techniques. We evaluate the performance of our intelligent energy management system on various large datasets of commuter trips crowdsourced in the United States. We show that our policy significantly outperforms the leading algorithms that were previously proposed as part of an open algorithmic challenge. Further, we show how to extend our approach to an incremental learning setting, where the policy is capable of improving and adapting as new data is being collected over time.     

Specifying and validating structural constraints of analysis class models using OCL

Analysis modeling focuses on functional requirements and postpone implementation specific issues until subsequent design activities are undertaken. Based on the analysis models, the design activities are performed by refining and clarifying the analysis models. Thus, the quality of analysis models has a vast impact on the design models. Therefore, much effort should be taken to build correct analysis models.In this paper, we propose structural constraints that analysis class models of information systems should satisfy, and describe an OCL-based approach to validating the analysis class models against the constraints. In addition, through a case study with four medium-sized industrial information systems, we find that the proposed approach can help to identify deficiencies in analysis models.     

Engineering and verifying agent-oriented requirements augmented by business constraints with $${\mathcal{B}}$$-Tropos

We propose B{\mathcal{B}}-Tropos as a modeling framework to support agent-oriented systems engineering, from high-level requirements elicitation down to execution-level tasks. In particular, we show how B{\mathcal{B}}-Tropos extends the Tropos methodology by means of declarative business constraints, inspired by the ConDec graphical language. We demonstrate the functioning of B{\mathcal{B}}-Tropos using a running example inspired by a real-world industrial scenario, and we describe how B{\mathcal{B}}-Tropos models can be automatically formalized in computational logic, discussing formal properties of the resulting framework and its verification capabilities.     

Migration policies in dynamic island models

Dynamic island models are population-based algorithms for solving optimization problems, where the individuals of the population are distributed on islands. These subpopulations of individuals are processed by search algorithms on each island. In order to share information within this distributed search process, the individuals migrate from their initial island to another destination island at regular steps. In dynamic island models, the migration process evolves during the search according to the observed performance on the different islands. The purpose of this dynamic/adaptive management of the migrations is to send the individuals to the most promising islands, with regards to their current states. Therefore, our approach is related to the adaptive management of search operators in evolutionary algorithms. In this work, our main purpose is thus to precisely analyze dynamic migration policies. We propose a testing process that assigns gains to the algorithms applied on the islands in order to assess the adaptive ability of the migration policies, with regards to various scenarios. Instead of having one dynamic migration policy that is applied to the whole search process, as it has already been studied, we propose to associate a migration policy to each individual, which allows us to combine simultaneously different migration policies.

     

Distributed and minimal usage control

With more and more personal data being collected and stored by service providers, there is an increasing need to ensure that their usage is compliant with privacy regulations and user preferences. We consider the specific scenario where promised usage is specified as metric temporal logic policies, and these policies can be verified against the database usage logs. Given the vast amount of data being collected, scalability is very important. In this work, we show how such usage monitoring can be performed in a distributed fashion for an expressive subset of policies. Experimental results are given for a real-life use case to show the genericness and scalability of the results.     

Comments on `A method for verifying sector conditions in nonlineardiscrete-time control systems'

The commenters note that the results obtained by Y. Mutoh and P.N. Nikiforuk (ibid., vol.37, p.1505-9, (1992)) can also be derived from the frequency domain stability criteria with less computational effort, and that the stability conditions can considerably be relaxed     

BlockU: Extended usage control in and for Blockchain

An electronic business transaction among untrusted bodies without consulting a mutually trusted party has remained widely accepted problem. Blockchain resolves this problem by introducing peer-to-peer network with a consensus algorithm and trusted ledger. Blockchain originally introduced for cryptocurrency that came with proof-of-work consensus algorithm. Due to some performance issues, scientists brought concept of permissioned Blockchain. Hyperledger Fabric is a permissioned Blockchain targeting business-oriented problems for industry. It is designed for efficient transaction execution over Blockchain with pluggable consensus model; however, there is limitation of rapid application development. Hyperledger introduced a new layer called Hyperledger Composer on top of the Fabric layer, which provides an abstract layer to model the business application readily and quickly. Composer provides a smart contract to extend the functionality and flexibility of Fabric layer and provides a way of communication with other systems to meet business requirements. Hyperledger Composer uses role-based access control (RBAC) model to secure access to its valuable assets. However, RBAC is not enough because many business deals require continuous assets monitoring. Our proposed model, BlockU, covers all possible access control models required by a business. BlockU can monitor assets continuously during transactions and updates attributes accordingly. Moreover, we incorporate hooks in Hyperledger Composer to implement extended permission model that provides extensive permission management capability on an asset. Subsequently, our proposed enhanced access control model is implemented with a minimal change to existing Composer code base and is backward compatible with the current security mechanism.