Date: Tuesday 10 March 2015
Time: 14:30 - 16:00
Location / Room: Les Bans

Chair:
Saddek Bensalem, Université Joseph Fourier, FR

Co-Chair:
Linh Thi Xuan Phan, University of Pennsylvania, US

This session focuses on the analysis and verification in model-based design of embedded systems. It has four regular papers : The first paper presents a delay analysis method for a general graph based workload model. The second one presents a new formal approach to verifying Interrupt-driven software based on symbolic execution. The third one proposes a method for model-based verification (and arguably implementation) of real-time systems, where the original model is expressed as a network of UPPAAL timed automata (PIM). The fourth one presents a generic method to automatically generate a symbolic executor for a given hardware architecture specified by some Architecture Description Language, which is used to verify program properties regarding the binary code level. In this session we have also an IP paper, which presents a technique for estimating non-functional requirements using a Knowledge Discovery in Databases (KDD) approach.

Time	Label	Presentation Title Authors
14:30	3.7.1	DELAY ANALYSIS OF STRUCTURAL REAL-TIME WORKLOAD Speakers: Nan Guan1, Yue Tang2, Yang Wang2 and Wang Yi3 1Uppsala University, SE; 2Northeastern University, CN; 3Uppsala University, CN Abstract In many complex embedded systems, real-time workload is generated conforming certain structural constraints. In this paper we study how to analyze the delay of real-time workload of which the generation pattern can be modeled by task graphs. We first show that directly combining path abstraction technique (PAT) in real-time scheduling theory and real-time calculus (RTC) can provide safe delay bounds, but the results are typically over-pessimistic. Then we propose new algorithms to efficiently and precisely solve the delay analysis problem. Experiments with randomly generated task systems are conducted to evaluate the performance of the proposed methods. Download Paper (PDF; Only available from the DATE venue WiFi)
15:00	3.7.2	EFFECTIVE VERIFICATION OF LOW-LEVEL SOFTWARE WITH NESTED INTERRUPTS Speakers: Daniel Kroening1, Lihao Liang1, Tom Melham1, Peter Schrammel1 and Michael Tautschnig2 1University of Oxford, GB; 2Queen Mary, University of London, GB Abstract Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested and subject to priorities. Interrupts can arrive at arbitrary times, leading to an explosion in the number of cases to be considered. We present a new formal approach to verifying interrupt-driven software based on symbolic execution. The approach leverages recent advances in the encoding of the execution traces of interacting, concurrent threads. We assess the performance of our method on benchmarks drawn from embedded systems code and device drivers, and experimentally compare it to conventional formal approaches that use source-to-source transformations. Our experimental results show that our method significantly outperforms conventional techniques. To the best of our knowledge, our technique is the first to demonstrate effective formal verification of low-level embedded software with nested interrupts. Download Paper (PDF; Only available from the DATE venue WiFi)
15:30	3.7.3	PLATFORM-SPECIFIC TIMING VERIFICATION FRAMEWORK IN MODEL-BASED IMPLEMENTATION Speakers: Baek Gyu Kim, Lu Feng, Linh T.X. Phan, Oleg Sokolsky and Insup Lee, University of Pennsylvania, US Abstract In the model-based implementation methodology, the timed behavior of the software is typically modeled independently of the platform-specific timing semantics such as the delay due to scheduling or I/O handling. Although this approach helps to reduce the complexity of the model, it leads to timing gaps between the model and its implementation. This paper proposes a platform-specific timing verification framework that can be used to formally verify the timed behavior of an implementation that has been developed from a platform-independent model. We first describe a way to categorize the interactions among the software, a platform, and the environment in the form of implementation schemes. We then present an algorithm that systematically transforms a platform-independent model into a platform-specific model under a given implementation scheme. This transformation algorithm ensures that the timed behavior of the platform-specific model is close to that of the corresponding implementation. Our case study of an infusion pump system shows that the measured timing delay of the system is bounded by the formally verified bound of its platform-specific model. Download Paper (PDF; Only available from the DATE venue WiFi)
15:45	3.7.4	ARCHITECTURE DESCRIPTION LANGUAGE BASED RETARGETABLE SYMBOLIC EXECUTION Speaker: Andreas Ibing, TU München, DE Abstract This paper presents an approach to retargetable SMT-constrained symbolic execution of machine code. The retargetability is based on an existing open-source processor architecture description language which has been used for processor design and automatic generation of toolchains for dynamic program analysis. The benefit of the presented approach is that with a given architecture description, no manual writing of an instruction set grammar or of a translation of instruction semantics into logics is necessary. The proposed tool architecture relies on language reflection, code generation and dynamic loading to retarget symbolic execution to different machine code syntax. Instruction semantics is translated into SMT bit-vector logic equations by symbolically interpreting the architecture description language. The approach is implemented as plug-in extension to the Eclipse IDE and evaluated by automatically detecting integer overflows in binaries for the ARMv5 and SPARCv8 architectures. Download Paper (PDF; Only available from the DATE venue WiFi)
16:00	IP1-17, 877	NFRS EARLY ESTIMATION THROUGH SOFTWARE METRICS Speakers: Andrws Vieira1, Pedro Faustini1, Luigi Carro2 and Erika Cota1 1Federal University of Rio Grande do Sul (UFRGS), BR; 2Federal University of Rio Grande do Sul (UFRGS), Abstract We propose the use of regression analysis to generate accurate predictive models for physical metrics using design metrics as input. We validate our approach with 40+ implementations of three systems in two development scenarios: system evolution and first design. Results show maximum prediction errors of 1.66% during system evolution. In a first design scenario, the average error is 15% with the maximum error still below 20% for all physical metrics. This approach provides a fast and accurate strategy to boost embedded software productivity and quality, by estimating Non-Functional Requirements (NFRs) during the first design stages. Download Paper (PDF; Only available from the DATE venue WiFi)
16:00		End of session Coffee Break in Exhibition Area Coffee Break in Exhibition Area On all conference days (Tuesday to Thursday), coffee and tea will be served during the coffee breaks at the below-mentioned times in the exhibition area. Lunch Break On Tuesday and Wednesday, lunch boxes will be served in front of the session room Salle Oisans and in the exhibition area for fully registered delegates (a voucher will be given upon registration on-site). On Thursday, lunch will be served in Room Les Ecrins (for fully registered conference delegates only). Tuesday, March 10, 2015 Coffee Break 10:30 - 11:30 Lunch Break 13:00 - 14:30; Keynote session from 13:20 - 14:20 (Room Oisans) sponsored by Mentor Graphics Coffee Break 16:00 - 17:00 Wednesday, March 11, 2015 Coffee Break 10:00 - 11:00 Lunch Break 12:30 - 14:30, Keynote lectures from 12:50 - 14:20 (Room Oisans) Coffee Break 16:00 - 17:00 Thursday, March 12, 2015 Coffee Break 10:00 - 11:00 Lunch Break 12:30 - 14:00, Keynote lecture from 13:20 - 13:50 Coffee Break 15:30 - 16:00