Abstract:Geometric algebra(GA) is an algebraic language used to describe and calculate geometric problems.Due to its unified expression and coordinate-free geometric calculation, GA has now become an important theoretical foundation and calculation tool in mathematical analysis, theoretical physics, geometry and many other fields.While being widely used in the areas of modern science and technology, GA based analysis is traditionally performed using computer based numerical techniques or symbolic methods.However, both of these techniques cannot guarantee the analysis accuracy for safety-critical applications.The higher order-logic theorem proving is one of the rigorous formal methods.This paper establishes a formal model of GA in the higher-order logic proof tool HOL Light.The proof of the correctness is provided for some definitions and properties including blade, multivector, outer product, inner product, geometric product, inverse, dual, operation rules of basis vector and transform operator.In order to illustrate the practical effectiveness and utilization of this formalization, a conformal geometric model is established to provide a simple and effective way on rigid body motion verification.

Abstract:Termination of a class of nonlinear loops is analyzed in this paper.Based on Groebner bases, determining the termination problem of this type of loop programs is equivalent to determining whether or not the iteration functions of the loops have fixed points in the domains specified by loop guards.

Abstract:This work presents a new framework for urban traffic flow control based on the real time calculus(RTC) method.The queuing behavior of the traffic flow is transformed into an arrival curve, and the capacity of the intersection is characterized by a service curve.According to different signal control strategies, the service and arrival curves at an intersection are used to calculate the outgoing arrival curve.This result curve at each intersection is further integrated with the curves at the adjacent intersections, which finally exhibits the RTC model of the whole traffic network.The presented model can evaluate the bounds of the delay D of a vehicle and the backlog B of an intersection.The experiments are settled on the urban girds, and reveal the changing trend of the congestion factors D and B that are under fixed-time and adapted control strategies respectively.This is followed by a discussion of how this modeling method helps to estimate the effect of different signal control strategies.

Abstract:Interrupt data race is a category of critical bugs in interrupt-driven software such as aerospace embedded software.However, interrupt is much different from thread or task on concurrency semantics, synchronization and schedule, and its ad-hoc characteristics is hard to describe.Thus the state-of-art data race detection techniques are not suitable to interrupt-driven software.In this paper, the data race bug repository of aerospace embedded software is reviews systematically, and seven bug patterns for harmful interrupt data race are proposed.For the pattern single variable access order, an efficient abstract interpretation based detection method is developed to support inter-procedural and interrupt concurrency analysis.A tool named SpaceDRC is designed to verify our method.The evaluation results show that SpaceDRC only takes 145ms to detect 21400 lines of code to find the true bugs.Up to now, SpaceDRC has been applied in several aerospace missions, increasing the efficiency of interrupt data race inspection by 5 times and making a significant reduction in bug omission rate.

Abstract:The trustworthiness of safety-critical systems(SCS) is very important.Assessing the trustworthiness mainly depends on data from test.In order to ensure the reliability and validity of test data, especially for such complex systems, manual testing is infeasible in practice.Development of test languages as effective way to implement automatic testing is inevitable trend for automatic testing of SCS.As in general test language for SCS, testing should be independent of specific equipment, including SCS(SCS under test) and test equipment.In the paper, the issues of equipment collaboration are discussed.Aiming at high order and real time characteristics of equipment collaboration during testing, types and expressions of equipment collaboration involved in test of SCS are proposed, and the syntax of statements of equipment collaboration is defined.Then by defining the evaluating rules of these equipment collaboration expressions, semantic rules of statements of equipment collaboration are specified, and related properties are proved to show the soundness of these semantic rules.This work demonstrates that the equipment collaboration is dynamic and open, and the test languages of SCS can be general.

Abstract:Refinement checking is an important method in formal verification to convey a refinement relationship between an implementation model and a specification model in the same language.If the specification satisfies certain property and the refinement relationship is strong enough to preserve the property, then implementation satisfies the property.Refinement checking was developed in order to verify different kinds of properties, traces, stables failures and failures/divergence.Refinement checking often relies on the subset construction, thus suffers from state space explosion.Recently, some researchers proposed a simulation based approach for solving the language inclusion problem of NFA, which outperforms the previous methods significantly and can be directly used in traces refinement checking.Base on this advancement, this work further proposes stable failures and failures-divergence refinement checking algorithms based on simulation relations.In addition, this work also extends the idea of trace refinement checking to timed systems, and proposes timed automata traces refinement checking based on simulation relations.Experimental results confirm the efficiency of the presented approaches.

Abstract:Condition/decision coverage(C/DC) is a frequently used coverage criteria for safety-critical software testing.It requires every decision and condition in the program have taken all possible outcomes(true or false).Existing approaches of automatic test generation for C/DC criteria are defective.For example, symbolic execution based approaches are limited by the constraint solver, which is difficult in processing non-linear constraints;hill climbing often sticks at local optima, which limits yielding of high-coverage cases;and simulated annealing and genetic algorithm need complicated configuration, which make the results unstable.In this paper, a novel test generation approach that is guided by linear fitting is proposed.The basis of the approach is to sample every decision and condition of numerical values with program instrumentation.The relationship of inputs and samples is then build with linear fitting functions.By searching the target inputs on the gradually refined functions, test case is generated with high coverage.Experiments on 25 real programs in open source projects show that the proposed approach is more effective and efficient than the genetic algorithm of test generation.

Abstract:Multi-core processors are being widely used in safety-critical systems.Unfortunately, the introduction of performance-enhancing architectural elements, such as pipelines, out-of-order execution, dynamic branch prediction, caches and inter-cores resource-sharing, make WCET(worst-case execution time) analysis of a system become more difficult.Thus, time-predictable system design is established to meet the challenge of building systems for which WCET can be statically and easily analyzed.At the software level, this paper proposes a time-predictable multi-threaded code generation based on synchronous-model development.At the platform level, it presents a time-predictable multi-core architecture model in AADL(architecture analysis and design language), and then maps the multi-threaded code to this model.Real-time specifications propagate down in the system hierarchy.As a result, the proposed method integrates time predictability across several design layers, and finally reduces the complexity of WCET analysis.

Abstract:Interference problems refer to the undesired interaction between aspects and base programs or interaction between aspects that results in unexpected functions and is harmful to the correctness of the entire program.The difficulty in detecting and fixing interferences in aspect-oriented designs impedes the widespread application of aspect-oriented programming paradigm.Suffered from the scalability problem, existing researches that use model checking techniques cannot effectively handle functional interferences.The paper designs and implements a tool that employs deduction-based technologies to support direct checking and remove functional interferences in aspect-oriented designs.This tool can automatically generate proof obligations excluding the existence of interference.In addition, the paper introduces the tool PVS to raise the automation level of verification.The proof can either ascertain no interference exists or give clues on how to rectify the design.

Abstract:Barrier certificates have been widely used in verification of continuous systems.The main idea is to find a barrier which separates the reachable set from the unsafe set such that all the trajectories starting from the initial set will never go across the barrier.Thus the system's safety can be guaranteed by constructing a barrier.In recent years, barrier certificates have been successfully used for verification of continuous systems with unbounded time.However sometimes the safety for bounded time needs to be addressed.Since a system is unsafe with unbounded time cannot imply it is also unsafe with a bounded time, the unbounded time barrier certificate method could fail to verify the safety with bounded time.In this paper, a method is presented to generate a bounded time barrier certificate for safety verification of continuous systems with bounded time.Some sufficient conditions for the bounded time barrier certificate are specified.If the continuous system is a polynomial system, relax all the conditions of positive semi-definite polynomial to the sum of squares(SOS) polynomial and then use semi-definite programming(SDP) to solve the conditions for a bounded time barrier certificate;if the continuous system is an elementary system(containing some elementary functions), transform it to a polynomial system approximately, and then solve the corresponding polynomial system for a bounded time barrier certificate.For some practical examples which are unsafe for unbounded time, the paper shows the effectiveness of the proposed method for generating bounded time barriers.

Abstract:In recent years people have witnessed an increased worldwide attention to the concept of smart buildings.Compared with traditional counterpart, smart buildings are more energy efficient, comfortable and maintainable.Hence, smart buildings are becoming the mainstream of future building construction.As a key part of smart building ventilation systems, air conditioners highly impact the overall energy consumption of smart buildings as well as the experience of their occupants.Therefore, how to design and evaluate feasible scheduling strategies of air conditioning systems becomes a major challenge in the design of smart buildings.Especially when many uncertain factors caused by physical environment are involved, the complexity of strategy evaluation increases drastically.Although existing approaches allow the evaluation of smart buildings from the perspectives of energy consumption and performance, few of them consider the evaluation of the scheduling strategies themselves.Based on priced timed automata, this paper proposes an efficie framework that enables accurate modeling and evaluation of scheduling strategies of smart building air-conditioning systems with uncertain environment.This framework utilizes the statistical model checker UPPAAL-SMC as the engine to quantitatively analyze user-specified performance queries in the form of properties.Based on the underlying random simulation runs monitored by UPPAAL-SMC, the framework can automatically report the quantitative analysis results of energy consumption and user satisfaction under uncertain environment.Experimental results show that the proposed approach can effectively help smart building designers to make their decisions in the selection and optimization of scheduling strategies.

Abstract:Programs become more error-prone with inappropriate management of memory because of pointer aliasing, e.g., dereferencing null or dangling pointers, and memory leaks.PPTL^SL is a two-dimensional(spatial and temporal) logic which integrates separation logic with PPTL(propositional projection temporal logic).It is useful to describe and verify temporal properties of list manipulating programs.This paper first gives an overview of PPTL^SL, and then introduces the foundation of the tool SAT-PPTL^SL in detail.SAT-PPTL^SL can be used to check the satisfiability of PPTL^SL formulas according to the "isomorphic" relationship between PPTL^SL and PPTL.In addition, the paper presents examples to show the checking process of SAT-PPTL^SL and analyze the effect of some key parameters on the performance of SAT-PPTL^SL.

Abstract:Infinite data exists extensively in computer programs and database systems.Driven by the need from the applications of formal verification and database management, formal models over infinite alphabets are becoming a research focus of theoretical computer science.The main purpose of this article is to do a relatively complete and detailed survey on this topic.The article is organized according to the different mechanisms of automata models to deal with the infinite data values.The main focus is on the decidability and complexity of the related decision problems, that is, the nonemptiness and language inclusion problem of automata, and the satisfiability problem of logics.

Abstract:Learning to rank(L2R) techniques try to solve sorting problems using machine learning methods, and have been well studied and widely used in various fields such as information retrieval, text mining, personalized recommendation, and biomedicine.The main task of L2R based recommendation algorithms is integrating L2R techniques into recommendation algorithms, and studying how to organize a large number of users and features of items, build more suitable user models according to user preferences requirements, and improve the performance and user satisfaction of recommendation algorithms.This paper surveys L2R based recommendation algorithms in recent years, summarizes the problem definition, compares key technologies and analyzes evaluation metrics and their applications.In addition, the paper discusses the future development trend of L2R based recommendation algorithms.

Abstract:Accurately extracting content from Web news is a key technology for quality improvement in Web news analysis and applications.Due to the lack of publication standards, differences in publishing formats, and a highly heterogeneous big data carrier of the Web itself, Web news extraction has become an open research problem.Extensive case studies by this research indicate that there is potential relevance between Web content layouts and their tag paths.Inspired by this observation, this paper designs a series of tag path extraction features to distinguish the Web content and noise from different perspectives.Based on the similarity analysis of these features, the paper proposes a features fusion strategy with group feature selection, and provides a Web news extraction method via feature fusion, CEPF.CEPF is a fast, universal, no-training and online Web news extraction algorithm.It can extract Web news pages across multi-resources, multi-styles, and multi-languages.Experimental results with public data sets such as CleanEval show that the CEPF method achieves better performance than the state-of-the-art CETR method.

Abstract:The fast development of the Internet also results in sharp rise in network energy consumption.The energy efficiency of present network devices is very low, which is an obstacle in realizing energy-proportional computing.However, while networks are designed for peak hour load, actual network load can be quite low in a large fraction of time, leaving great opportunity for energy saving.After an introduction of the energy consumption model of network devices, theories and technologies for optimizing network energy consumption are studied from two aspects.First, when the total amount of network traffic cannot be changed, it is possible to add power and performance states to individual network devices and optimize local control policies to realize energy proportionality;or, without sophisticated power management capabilities, it is also possible for a network as an ensemble to realize energy proportionality through coordination and traffic engineering.Second, it is possible to reduce or alleviate the traffic by providing cache capability to the network, which in turn reduces or alleviates the growth of network transmission energy.Intelligent cache deployment, content cache and request routing policies can further optimize network energy consumption.Based on the above discussion, a thorough comparison between different technologies is provided and potential future research directions are analyzed.

Abstract:In this paper the historic development of public-key cryptanalysis and important literature are surveyed.In particular the breakthroughs during 2010~2014 about the discrete logarithm problems for finite fields and elliptic curves are described.Since the birth of public key cryptography, public key cryptanalysis has been developed to be an inter discipline research with tools from mathematics, algorithmic science and experimental simulations.This survey intents to help the young researchers in Chinese cryptologic community to enter this active research field.