Many IoT systems are data intensive and are for the purpose of monitoring for fault detection and diagnosis of critical systems. A large volume of data steadily come out of a large number of sensors in the monitoring system. Thus, we need to consider how to store and manage these data. Existing time series databases (TSDBs) can be used for monitoring data storage, but they do not have good models for describing the data streams stored in the database. In this paper, we develop a semantic model for the specification of the monitoring data streams (time series data) in terms of which sensor generated the data stream, which metric of which entity the sensor is monitoring, what is the relation of the entity to other entities in the system, which measurement unit is used for the data stream, etc. We have also developed a tool suite, SE-TSDB, that can run on top of existing TSDBs to help establish semantic specifications for data streams and enable semantic-based data retrievals. With our semantic model for monitoring data and our SE-TSDB tool suite, users can retrieve non-existing data streams that can be automatically derived from the semantics. Users can also retrieve data streams without knowing where they are. Semantic based retrieval is especially important in a large-scale integrated IoT-Edge-Cloud system, because of its sheer quantity of data, its huge number of computing and IoT devices that may store the data, and the dynamics in data migration and evolution. With better data semantics, data streams can be more effectively tracked and flexibly retrieved to help with timely data analysis and control decision making anywhere and anytime.
Dataraces are a notorious concurrency error that most shared-memory parallel programs have the potential to cause but that rarely come out of hiding in test runs. To eradicate dataraces, a large amount of detection techniques have been proposed so far, some of which are efficient enough to be used in an always-on fashion during testing and debugging. However, existing lightweight race detectors either (1) suffer from false negatives (Le. miss races) due to the use of vector clock algorithms (detection results by which are highly dependent on thread schedules) or (2) incur false positives (i.e. issue false race-alarms) due to the use of coarse-grained lockset analysis. In this paper, we present an adaptive range-sensitive lockset analysis to overcome these drawbacks. The analysis focuses on compound memory objects (such as arrays and structures) to dynamically associate their truly shared subregions with fine-grained locksets. Preliminary case studies provide good evidence for the effectiveness of our analysis. Indeed, for small (but real) benchmarks, the analysis was able to prune spurious race-alarms (that coarse-grained lockset analysis would incur) while avoiding false negatives (that would occur with vector clocks).
The evolved smart grid has become a cyber physical energy system that could be exposed to a massive amount of cyber threats. Vulnerabilities within the cyber part can be used to launch multiple types of attacks that corrupt the physical system. The complexity of cyber physical energy system, the existing of different kinds of attacks, require an appropriate tool to aid in modeling and simulation for cyber security analysis. In this paper, we introduce a modeling language Modelica to the security community of cyber physical system. We show the capability of Modelica in modeling complex systems and attacks by building up a power grid model with frequency control loop (i.e., automatic generation control), as well as data integrity attack and data availability attack models. The simulation results show how different types of attacks or even combined attacks can affect the system frequency stability.
Several approaches have been developed to assist automotive system manufacturers in designing safer vehicles by complying with functional safety standards.However, most of these approaches either mainly focus on the technical aspects of automotive systems and ignore the social ones, or they are not equipped with an adequate automated support.To this end, we propose a model-based approach for modeling and analyzing the Functional Safety Requirements (FSR) for automotive systems, which is based on the ISO 26262 standard and considers both technical and social aspects of such systems.This approach proposes a UML profile for modeling the FSR starting from item definition until safety validation, and it proposes constraints expressed in OCL to be used for the verification of FSR models.We illustrate the utility of the approach using an example from the automotive domain.
Moose File System (MooseFS) is an Open-source, POSIX-compliant distributed file system, which provides a high throughput access to application data and is suitable for applications that have large data sets. Its high performance, high availability and fault-tolerant features have drawn huge interest from industry. However, the correctness of the dominate parts including reading and writing files of MooseFS has not got much attention of academia, which is the main concern of industry. In this paper, we use the process algebra Communicating Sequential Process (CSP) to model and analyze MooseFS. We mainly focus on the dominant parts which include reading and writing files in MooseFS and formalize them in detail. On that basis, we use the model checker Failures Divergence Refinement (FDR) to automatically simulate the developed model and verify whether the model is consistent with the specification and exhibits relevant secure properties including deadlock freedom, divergence-free, mutual exclusion and backup scheme.
As the urban size is constantly expanding, urban complex, which is an integrated area of business, catering and entertainment, has became an essential part of our daily life. However, urban complex leads to high passenger flow volume. One of the significant problems is customers spend more and more time on waiting for a taxi. To solve this problem, we present a novel mini-bus system, which transports customers from the exits of the complex to the optimal selected areas nearby to reduce the waiting time. Specifically, based on the harvested data of transportation and passenger flow volume in urban complexes, we establish this mini-bus system in Suzhou Center, one of the largest and most advanced urban complexes in China. The experimental results show that our system significantly reduces the waiting time for customer and thus improve the customer experience.
Computer security has gained more and more attention in a public over the last years, since computer systems are suffering from significant and increasing security threats that cause security breaches by exploiting software vulnerabilities. The most efficient way to ensure the system security is to patch the vulnerable system before a malicious attack occurs. Besides the commonly-used push-type patch management, the pull-type patch management is also adopted. The main issues in the pull-type patch management are two-fold; when to check the vulnerability information and when to apply a patch? This paper considers the security patch management for a virtual machine (VM) based intrusion tolerant system (ITS), where the system undergoes the patch management with a periodic vulnerability checking strategy, and evaluates the system security from the availability aspect. A composite stochastic reward net (SRN) model is applied to capture the attack behavior of adversary and the defense behaviors of system. Two availability measures; interval availability and point-wise availability are formulated to quantify the system security via phase expansion. The proposed approach and metrics not only enable us to quantitatively assess the system security, but also provide insights on the patch management. In numerical experiments, we evaluate effects of the intrusion rate and the number of vulnerability checking on the system security.
Model transformation tools assist system designers by reducing the labor-intensive task of creating and updating models of various aspects of systems, ensuring that modeling assumptions remain consistent across every model of a system, and identifying constraints on system design imposed by these modeling assumptions. We have proposed a model transformation approach based on abstract interpretation, a static program analysis technique. Abstract interpretation allows us to define transformations that are provably correct and specific. This work develops the foundations of this approach to model transformation. We define model transformation in terms of abstract interpretation and prove the soundness of our approach. Furthermore, we develop formalisms useful for encoding model properties. This work provides a methodology for relating models of different aspects of a system and for applying modeling techniques from one system domain, such as smart power grids, to other domains, such as water distribution networks.
Healthy operational status of space imager is important for the successful completion of space exploration tasks, and any abnormal event may lead to serious faults or disasters. Real-time anomaly detection is an important technique for finding abnormal parameters and potential faults of space equipment. The downlink data of space imager is streaming data that presents technique challenges and opportunities. The fundamental capability of anomaly detection techniques for space imager streaming data is to model each stream in an unsupervised fashion and detect unusual. Under the influence of operating instructions, environmental conditions and equipment performance, the streaming times series fluctuates acutely and indicates obvious concept drifting. Besides, application constraints require the method to process data in real-time, not batches. However, most anomaly detection methods need offline training of amount of historical data, and it is difficult to realize the online learning and detecting continuously. In this paper, a novel method is proposed that meets the constraints. The method is based on online time series memory and learning algorithm called Hierarchical Temporal Memory (HTM). We also present the comparison results of the proposed method and other algorithms, and the experiments show the proposed method could realize the real-time anomaly detection effectively.
In order to achieve safe, secure, efficient and environmentally sustainable air traffic management at global, regional and local levels, the system-wide operational information exchange and life-cycle management technologies are required. The System Wide Information Management (SWIM) is to provide a collaborative air traffic management environment for system-wide interoperability and harmonization operation. However, according to current point-to-point communication and local information management, it is a challenge to construct a collaborative environment for system-wide flight and flow information exchange which enables a common operational picture for all related stakeholders in order to achieve safe operation. In this paper, based on a practical validation exercise, the architecture and the collaborative information exchange technology to support coordination between ground to-ground and air-to-ground systems are proposed. Moreover, the problems and challenges for constructing the collaborative operating environment to include interactions of related stakeholders using data, systems, and services through a system wide information management environment are discussed.
The cost of care (COC) and quality of care (QOC) of healthcare services provided by healthcare organizations (HCOs) has been a central issue in the US healthcare system. This paper provides a structural model of a healthcare organization (HCO). This model will serve as the infrastructure that will be used to track conditions impact the COC and QOC in real time, whenever possible. The structural model of HCOs is achieved by defining the relevant system domains, populated by their components, which directly contribute to the cost and quality of care using a concept of traceability. A framework for large-scale complex systems, namely the Engineering Systems Multiple-Domain Matrix is used to ensure comprehensiveness and facilitate integration and analysis of system engineering data. The analysis of the model suggests that it is generic and can be applied to any HCO. It is shown that the developed network topology model provides a structure for a model-based approach to automate patient flow and resource utilization management, which can contribute to sustainable improvement to QOC and reduction to COC.
Many threat cases for in-vehicle systems have been reported and various methods to enhance automotive security have been proposed in recent years. One of the methods proposed is a means for detecting possible CAN message spoofing by attaching a message authentication code(MAC) to controller area network (CAN) messages. It is expected, however, that MAC generation keys are compromised during the replacement of ECUs if malicious dealers or repair shops are attackers. For this reason, a secure ECU replacement method is proposed in this paper.
To counter the exorbitant cost of developing certifiable safety-critical software, we propose task execution models that realize an architectural mitigation-based approach to achieving high integrity and highly predictable safety-critical systems. Our premise is that high design assurance levels (DALs) for a software component may be achieved as follows: each system operation that needs a high assurance level will be handled by a software component that has high performance/quality-of-service on average, but built at a lower assurance level, and this component is "monitored" by one (or more) simple component(s) that is (are) predictable, may have lower QoS, but is (are) built at the highest assurance level. The components associated with a software function would run isochronously on separate processors. We present a suite of such isochronous allocation and scheduling problems with varying levels of generality, along with their solutions. We extend our results to the recurrent task model, where tasks should complete before their deadlines.
The distribution network fault will cause big range and long-time blackout which will affect the safe and stable operation of the power system. The difficulty of locating grounding faults in power distribution networks is arc-suppression-coil-ground neutral system. The introduction of the arc suppression coil and the increase of the compensation current in the system make the relationship among zero sequence currents more complex, moreover, the comparison of zero sequence currents to realize the grounding fault location of arc suppression coil becomes more difficult. Although the residual increment method, short-circuit fault indicator method, signal injection method and first-half wave method are proposed in our country, but their effect are not good for grounding fault with high transition resistance, and the success rate of the grounding fault location is not high. In order to improve the real-time and accuracy of online monitoring for grounding fault location in the distribution network, this paper proposes a grounding fault location method based on regional parameters. The method divides the distribution network into several regions, and each region is installed a zero-phase sequence current transformer at the boundary. The transformer is used to measure the zero-phase sequence current, and the voltage transformer is used to measure the three-phase grounding voltages. According to the zero-phase sequence current, it can calculate the total grounding current of each region; through analysis and calculation of the total grounding current and the grounding voltages of three-phase line, we can get the three-phase grounding conductivities and the three-phase grounding susceptances. The simulation verifies that the grounding fault diagnosis method based on regional parameters has certain versatility, especially for high resistance grounding fault problems, thus it has great significance to ensure the safe and stable operation of distribution network and transmission line.
The CAST-32A provides some guidelines to help certify multi-core-based systems in the avionics domain. One major requirement is to compute all the potential interference and to provide adequate mitigation means. In this paper, we compare two approaches to identify the interference: the initiator-target and the PHYLOG models. The latter is more compact and efficient, despite also covering all of the problematic conflictual situations.
A pressure to deploy autonomous systems in real life is increasing. Since exhaustive verification of safety of autonomous systems is unfeasible, the emphasis should be put on safety optimisation and run-time safety-monitoring techniques. In this paper, we propose a multi-layered architecture of autonomous systems. We define the notions of strategic, tactic and active safety the complementary mechanisms for achieving safety. We take a swarm of drones as an example and formally define a multi-layered safety architecture and associated coordination mechanisms and underlying communication model to implement the defined complementary safety mechanisms. The derived coordination logic and communication model is formalised in Event-B framework.
The rise of complex Cyber-Physical Systems has led to many initiatives to promote automation of the assurance of their dependability. There exists mature practices and tools to perform necessary activities to provide evidence that a system satisfies dependability requirements. However, there is few harmonized an integrated framework that can support both the definition of the evidence and their collection and management from the specification to the V&V activities to testify of the assurance of those systems in compliance with standards. This paper presents Sophia, a framework that supports assurance of critical cyber physical systems using compositional model-based approaches. Sophia features a wide range of dependability analysis tools targeting all phases of system lifecycle for development of cyber physical systems. Sophia further helps trace the developed analysis outcomes to the requirements in standards for compliance support. We have validated the framework components through different case studies that indicate its usefulness and efficiency in helping prepare for certification of the systems.
Avoiding undefined software behavior in case of software faults is important to ensure a minimum of software quality even in unexpected situations. We discuss interface error injection in the embedded domain, which is used to extend unit testing for successful to faulty executions. Since well-known methods are not applicable, we present a new injection method based on AspectC++, an aspect-oriented language extension for C++, as it allows for automated injection of errors without modifying the C++ source code. Our method is flexible, for example it allows to inject errors into arbitrary software interfaces as well as interfaces defined by specifications. For an application scenario, we consider the POSIX standard, as its importance is growing in embedded systems, and provide automatisms to generate the test environment. We use custom C++ attributes, an AspectC++ language extension, to control the automatic testing process by providing information about potential errors. Finally, we compare it with existing approaches.
There are various possible mechanisms for updating potentially vulnerable and exploitable software and firmware on Internet connected devices. Due to their well-known benefits, delta updates have become a common way of updating software. Recently, several authors proposed the use of blockchain technology to update software and firmware. While both delta updates and blockchain technology are now used in different areas, this paper studies the feasibility of combining the two technologies for firmware updates on resource constrained IoT devices such as Wi-Fi smart plugs and sensors. The paper identifies the scenarios where delta updates may not work and proposes a private blockchain network-based IoT device firmware integrity verification and update mechanism. The proposed private blockchain mechanism for integrity verification utilizes a tamper-proof blockchain server. The proposed solution aims to enhance firmware update performance.
This paper presents a methodology for modelling and verification of high-assurance distributed protocols. In the paper we describe two main technical contributions needed for the development method: communication modelling patterns and a refinement strategy. The applicability of the proposed method is demonstrated by developing a new distributed resource allocation protocol. We also discuss the necessity of integrating other tools such as stochastic model checkers for enabling verification of wider range of protocol properties.
