On the Effectiveness of the System Validation Based on the Black Box Testing Methodology

With the advancement of technology in recent years, effective fault diagnosis became a necessity to verify the performance and ensure the quality of complex systems. In this paper, an original verification methodology for complex consumer electronic devices is presented. Verification of the system which consists of hardware （integrated circuit） and corresponding software within a flat panel TV set is in the focus. Proposed methodology provides reliable functional failure detection using the concept of black box testing. Further, the approach is fully automated, improving the reliability and speed of failure detection. The methodology effectiveness has been experimentally evaluated and the analysis results have been reported.

A QUANTIFIER-ELIMINATION BASED HEURISTIC FOR AUTOMATICALLY GENERATING INDUCTIVE ASSERTIONS FOR PROGRAMS

A method using quantifier-elimination is proposed for automatically generating program invariants/inductive assertions. Given a program, inductive assertions, hypothesized as parameterized formulas in a theory, are associated with program locations. Parameters in inductive assertions are discovered by generating constraints on parameters by ensuring that an inductive assertion is indeed preserved by all execution paths leading to the associated location of the program. The method can be used to discover loop invariants-properties of variables that remain invariant at the entry of a loop. The parameterized formula can be successively refined by considering execution paths one by one; heuristics can be developed for determining the order in which the paths are considered. Initialization of program variables as well as the precondition and postcondition, if available, can also be used to further refine the hypothesized invariant. The method does not depend on the availability of the precondition and postcondition of a program. Constraints on parameters generated in this way are solved for possible values of parameters. If no solution is possible, this means that an invariant of the hypothesized form is not likely to exist for the loop under the assumptions/approximations made to generate the associated verification condition. Otherwise, if the parametric constraints are solvable, then under certain conditions on methods for generating these constraints, the strongest possible invariant of the hypothesized form can be generated from most general solutions of the parametric constraints. The approach is illustrated using the logical languages of conjunction of polynomial equations as well as Presburger arithmetic for expressing assertions.

WIDE:A witness-based data priority mechanism for vehicular forensics

In this paper,we present a WItness based Data priority mEchanism(WIDE)for vehicles in the vicinity of an accident to facilitate liability decisions.WIDE evaluates the integrity of data generated by these vehicles,called witnesses,in the event of an accident to assure the reliability of data to be used for making liability decisions and ensure that such data are received from credible witnesses.To achieve this,WIDE introduces a two-level integrity assessment to achieve end-to-end integrity by initially ascertaining the integrity of data-producing sensors,and validating that data generated have not been altered on transit by compromised road-side units(RSUs)by executing a practical byzantine fault tolerance(pBFT)protocol to reach consensus on data reliability.Furthermore,WIDE utilises a blockchain based reputation management system(BRMS)to ensure that only data from highly reputable witnesses are utilised as contributing evidence for facilitating liability decisions.Finally,we formally verify the proposed framework against data integrity requirements using the Automated Verification of Internet Security Protocols and Applications(AVISPA)with High-Level Protocol Specification Language(HLPSL).Qualitative arguments show that our proposed framework is secured against identified security attacks and assures the reliability of data utilised for making liability decisions,while quantitative evaluations demonstrate that our proposal is practical for fully autonomous vehicle forensics.