Consistency is a significant indicator to measure the correctness of a software system in its lifecycle. It is inevitable to introduce inconsistencies between different software artifacts in the software development process. In practice, developers perform consistency checking to detect inconsistencies, and apply their corresponding repairs to restore consistencies. Even if all inconsistencies can be repaired, how to preserve consistencies in the subsequent evolution should be considered. Consistency management (consistency checking and consistency preservation) is a challenging task, especially in the multi-view model-driven software development process. Although there are some efforts to discuss consistency management, most of them lack the support of formal methods. Our work aims to provide a framework for formal consistency management, which may be used in the practical software development process. A formal model, called a Structure model, is first presented for specifying the overall model-based structure of the software system. Next, the definition of consistency is given based on consistency rules. We then investigate consistency preservation under the following two situations. One is that if the initial system is inconsistent, then the consistency can be restored through repairs. The other is that if the initial system is consistent, then the consistency can be maintained through update propagation. To demonstrate the effectiveness of our approach, we finally present a case study with a prototype tool.

The sample labeling is the basis for wireline logs-based automatic lithology identification (WLALI). Due to the paucity of core data, the expert-annotation accounts for most labeling workload. In the traditional workflow of WLALI, the samples for labeling are passively selected. The labeled samples thus fail to reflect the overall distribution and feature of whole data set, leading to the difficulty in training the prediction model with robust generalization performance. To solve this problem, a novel workflow of hybrid active and semi-supervised learning-based WLALI has been proposed. First, we alter the conventional labeling process to active selection mode by employing the approach of active learning. In such way the labeled samples are representative of whole data features. Second, we propose a novel active learning algorithm based on density difference of Gaussian probability (DDGP) to obtain a better performance of sample query. Third, the semi-supervised learning method is introduced to combine the active learning algorithm, attempting to minimize the involvement of hand-crafted labeling under the target performance. In the evaluation, the proposed workflow not only has achieved favorable result in the uppercase image dataset, but also the practical application shows great promise. When compared with the workflow of random sampling + semi-supervised learning that is similar to the traditional mode, the average F1-score of proposed workflow of DDGP + semi-supervised learning can increase by approximately 3.47%.

To guarantee the safety and security of a real-time mobile system such as an intelligent transportation system, it is necessary to model and analyze its behaviors prior to actual development. In particular, the mobile objects in such systems must be isolated from each other so that they do not collide with each other. Since isolation means two or more mobile objects must not be located in the same place at the same time, a scheduling policy is required to control and coordinate the movement of such objects. However, traditional scheduling theories are based on task scheduling which is coarse-grained and cannot be directly used for fine-grained isolation controls. In this article, we first propose a fine-grained event-based formal model called a time dependency structure and use it to model and analyze real-time mobile systems. Next, an event-based schedule is defined and the composition of schedules is discussed. Then, we investigate the schedulability of isolation—that is, checking whether a given schedule ensures the isolation relationship among mobile objects or not. After that, we present an automation approach for scheduling generation to guarantee isolation controls in real-time mobile systems. Finally, case studies and simulation experiments demonstrate the usability and effectiveness of our approach.

Autonomous driving systems are complex real-time mobile systems.To guarantee their safety and security, the mobile objects (agents) in these systems must be isolated from each other so that they do not collide with each other.Since isolation means two or more mobile objects cannot be located in the same area at the same time, a scheduling policy is required to control the movement of these mobile objects.However, traditional scheduling theories are based on task scheduling which is coarsegrained and cannot be directly used for fine-grained isolation controls.In this paper, we first propose an event-based formal model called a time dependency structure which is used to model and analyze real-time mobile systems.Then, an event-based schedule is defined.Finally, we analyze the schedulability of isolation-that is, checking whether a given schedule ensures the isolation relationship among mobile objects or not.

In a mobile system, mobility refers to a change in position of a mobile object with respect to time and its reference point, whereas isolation means the isolation relationship between mobile objects under some scheduling policies. Inspired by event-based formal models and the ambient calculus, we first propose the two types of special events, entering and exiting an ambient, as movement events to model and analyze mobility. Based on mobility, we then introduce the notion of the isolation of mobile objects for ambients. To ensure the isolation, a priority policy needs to be used to schedule the movement of mobile objects. However, traditional scheduling policies focus on task scheduling and depend on the strong hypothesis: The scheduled tasks are independent—that is, the scheduled tasks do not affect each other. In a practical mobile system, mobile objects and ambients interact with each other. It is difficult to separate a mobile system into independent tasks. We finally present an automatic approach for generating a priority scheduling policy without considering the preceding assumption. The approach can guarantee the isolation of the mobile objects for ambients in a mobile system. Experiments demonstrate these results.

Traditional formalisms model communication and mobility in a separate way.This may cause complex name management and complex analysis for a communicating and mobile system.In this paper, following the ambient calculus [2], we first propose two types of special events, entering and exiting an ambient, as movement events and discuss the relationship of ambients based on mobility.Then a communication model is introduced based on message movement, which can represent synchronous communication, asynchronous communication and broadcasting communication in a unified way.Finally, we show that such a communication model is contained in a general event-based formal model called a dependency structure [4], [5].

As a semi-formal model, a UML sequence diagram can be widely useful for modelling and analyzing functional behaviors of a developing software system. However, reasoning about decomposition and composition of sequence diagrams has not been addressed adequately. The traditional decomposition method is based on the ideas from a global system to local components, and local components are recomposed into the whole system according to communication assumptions or other mechanisms. In this paper, we propose an event-based formal semantics for sequence diagrams and present a new functional decomposition approach based on sequence diagrams. The new decomposition idea is from a global system to global subsystems. Under the decomposition method global subsystems can be recomposed into the global system using the composition operation called union without necessarily considering assumptions such as communication.

Summary In software engineering, UML activity diagrams in general can be useful for a modeling system functional behavior, ranging from the sequences of activities/actions from business processes within an organization or among organizations down to the detail of an algorithm. The stepwise refinement process makes activity diagrams more and more complex. To guarantee the behavior consistency and correctness under refinement, the activity diagrams must be decomposed according to the divide‐and‐conquer strategy. Traditional decomposition methods adopt manual techniques and cannot ensure the independence and completeness of the obtained subdiagrams. In this paper, a novel decomposition approach is proposed, which can automatically divide an activity diagram into atomic and correct subdiagrams (subdiagrams without abnormal behavioral problems) at the same level. When such an activity diagram specifies the whole functional behavior of a software system, the approach can in fact decompose a system into multiple atomic subsystems. Every atomic subsystem is a completely independent system. It may be independently developed, independently tested, and independently deployed. The method facilitates the management, development, and maintenance of a software system. With the help of a prototype tool, a case study demonstrates the decomposition method.

Mobility is a critical issue that must be considered during the modeling and analyzing of a mobile system. At a high abstract level, event-based models can directly specify a mobile system without the introduction of additional mechanisms. In this article, we first propose two types of special events, entering and exiting an ambient, as movement events. Next, based on the movement events, we introduce the notion of a movement path and propose a feasible movement criterion (deciding whether a given movement path of a mobile object (agent) is feasible or not in terms of spatiotemporal topological relationships of ambients). Then, we investigate how a message movement--based communication model represents synchronous communication, asynchronous communication, and broadcast communication in a unified way. Finally, we use movement event sequences to discuss the exclusivity of ambients (an ambient only allows one mobile object to occupy (enter) it at any moment) and show that a priority scheduling control policy can guarantee exclusivity. Accordingly, we propose a correct movement criterion—that is, a correct movement path is feasible and satisfies the exclusivity of ambients. Case studies demonstrate these results.

The traditional research on scheduling focuses on task scheduling and schedulability analysis in concurrent reactive systems. In this article, we dedicate ourselves to event-based scheduling. We first formally define an event-based scheduling policy and propose the notion of the correctness of a scheduling policy in terms of weak termination. Then we investigate the correctness of the decomposition of scheduling controls and finally obtain a decentralized scheduling method. The method can automatically decompose the scheduling policies of a concurrent reactive system into atomic scheduling policies. Every atomic scheduling policy corresponds to one subsystem. Each of the subsystems is a completely independent system, which may be developed and deployed independently. An experiment demonstrates these results that may help engineers to design correct and efficient schedule policies for a concurrent reactive system.

Virtualization is fundamental to cloud computing. It allows abstraction centred on services and isolation of lower level functionalities and underlying hardware. Modeling, analyzing and verifying cloud systems necessarily involve virtualization and services. However, there exist few efforts to effectively formalizing virtualization in cloud computing. In this paper, based on services we present an approach for defining virtualization. We discuss some properties of service virtualization under some operations and the correctness of virtual services (virtual services without abnormal behavioral problems). Moreover, we investigate automatic configuration of a service based on virtualization, that is, given a virtualized service, how can we automatically obtain all possible correct virtual services of such a service? The configuration process is to first separate a virtualized service into atomic and correct virtual services and then merge these atomic virtual services into all possible correct virtual services of such a virtualized service. The obtained theoretical results help to formally analyze, verify and configure cloud systems.

Mismatch patterns capture the possible differences between two service (business) protocols to adapt. For these mismatches, formal definitions are presented in this paper. And a novel technique provides support for adapting two or more services. This technique requires that messages and message dependencies are used to directly model service (business) protocols and form a novel model, called a\emph{protocol structure}. Unlike most of existing approaches that only consider typical mismatches (e.g. deadlock), this model is easily used to detect multiple mismatches at a time and to automatically generate BPEL adapters.

In SOA, adaptation techniques aim to automatically generate adapters. However, the generation of the adapter is a complicated task and requires extra knowledge to resolve all kinds of mismatches. We propose a novel model, called a protocol structure, which is used to model services and adapters and detect the mismatches among services. Once developers present interface mappings among services, adapters can be derived from the interface mappings.