Abstract:The main task of real-time system design is to analyze the timing behaviors of a system at design time in order to guarantee that the given timing constraints are met at run time. The key issue is to estimate the Worst-Case Execution Time (WCET) of a program. Typically the WCET is heavily influenced by the hardware features of the target processor, among which Cache is the most influential factor. This article presents a survey on Cache analysis for WCET estimation. It introduces main research problems and challenges in different dimensions, such as the analysis of loops, data caches, multi-level caches, multi-core shared caches, non-LRU replacement policies, etc. The mainstream analysis techniques with their pros and cons are evaluated. An outlook for future research directions of Cache analysis is given in the end.

Abstract:With the widespread use of embedded software in safety critical system, software safety assurance becomes one of research hotspots of software engineering. In this paper, a survey is presented on Software safety standards, methods and tools in aircraft systems. First of all, airborne software safety definitions and standards are introduced, and the safety analysis framework is also presented. Secondly, airborne software safety analysis methods are classified into three types, namely, software requirement elicitation and specification, safety standard oriented software development, and software safety property verification. Existing research and application of software safety analysis methods are reviewed according to these three types. After that, existing researches on safety evidence collection during airborne software safety assurance process according to airworthiness certification are summarized. Finally, potential research directions of airborne software safety assurance are discussed.

Abstract:Hybrid System is a very important subclass of real time embedded system. The behavior of hybrid system is tangled with discrete control mode transformation and continuous real time behavior, therefore very complex and difficult to control. As hybrid system is widely used in safety-critical areas like industry, defense and transportation system, it is very important to analyze and understand the system effectively to guarantee the safe operation of the system. Ordinary techniques like testing and simulation can only observe the behavior of the system under given input. As they cannot exhaust all the possible inputs and scenarios, they are not enough to guarantee the safety of the system. In contrast to testing based techniques, formal method can answer questions like if the system will never violate certain specification by traversing the complete state space of the system. Therefore, it is very important to pursue the direction of formal verification of safety-critical hybrid system. Formal method consists of formal specification and formal verification. This paper reviews the modeling language and specification of hybrid system as well as techniques in model checking and theorem proving. In addition, it discusses the potential future directions in the related area.

Abstract:Based on CBSE (component-based software engineering), this research on composable embedded software investigates the theory, methods and technologies for modeling and verification of embedded components. The paper surveyes the state-of-the-art research and practices on composable embedded system from three perspectives: composite theory, modeling, and verification techniques. It introduces the optimistic and pessimistic definitions of component compatibility, and composition mechanisms including operations and rules. In modeling techniques, the paper particularly addresses the issues of composition of non-functional attributes and heterougeneous components, which are important to embedded components design and verification. It analyzes non-functional attribute constraints and multi-attributes oriented model. The paper also investigates three typical verification techniques of component composition including contract-based, invariants-based, and model checking techniques. It discusses future works in the end.

Abstract:To keep pace with the fast growing computing power, the memory system of mobile devices has become more complicated and larger in capacity. As a result, the memory systems, especially the on-chip cache and the main memory, consume a major portion of the system energy. With the limited lifespan of the battery, the memory system of the mobile device demands energy-efficient design and techniques urgently. Without the exploration of the memory access patterns of the programs, it is impossible to fully exploit the potential energy benefits provided by the current memory hardware. This paper introduces the memory access patterns of the programs, describes its three main characteristics, and discusses how to develop energy-efficient techniques based on it in detail. In the end, some future trends in this area are discussed.

Abstract:With the rapid development of technology, the application area of embedded systems continues to broaden. This makes the development of embedded systems facing increased pressure of quality, cost and cycle time. On the other hand, agile methods have been more and more adopted in traditional software projects. Many studies indicated that agile methods have significant values to adapt to changing requirements, increasing the productivity and the quality of the final product. Therefore, the application of agile methods in embedded systems development naturally has drawn attentions from researchers and practitioners. This paper applies systematic reviews to systematically understand the application status of agile methods in embedded system development. Through reviewing and analyzing 49 literatures since Agile Manifesto has been announced, this study tries to answer the following three questions: 1) In different types of embedded systems development, what is the overall application status of agile methods; 2) What characteristics of embedded systems are suitable to apply agile methods; 3) How to improve current agile methods (practices) to better adapt to the development of embedded systems. The study shows that, although there are some differences in the degree of application, agile methods have been applied in the development of different types of embedded system developments. However, the traditional agile methods also need to be appropriately revised to adapt to the characteristics of different types of embedded development projects.

Abstract:Multi-Core processors are more and more widely used in embedded systems as they provide great computing capacities to integrate multiple functionalities with different criticality levels into a shared platform. The scheduling problem of mixed-criticality systems appears to be challenging, even on single-processor platforms. This work extends the state-of-the-art single-processor mixedcriticality scheduling algorithm EY-VD to multi-processor systems. To begin with, it integrates EY-VD into traditional workload partitioning schemes to get a multiprocessor mixed-criticality scheduling algorithm MC-PEDF (mixed-criticality partitioned earliest deadline first). Although MC-PEDF performs better than previous solutions, the study finds that the traditional workload partitioning schemes are not suitable for mixed-criticality systems as it does not explore the asymmetricity of workload on different criticality levels. To overcome this problem, a workload partitioning policy OCOP (one criticality one partition) is proposed. OCOP allows tasks to be reassigned to a different processor when criticality mode switch occurs, thus can better balance the resource utilization among processors on different criticality levels. Based on OCOP, the second partitioned scheduling algorithm MC-MP-EDF (mixed-criticality multi-partitioned EDF) is constructed. Experiments with randomly generated workload show that MC-MP-EDF can drastically improve the system schedulability comparing with MC-PEDF and other previous algorithms, especially for systems with more processors.

Abstract:With the prevalence of general purpose computation, GPUs (graphics processing units) are becoming extremely important to significantly improve system performances for many computing systems, including embedded systems. Running massively parallel kernels on GPUs is challenging for system’s overall performance especially when large amount of workloads (kernels) are running together. This paper investigates how to schedule large amount of workloads that have to be executed on GPUs to minimize the makespan of all workloads to improve the system overall performance. By considering the transfer time and execution time together, the study makes an abstraction for each workload and formulate the scheduling problem on GPUs into a 2D rectangular strip-packing model. A polynomial 3-approxiamation algorithm is proposed to solve the strip-packing problem. The approximation results exhibit an effective approach for workload sequencing during the data offloading on GPUs. It also implies that the scheduling jointed by workload sequencing for GPUs data offloading and first-come-first-serve (FCFS) scheduling inside GPUs with workload conserving can improve the system performance optimally or near-optimally.

Abstract:NAND flash memory has been widely used in various embedded systems. Due to the “out-of-place” update constraints, a component of address translator in NAND flash management is needed to translate logical address from file system to physical address in NAND flash. With the capacity increase of NAND flash, it becomes vitally important to take small RAM print of the address mapping table while not introducing big performance overhead. Demand-based address mapping is an effective approach to solve this problem by storing the address mapping table in NAND flash (called translation pages) and catching mapping items on-demand in RAM. However, in such address mapping method, there exists extra many translation pages that may incur much performance overhead. This paper solves two most important problems in translation page management. First, to reduce frequent translation page updates overhead, a page-level caching mechanism is proposed to unify the granularity of the cached mapping unit in NAND flash and in translation caching. Second, to reduce the garbage collection overhead from translation pages, a translation page based data-assemblage strategy is designed to group data pages corresponding to the same translation page into one data block, reducing the cost of translation page update during garbage collection to the minimal level. The presented scheme is evaluated using a set of benchmarks and is compared to a representative previous work. Experimental results show that the new techniques can achieve significant reduction in the extra translation operations and improve the system response time.

Abstract:The development of wireless sensor networks requires the ability of efficiently updating application software running on sensors. To address this problem, this paper proposes ReLog, a reprogramming-oriented logical programming language for wireless sensor network applications and its processing system. Based on common characteristics of wireless sensor network applications, the ReLog language extends a traditional logical programming language and provides suitable programming abstractions with which programmers can write and modify programs efficiently. Meanwhile, the language processing system leverages on intermediate code to decouple application programs from system software so as to reduce the size of updating code to improve the updating efficiency. This paper demonstrates ReLog through a case of data collection application. Results show that ReLog can achieve compact and ease-to-modified source code. In addition, the executing mechanism of ReLog can significantly reduce the cost of energy and time when transmitting updating code of applications.

Abstract:Synchronous data-flow languages have been widely used in safety-critical industrial areas such as airplanes, high-speed railways, nuclear power plants, and so on. However，the safety of development tools themselves for this kind of languages has become one of the potential safety problems which have been highly focused on. It has proved to be successful to implement the construction and verification of a conventional language compiler using an assistant theorem prover, and it is expected to have the opportunity in solving the miscompilation problem to the utmost extent. Based on such an approach, the key technologies for a trustworthy compiler from a synchronous data-flow language (Lustre as the prototype) to a sequential imperative language (C as the prototype) have been studied. The challenge lies in the great difference between the source and target languages, where the source language has the features of clock synchrony, data-flow, concurrency, stream data object, etc., while the target language is instead with the sequential and control-flow features. Among the similar researches, there is no reported result so far for the key translation stages. Recently, this research completed a formal verification for the whole compilation stages in the case of single clock. The related technologies will be taken into the development of a safety-level compiler in the country’s nuclear power system. The paper presents a survey on the trustworthy compiler with the research background, the architecture, the key technologies, the current status, and the future work.

Abstract:In order to improve the precision of static analysis for C procedures, this paper introduces a static analysis method applying region-based symbolic three-valued logic (RSTVL). RSTVL can describe shape of data structures, all kinds of memory states and relations of addressable expressions including alias relations, hierarchical relations and logic relations. To improve precision, a RSTVLbased analysis method is proposed to analyze the shape, dataflow and point-to relationship at every procedure point. The method facilitates flow-sensitive and field-sensitive intra-procedure, and context-sensitive inter-procedure analysis based on symbolic function summary. Experimental results validate that the porposed static analysis method offers higher precision on the precondition with no efficiency loss.

Abstract:With the rapid increase of embedded computer system applications, the reliability of embedded software has drawn particular attention from researchers and industries. Many methods for testing and verifying reliability of embedded software have been discussed. However, the existing methods are weak in test suite automatic generation and therefore difficult in tackling large numbers of embedded computer applications. In this paper, the method and the technique of generating abstract test suite and their adaptation to a computer platform are presented. An algorithm for translating a LTS (labeled transition system) into BT (behavior tree) is proposed. Consequently, the TTCN (test and testing control notation) abstract test suite that employs BT as logical structure can automatically be generated with respect to the LTS description of embedded software. A TTCN tool set based on the translation algorithm for testing embedded software is introduced, and case study of testing embedded system of Internet of things device is presented.

Abstract:Defect detection generally includes two stages: static analysis and defect inspection. A large number of defects reported may lead developers and managers to reject the use of static analysis tools as part of the development process due to the overhead of defect inspection. To help with the inspection tasks, this paper formally introduces defect correlation, a sound dependency relationship between defects. If the occurrence of one defect causes another defect to occur, the two defects are correlated. This paper presents a sound optimized method to static analysis that can classify the defects reported by static defect detection tool into different groups, in which all defects are false positives (true positives) if the dominant defect is false positives (true positives). The experimental results show a decrease of 22% the time inspecting all defects and the capability and flexibility of this method to detect defects of large, critical or embedded systems.

Abstract:Cyber-Physical Systems (CPSs) have great potentials in several application domains. Time plays an important role in CPS and should be specified in the very early phase of requirements engineering. This paper proposes a framework to model and verify timing requirements for the CPS. To begin with, a conceptual model is presented for providing basic concepts of timing and functional requirements. Guided by this model, the CPS software timing requirement specification can be obtained from CPS environment properties and constraints. To support formal verification, formal semantics for the conceptual model is provided. Based on the semantics, the consistency properties of the timing requirements specification are defined and expressed as CTL formulas. The timing requirements specification is transformed into a NuSMV model and checked by this well-known model checker.

Abstract:In order to reduce the overall energy consumption of the distributed embedded system（DES）, this paper proposes an adaptive energy management and analysis method based on the attributes of devices and their relationships by considering the boot device set and the dynamic supply voltage of devices. The study results in the distributed embedded energy consumption net (DE-Net) which is used to model the basic components of the embedded system. The model of energy consumption is then formed to characterize the execution process and the attributes of energy consumption. Finally, CTL is used to express the basic properties of DES. The operational semantics of Petri nets helps verify the correctness and effectiveness of the proposed method. The example and experimental results show that this method can correctly describe the adaptive energy consumption of DES and simplify the modeling and analysis process, which has important theoretical significance and practical value for developing the low energy consumption of DES.