Date: Wednesday 16 March 2016
Time: 14:30 - 16:00
Location / Room: Konferenz 4

Chair:
Jian-Jia Chen, Technische Universität Dortmund, DE

Co-Chair:
Petru Eles, Linköping University, SE

This session presents new approaches that enable efficient analysis and testing of embedded software. The first paper presents an interesting dynamic partitioning strategy to reduce the complexity of symbolic execution based software testing. An extension to UML activity diagrams towards stocastic modeling is proposed in the second paper; this allows for quantitative reasoning based on statistical model checking techniques. The final paper presents a new testing methodology that combines symbolic decision procedures with statistical hypothesis testing to study the correctness of intelligent embedded systems.

Time	Label	Presentation Title Authors
14:30	7.6.1	DYNAMIC PARTITIONING STRATEGY TO ENHANCE SYMBOLIC EXECUTION Speaker: Brendan Marcellino, Virginia Tech, US Authors: Brendan Marcellino and Michael Hsiao, Virginia Tech, US Abstract Software testing is a fundamental part of the software development process. In the context of embedded-software applications, testing can find defects which cause unprecedented risks. The path explosion problem often necessitates one to consider an extremely large number of paths in order to reach a specific target. Symbolic execution can reduce this cost by using symbolic values and heuristic exploration strategies. Although various exploration strategies have been proposed in the past, the number of SMT solver calls for reaching a target is still large, resulting in long execution times for programs containing many paths. In this paper, we present a dynamic partitioning strategy in order to mitigate this problem, consequently reducing unnecessary SMT solver calls as well. Using this strategy on SSA-applied code, the code sections are analyzed in a nonconsecutive order guided by data dependency metrics within the sections. Experimental results show that our dynamic strategy can achieve significant speedups in reducing the number of unnecessary solver calls in large programs. More than 1000x speedup can be achieved in large programs over conflict-driven learning techniques. Download Paper (PDF; Only available from the DATE venue WiFi)
15:00	7.6.2	QUANTITATIVE TIMING ANALYSIS OF UML ACTIVITY DIAGRAMS USING STATISTICAL MODEL CHECKING Speaker: Mingsong Chen, East China Normal University, CN Authors: Fan Gu1, Xinqian Zhang1, Mingsong Chen1, Daniel Grosse2 and Rolf Drechsler2 1East China Normal University, CN; 2University of Bremen, DE Abstract Unified Modeling Language (UML) activity diagrams are widely used in modeling the dynamic aspects of system designs. However, due to frequent interactions between systems and external uncertain environment, the current version of UML activity diagrams cannot be used to accurately capture and quantify the overall timing behaviors of complex systems. To address this issue, this paper extends the UML activity diagrams to enable the stochastic modeling of user inputs and action executions, which strongly affect the overall timing behaviors of systems. Based on the statistical model checker UPPAAL-SMC, this paper proposes an automated framework that can perform quantitative reasoning under various functional and non-functional queries. Experimental results demonstrate the effectiveness of our proposed approach. Download Paper (PDF; Only available from the DATE venue WiFi)
15:30	7.6.3	INTEGRATING SYMBOLIC AND STATISTICAL METHODS FOR TESTING INTELLIGENT SYSTEMS: APPLICATIONS TO MACHINE LEARNING AND COMPUTER VISION Speaker: Sumit Kumar Jha, University of Central Florida, US Authors: Arvind Ramanathan1, Laura Pullum1, Faraz Hussain2, Dwaipayan Chakraborty2 and Sumit Kumar Jha2 1Oak Ridge National Laboratory, US; 2University of Central Florida, US Abstract Embedded intelligent systems ranging from tiny im- plantable biomedical devices to large swarms of autonomous un- manned aerial systems are becoming pervasive in our daily lives. While we depend on the flawless functioning of such intelligent systems, and often take their behavioral correctness and safety for granted, it is notoriously difficult to generate test cases that expose subtle errors in the implementations of machine learning algorithms. Hence, the validation of intelligent systems is usually achieved by studying their behavior on representative data sets, using methods such as cross-validation and bootstrapping. In this paper, we present a new testing methodology for studying the correctness of intelligent systems. Our approach uses symbolic decision procedures coupled with statistical hypothesis testing to validate machine learning algorithms. We show how we have employed our technique to successfully identify subtle bugs (such as bit flips) in implementations of the k-means algorithm. Such errors are not readily detected by standard validation methods such as randomized testing. We also use our algorithm to analyze the robustness of a human detection algorithm built using the OpenCV open-source computer vision library. We show that the human detection implementation can fail to detect humans in perturbed video frames even when the perturbations are so small that the corresponding frames look identical to the naked eye. Download Paper (PDF; Only available from the DATE venue WiFi)
16:00		End of session Coffee Break in Exhibition Area