一种结合线性时序逻辑和故障树的软件安全验证方法

嵌入式软件在安全关键领域的广泛应用使得保障软件的安全性成为学界的研究热点。故障树技术是工业界常用的传统的安全分析方法之一。然而,传统的故障树无法精确描述安全关键系统中具有时序特征的系统故障。针对此问题,给出了一种结合线性时序逻辑和故障树的安全验证方法。该方法运用线性时序逻辑对故障树进行形式化规约,从中抽取出软件安全属性并用时序逻辑公式进行描述,用以支持对安全关键软件的模型检验。最后,以某机载控制系统软件数据处理故障模块的模型检验为例,来说明该方法的有效性和可行性。     

Testing aspect‐oriented programs with finite state machines

Aspect‐oriented programming yields new types of programming faults due to the introduction of new constructs for dealing with crosscutting concerns. To reveal aspect faults, this paper presents a framework for testing whether or not aspect‐oriented programs conform to their state models. It supports two families of strategies (i.e. structure‐oriented and property‐oriented) for automated generation of aspect tests from aspect‐oriented state models. A structure‐oriented testing strategy derives tests and test code from an aspect‐oriented state model to meet a given structural coverage criterion, such as state coverage, transition coverage, or round trip. A property‐oriented testing strategy generates test code from the counterexamples of model checking. Two such strategies are checking an aspect‐oriented state model against trap properties and checking mutants of aspect models against system properties. Mutation analysis of aspect‐oriented programs is used to evaluate the effectiveness of these testing strategies. The experiments demonstrate that testing aspect‐oriented programs against their state models can detect many aspect faults. The comparative evaluations also reveal that the structure‐oriented and property‐oriented testing strategies complement each other—some aspect faults were detected by the structure‐oriented strategies, but not by the property‐oriented strategies and vice versa. Copyright © 2010 John Wiley & Sons, Ltd.     

对逻辑覆盖软件测试准则的公理化评估

由于形式规格说明采用一种精确、一致、容易被机器自动处理的符号系统来描述软件需求,因而形式规格说明为测试用例的自动生成和软件功能的验证提供了基础.在基于形式规格说明的测试过程中逻辑覆盖测试准则是一组常用的测试准则,如何选择和使用其中的每个测试准则是应用这组测试准则时面临的主要问题.因此分析和比较这组测试准则中每个测试准则的性质将为测试工程师选择测试准则提供指导和帮助.对测试充分性准则的公理化评估是一种比较测试准则的方式,这种方式将对理想的测试准则的直觉需求定义为一组公理,然后通过检查测试准则是否满足该组公理来分析和比较相应的测试准则.描述了一组理想的逻辑覆盖测试准则应该具有的性质和用来确定一个测试充分性准则是否完全的生成算法.这组性质被形式化地定义为一组公理.利用这种形式化的定义,用定理的形式精确地给出了这些性质之间的关系.最后通过这组公理系统来评估现有的逻辑覆盖测试准则.评估的结果为测试人员在实际过程中选择逻辑覆盖测试准则提供了指导.     

基于时态测试器的实时分支时态逻辑模型检测

基于自动机理论的模型检测技术在形式化验证领域处于核心地位, 然而传统自动机在时态算子上不具备可组合性, 导致各种时态逻辑的模型检测算法不能有机整合.本文为了实现集成限界时态算子的实时分支时态逻辑RTCTL*的高效模型检测, 提出一种RTCTL*正时态测试器构造方法, 以及相关符号化模型检测算法.证明了所提出的RTCTL*正时态测试器构造方法是完备的.也证明了该算法时间复杂度与被验证系统呈线性关系, 与公式长度呈指数关系.我们基于JavaBDD软件包成功开发了该算法的模型检测工具MCTK 2.0.0.我们完成了MCTK与著名的符号化模型检测工具nuXmv之间的实验对比分析工作, 结果表明MCTK虽然在内存消耗上要多于nuXmv, 但是MCTK的时间复杂度双指数级小于nuXmv, 使得利用MCTK验证大规模系统的实时时态性质成为可能.     

Using a bounded model checker for test generation: How to kill two birds with one SMT solver

Automated test generation has received a lot of attention in recent decades, because it is one possible solution to the problems inherent to software testing: the need to write tests in the first place and providing test coverage for the human factor. De facto the most promising technique to automatically generate a test is dynamic symbolic execution assisted by an automated constraint solver, e.g., an SMT solver. This process is very similar to bounded model checking, which also deals with generating models from source code, asserting logic properties in it, and processing the returned model. This paper describes a prototype unit test generator for C based on a working bounded model checker called Borealis and shows that these two techniques are very similar and can be easily implemented using the same basic components. The prototype test generator has been evaluated on a number of examples and has shown good results in terms of test coverage and test excessiveness.     

A data flow-based structural testing technique for FBD programs

With increased use of programmable logic controllers (PLCs) in implementing critical systems, quality assurance became an important issue. Regulation requires structural testing be performed for safety-critical systems by identifying coverage criteria to be satisfied and accomplishment measured. Classical coverage criteria, based on control flow graphs, are inadequate when applied to a data flow language function block diagram (FBD) which is a PLC programming language widely used in industry. We propose three structural coverage criteria for FBD programs, analyze relationship among them, and demonstrate their effectiveness using a real-world reactor protection system. Using test cases that had been manually prepared by FBD testing professionals, our technique found many aspects of the FBD logic that were not tested sufficiently. Domain experts, having found the approach highly intuitive, found the technique effective.     

应用MC/DC准则时需考虑的问题及其改进方法

MC／DC(修订的条件／判定覆盖)准则是一种实用的软件结构覆盖率测试准则。目前，MC／DC在国际上已被广泛地应用于软件验证和测试过程中，在我国也被应用于一些软件项目中。介绍了MC／DC准则，提出了用此准则进行结构覆盖率分析时需注意的两个问题：结构覆盖率分析的问题和复杂逻辑语句的问题。最后，详细讨论了用MC／DC准则检查逻辑表达式错误时需考虑的3个方面及相应的改进方法，这3个方面包括逻辑式中操作符OR与XOR的误写、括号的位置不正确和逻辑组元被误写。     

A practical model‐based statistical approach for generating functional test cases: application in the automotive industry

With the growing complexity of industrial software applications, industrials are looking for efficient and practical methods to validate the software. This paper develops a model‐based statistical testing approach that automatically generates online and offline test cases for embedded software. It discusses an integrated framework that combines solutions for three major software testing research questions: (i) how to select test inputs; (ii) how to predict the expected results of a test; and (iii) when to stop testing software. The automatic selection of test inputs is based on a stochastic test model that accounts for the main particularity of embedded software: time sensitivity. Software test practitioners may design one or more test models when they generate random, user‐oriented, or fault‐oriented test inputs. A formal framework integrating existing and appropriate specification techniques was developed for the design of automated test oracles (executable software specifications) and the formal measurement of functional coverage. The decision to stop testing software is based on both test coverage objectives and cost constraints. This approach was tested on two representative case studies from the automotive industry. The experiment was performed at unit testing level in a simulated environment on a host personal computer (automatic test execution). The two software functionalities tested had previously been unit tested and validated using the test design approach conventionally used in the industry. Applying the proposed model‐based statistical testing approach to these two case studies, we obtained significant improvements in performing functional unit testing in a real and complex industrial context: more bugs were detected earlier and in a shorter time. Copyright © 2012 John Wiley & Sons, Ltd.     

基于分支覆盖的回归测试路径选择

回归测试是迭代式软件开发的重要环节,测试数据生成是回归测试的前提.传统的回归测试方法,从已有的测试数据中选择部分测试数据,并生成一些新的测试数据,以验证程序的正确性.但是,该方法容易生成冗余的测试数据,从而降低了回归测试的效率.研究了回归测试的分支覆盖问题,通过利用已有测试数据的路径覆盖信息,并选择一定个数的路径,以覆盖所有的目标分支.首先,以若干路径形成的集合作为决策变量,以路径最少、覆盖的分支最多以及包含的未覆盖路径最少为目标,建立路径选择问题的3目标优化模型;然后,采用遗传算法求解上述模型时,设计了基于目标重要性的个体评价策略;最后,基于已有的测试数据与选择的路径之间的覆盖关系,确定需要生成的测试数据.将所提方法应用于6个基准工业程序测试中,并与其他方法比较.实验结果表明,采用该方法选择的路径,能够覆盖更多的分支,需要生成的测试数据更少,回归测试消耗的时间更短.     

使用基于脚本的故障注入测试安全苛求软件

由于安全性苛求软件直接关系人身和大宗财产的安全,为此需要对软件进行严格的安全性测试。提出了一个基于脚本语言的故障注入方法以期得到新的测试手段。此方法通过在故障环境下运行安全苛求软件检验其是否容错和故障安全,结果显示软件测试覆盖率和揭错能力均有增强。该系统可进一步提高安全苛求软件测试自动化水平和测试效率。     

An initial industrial evaluation of interactive search-based testing for embedded software

Search-based software testing promises the ability to generate and evaluate large numbers of test cases at minimal cost. From an industrial perspective, this could enable an increase in product quality without a matching increase in the time and effort required to do so.Search-based software testing, however, is a set of quite complex techniques and approaches that do not immediately translate into a process for use with most companies.For example, even if engineers receive the proper education and training in these new approaches, it can be hard to develop a general fitness function that covers all contingencies. Furthermore, in industrial practice, the knowledge and experience of domain specialists are often key for effective testing and thus for the overall quality of the final software system. But it is not clear how such domain expertise can be utilized in a search-based system.This paper presents an interactive search-based software testing (ISBST) system designed to operate in an industrial setting and with the explicit aim of requiring only limited expertise in software testing. It uses SBST to search for test cases for an industrial software module, while also allowing domain specialists to use their experience and intuition to interactively guide the search.In addition to presenting the system, this paper reports on an evaluation of the system in a company developing a framework for embedded software controllers. A sequence of workshops provided regular feedback and validation for the design and improvement of the ISBST system. Once developed, the ISBST system was evaluated by four electrical and system engineers from the company (the ‘domain specialists’ in this context) used the system to develop test cases for a commonly used controller module. As well as evaluating the utility of the ISBST system, the study generated interaction data that were used in subsequent laboratory experimentation to validate the underlying search-based algorithm in the presence of realistic, but repeatable, interactions.The results validate the importance that automated software testing tools in general, and search-based tools, in particular, can leverage input from domain specialists while generating tests. Furthermore, the evaluation highlighted benefits of using such an approach to explore areas that the current testing practices do not cover or cover insufficiently.     

Formal modeling and synthesis of programmable logic controllers

Programmable logic controllers (PLCs) are complex cyber-physical systems which are widely used in industry. This paper presents a robust approach to design and implement PLC-based embedded systems. Timed automata are used to model the controller and its environment. We validate the design model with resort to model checking techniques. We propose an algorithm to generate PLC code from timed automata and implement this algorithm with a prototype tool. This method can condense the developing process and guarantee the correctness of PLC programs. A case study demonstrates the effectiveness of the method.     

黑箱条件下的软件测试充分性与揭错能力分析

在白箱条件下,软件的测试充分性可通过语句覆盖、判定覆盖、条件覆盖、判定／条件覆盖和路径覆盖等方法进行度量。但在黑箱情况下,这些基于程序的覆盖度量方法不再实用,为此提出了基于程序外部特性的测试充分性,即基于功能覆盖的软件测试充分性概念。然而对于一个较复杂的安全性关键软件仅仅满足功能覆盖的软件测试充分性是不够的,应增加安全性扩充测试。经过对黑箱条件下的软件测试技术揭错能力的分析,得出了基于第3方的软件安全性测试技术在理论上有条件发现所有的软件危害故障的结论。     

软件自动化测试中热点路径的研究

在面向路径的软件测试中,对于大型系统将会产生海量的静态路径,测试人员很难对所有路径进行完全测试。本文提出热点路径的思想,运用该思想可以在繁多的静态路径中迅速找到容易引起程序缺陷的路径,通过热点函数树形化可以对热点进行快速定位显示,给软件测试人员带来更多的便捷,提高测试效率,降低测试成本。     

GenUTest: a unit test and mock aspect generation tool

Unit testing plays a major role in the software development process. What started as an ad hoc approach is becoming a common practice among developers. It enables the immediate detection of bugs introduced into a unit whenever code changes occur. Hence, unit tests provide a safety net of regression tests and validation tests which encourage developers to refactor existing code with greater confidence. One of the major corner stones of the agile development approach is unit testing. Agile methods require all software classes to have unit tests that can be executed by an automated unit-testing framework. However, not all software systems have unit tests. When changes to such software are needed, writing unit tests from scratch, which is hard and tedious, might not be cost effective. In this paper we propose a technique which automatically generates unit tests for software that does not have such tests. We have implemented GenUTest, a prototype tool which captures and logs interobject interactions occurring during the execution of Java programs, using the aspect-oriented language AspectJ. These interactions are used to generate JUnit tests. They also serve in generating mock aspects—mock object-like entities, which enable testing units in isolation. The generated JUnit tests and mock aspects are independent of the tool, and can be used by developers to perform unit tests on the software. Comprehensiveness of the unit tests depends on the software execution. We applied GenUTest to several open source projects such as NanoXML and JODE. We present the results, explain the limitations of the tool, and point out direction to future work to improve the code coverage provided by GenUTest and its scalability.     

Non-specification-based approaches to logic testing for software

Testing is a crucial part of the development of software systems. In this paper, we consider testing of an implementation that is intended to satisfy a Boolean formula. In the literature, specification-based testing has been suggested for this purpose. Typically, such methods first hypothesize a fault class and then generate tests. However, there is almost no research that justifies fault classes proposed previously. Moreover, specifications amenable to automatic test generation are not always available to testers in practice. Based on these observations, we examine the applicability of non-specification-based approaches, which need no specification in the form of a Boolean formula to create tests. We compare a specification-based approach to three non-specification-based approaches, namely, random testing, antirandom testing, and combinatorial testing. The results of an experiment show that combinatorial testing is often comparative to specification-based testing and is superior to both random testing and antirandom testing.     

Iterative Android automated testing

With the benefits of reducing time and workforce, automated testing has been widely used for the quality assurance of mobile applications (APPs). Compared with automated testing, manual testing can achieve higher coverage in complex interactive Activities. And the effectiveness of manual testing is highly dependent on the user operation process (UOP) of experienced testers. Based on the UOP, we propose an iterative Android automated testing (IAAT) method that automatically records, extracts, and integrates UOPs to guide the test logic of the tool across the complex Activity iteratively. The feedback test results can train the UOPs to achieve higher coverage in each iteration. We extracted 50 UOPs and conducted experiments on 10 popular mobile APPs to demonstrate IAAT’s effectiveness compared with Monkey and the initial automated tests. The experimental results show a noticeable improvement in the IAAT compared with the test logic without human knowledge. Under the 60 minutes test time, the average code coverage is improved by 13.98% to 37.83%, higher than the 27.48% of Monkey under the same conditions.     

Analysing sanity of requirements for avionics systems

In the last decade it became a common practice to formalise software requirements to improve the clarity of users’ expectations. In this work we build on the fact that functional requirements can be expressed in temporal logic and we propose new sanity checking techniques that automatically detect flaws and suggest improvements of given requirements. Specifically, we describe and experimentally evaluate approaches to consistency and redundancy checking that identify all inconsistencies and pinpoint their exact source (the smallest inconsistent set). We further report on the experience obtained from employing the consistency and redundancy checking in an industrial environment. To complete the sanity checking we also describe a semi-automatic completeness evaluation that can assess the coverage of user requirements and suggest missing properties the user might have wanted to formulate. The usefulness of our completeness evaluation is demonstrated in a case study of an aeroplane control system.     

Automatic testing environment for multi-core embedded software—ATEMES

Software testing during the development process of embedded software is not only complex, but also the heart of quality control. Multi-core embedded software testing faces even more challenges. Major issues include: (1) how demanding efforts and repetitive tedious actions can be reduced; (2) how resource restraints of embedded system platform such as temporal and memory capacity can be tackled; (3) how embedded software parallelism degree can be controlled to empower multi-core CPU computing capacity; (4) how analysis is exercised to ensure sufficient coverage test of embedded software; (5) how to do data synchronization to address issues such as race conditions in the interrupt driven multi-core embedded system; (6) high level reliability testing to ensure customer satisfaction. To address these issues, this study develops an automatic testing environment for multi-core embedded software (ATEMES). Based on the automatic mechanism, the system can parse source code, instrument source code, generate testing programs for test case and test driver, support generating primitive, structure and object types of test input data, multi-round cross-testing, and visualize testing results. To both reduce test engineer's burden and enhance his efficiency when embedded software testing is in process, this system developed automatic testing functions including unit testing, coverage testing, multi-core performance monitoring. Moreover, ATEMES can perform automatic multi-round cross-testing benchmark testing on multi-core embedded platform for parallel programs adopting Intel TBB library to recommend optimized parallel parameters such as pipeline tokens. Using ATEMES on the ARM11 multi-core platform to conduct testing experiments, the results show that our constructed testing environment is effective, and can reduce burdens of test engineer, and can enhance efficiency of testing task.