Interface automata are one of the prominent formalisms for specifying interface behaviors of componentbased systems. However, only one-to-one communication is allowed in the composition of interface automata. This paper presents multicast interface automata which generalize the classic interface automata and accommodate multicast communication mechanism. The multicast interface automata endorse both bottom-up and top-down design methodologies. Theoretical results on compatibility and refinement are established for incremental design and independent implementability.

Architectural modeling and behavior analysis are two important concerns in the software development. They are often implemented separately, and specified by their own supporting notations. Architectural modeling helps to guarantee the system design to satisfy the requirement, and behavior analysis can ensure the interaction correctness. To improve the trustworthiness, methods trying to combine architectural modeling and behavior analysis notations together have been proposed, e.g., establishing a one-way mapping relation. However, the one-way relation cannot ensure updating one notation specifications in accordance with the other one, which results in inconsistency problems. In this paper, we present an approach to integrating behavior analysis into architectural modeling, which establishes the interoperability between architectural modeling notation and behavior analysis notation by a bidirectional mapping. The architecture is specified by the modeling language, architecture analysis and design language (AADL), and then mapped to behavior analysis notation, Darwin/FSP (finite state process) through the bidirectional transformation. The bidirectional transformation provides traceability, which makes behavior analysis result provided by a model checker can be traced and reflected back to the original AADL specifications. In this way, the behavior analysis is integrated into architectural modeling. The feasibility of our approach is shown by a control system example.

Memory leaks are a common type of defect that is hard to detect manually. Existing memory leak detection tools suffer from lack of precise interprocedural analysis and path-sensitivity. To address this problem, we present a static interprocedural analysis algorithm, that performs fully pathsensitive analysis and captures precise function behaviors, to detect memory leak in C programs. The proposed algorithm uses path-sensitive symbolic execution to track memory actions in different program paths guarded by path conditions. A novel analysis model called memory state transition graph (MSTG) is proposed to describe the tracking process and its results. In order to do interprocedural analysis, the proposed algorithm generates a summary for each procedure from MSTG and applies the summary at the procedure’s call sites. A prototype tool called Melton is implemented for this procedure. Melton was applied to five open source C programs and 41 leaks were found. More than 90% of these leaks were subsequently confirmed and fixed by their maintainers. For comparison with other tools, Melton was also applied to some programs in standard performance evaluation corporation (SPEC) CPU 2000 benchmark suite and detected more leaks than the state of the art approaches.

In general the problem of verifying whether a structured business process is compliant with a given set of regulations is NP-hard. The present paper focuses on identifying a tractable subset of this problem, namely verifying whether a structured business process is compliant with a single global obligation. Global obligations are those whose validity spans for the entire execution of a business process. We identify two types of obligations: achievement and maintenance.

In the present paper we firstly define an abstract framework capable to model the problem and secondly we define procedures and algorithms to deal with the compliance problem of checking the compliance of a structured business process with respect to a single global obligation. We show that the algorithms proposed in the paper run in polynomial time.

Coalition logic (CL) is one of the most influential logical formalisms for strategic abilities of multi-agent systems. CL can specify what a group of agents can achieve through choices of their actions, denoted by [C]? to state that a group of agents C can have a strategy to bring about ? by collective actions, no matter what the other agents do. However, CL lacks the temporal dimension and thus can not capture the dynamic aspects of a system. Therefore, CL can not formalize the evolvement of rational mental attitudes of the agents such as knowledge, which has been shown to be very useful in specifications and verifications of distributed systems, and has received substantial amount of studies. In this paper, we introduce coalition logic of temporal knowledge (CLTK), by incorporating a temporal logic of knowledge (Halpern and Vardi’s logic of CKL_n) into CL to equip CL with the power to formalize how agents’ knowledge (individual or group knowledge) evolves over the time by coalitional forces and the temporal properties of strategic abilities as well. Furthermore, we provide an axiomatic system for CLTK and prove that it is sound and complete, along with the complexity of the satisfiability problem which is shown to be EXPTIME-complete.

This paper presents an approach to build a communication behavioural semantic model for heterogeneous distributed systems that include synchronous and asynchronous communications. Since each node of such system has its own physical clock, it brings the challenges of correctly specifying the system time constraints. Based on the logical clocks proposed by Lamport, and CCSL proposed by Aoste team in INRIA, as well as pNets from Oasis team in INRIA, we develop timed-pNets to model communication behaviours for distributed systems. Timed-pNets are tree style hierarchical structures. Each node is associated with a timed specification which consists of a set of logical clocks and some relations on clocks. The leaves are represented by timed-pLTSs. Non-leaf nodes (called timed-pNets nodes) are synchronisation devices that synchronize the behaviours of subnets (these subnets can be leaves or non-leaf nodes). Both timed-pLTSs and timed-pNets nodes can be translated to timed specifications. All these notions and methods are illustrated on a simple use-case of car insertion from the area of intelligent transportation systems (ITS). In the end the TimeSquare tool is used to simulate and check the validity of our model.

NoSQL databases are famed for the characteristics of high scalability, high availability, and high faulttolerance. So NoSQL databases are used in a lot of applications. The data partitioning strategy and fragment allocation strategy directly affect NoSQL database systems’ performance. The data partition strategy of large, global databases is performed by horizontally, vertically partitioning or combination of both. In the general way the system scatters the related fragments as possible to improve operations’ parallel degree. But the operations are usually not very complicated in some applications, and an operation may access to more than one fragment. At the same time, those fragments which have to be accessed by an operation may interact with each other. The general allocation strategies will increase system’s communication cost during operations execution over sites. In order to improve those applications’ performance and enable NoSQL database systems to work efficiently, these applications’ fragments have to be allocated in a reasonable way that can reduce the communication cost i.e., to minimize the total volume of data transmitted during operations execution over sites. A strategy of clustering fragments based on hypergraph is proposed, which can cluster fragments which were accessed together in most operations to the same cluster. The method uses a weighted hypergraph to represent the fragments’ access pattern of operations. A hypergraph partitioning algorithm is used to cluster fragments in our strategy. This method can reduce the amount of sites that an operation has to span. So it can reduce the communication cost over sites. Experimental results confirm that the proposed technique will effectively contribute in solving fragments re-allocation problem in a specific application environment of NoSQL database system.

MapReduce is a popular parallel data-processing system, and task scheduling is one of the kernel techniques in MapReduce. In many applications, users have requirements that their MapReduce jobs should be completed before specific deadlines. Hence, in this paper, a novel scheduling algorithm based on the most effective sequence (SAMES) is proposed for deadline-constraint jobs in MapReduce. First, according to the characteristics of MapReduce, we propose a novel sequence-based execution strategy for MapReduce jobs and a new concept, the effective sequence (ES). Then, we design some efficient approaches for finding ESes and choose the most effective sequence (MES) for job execution. We also propose methods for MES-updates and exception handling. Finally, we verify the effectiveness of SAMES through experiments. The experimental results show that SAMES is an efficient scheduling algorithm for deadline-constraint jobs in MapReduce.

As service demands rise and expand single-server user authentication has become unable to satisfy actual application demand. At the same time identity and password based authentication schemes are no longer adequate because of the insecurity of user identity and password. As a result biometric user authentication has emerged as a more reliable and attractive method. However, existing biometric authentication schemes are vulnerable to some common attacks and provide no security proof, some of these biometric schemes are also either inefficient or lack sufficient concern for privacy. In this paper, we propose an anonymous and efficient remote biometric user authentication scheme for a multi-server architecture with provable security. Through theoretical mathematic deduction, simulation implementation, and comparison with related work, we demonstrate that our approach can remove the aforementioned weaknesses and is well suited for a multiserver environment.

Cross-domain password-based authenticated key exchange (PAKE) protocols have been studied for many years. However, these protocols are mainly focusing on multi-participant within a single domain in an open network environment. This paper proposes a novel approach for designing a cross-domain group PAKE protocol, that primarily handles with the setting of multi-participant in the multidomain. Moreover, our protocol is proved secure against active adversary in the Real-or-Random (ROR) model. In our protocol, no interaction occurs between any two domain authentication servers. They are regarded as ephemeral certificate authorities (CAs) to certify key materials that participants might subsequently use to exchange and agree on group session key. We further justify the computational complexity and measure the average computation time of our protocol. To the best of our knowledge, this is the first work to analyze and discuss a provably secure multi-participant cross-domain group PAKE protocol.