IP2_1 Interactive Presentations

Date: Tuesday, 02 February 2021
Time: 17:00 - 17:30 CET
Virtual Conference Room: https://virtual21.date-conference.com/meetings/virtual/JGXWJ2m4MyTpq2spH

Interactive Presentations run simultaneously during a 30-minute slot. Additionally, each IP paper is briefly introduced in a one-minute presentation in a corresponding regular session

Label	Presentation Title Authors
IP2_1.1	AN EFFECTIVE METHODOLOGY FOR INTEGRATING CONCOLIC TESTING WITH SYSTEMC-BASED VIRTUAL PROTOTYPES Speaker: Sören Tempel, University of Bremen, DE Authors: Sören Tempel¹, Vladimir Herdt² and Rolf Drechsler³ ¹University of Bremen, DE; ²DFKI, DE; ³University of Bremen/DFKI, DE Abstract In this paper we propose an effective methodology for integrating Concolic Testing (CT) with SystemC-based Virtual Prototypes (VPs) for verification of embedded SW binaries. Our methodology involves three steps: 1) integrating CT support with the Instruction Set Simulator (ISS) of the VP, 2) utilizing the standard TLM-2.0 extension mechanism for transporting concolic values alongside generic TLM transactions, and 3) providing lightweight concolic overlays for SystemC-based peripherals that enable non-intrusive CT support for peripherals and thus significantly reduce the CT integration effort. Our RISC-V experiments using the RIOT operating system demonstrate the effectiveness of our approach.
IP2_1.2	A CONTAINERIZED ROS-COMPLIANT VERIFICATION ENVIRONMENT FOR ROBOTIC SYSTEMS Speaker: Samuele Germiniani, University of Verona, IT Authors: Stefano Aldegheri, Nicola Bombieri, Samuele Germiniani, Federico Moschin and Graziano Pravadelli, University of Verona, IT Abstract This paper proposes an architecture and a related automatic flow to generate, orchestrate and deploy a ROS-compliant verification environment for robotic systems. The architecture enables assertion-based verification by exploiting monitors automatically synthesized from LTL assertions. The monitors are encapsulated in plug-and-play ROS nodes that do not require any modification to the system under verification (SUV). To guarantee both verification accuracy and real-time constraints of the system in a resource-constrained environment even after the monitor integration, we define a novel approach to move the monitor evaluation across the different layers of an edge-to-cloud computing platform. The verification environment is containerized for both cloud and edge computing using Docker to enable system portability and to handle, at run-time, the resources allocated for verification. The effectiveness and efficiency of the proposed architecture have been evaluated on a complex distributed system implementing a mobile robot path planner based on 3D simultaneous localization and mapping.

Label

Presentation Title
Authors

IP2_1.1

AN EFFECTIVE METHODOLOGY FOR INTEGRATING CONCOLIC TESTING WITH SYSTEMC-BASED VIRTUAL PROTOTYPES
Speaker:
Sören Tempel, University of Bremen, DE
Authors:
Sören Tempel¹, Vladimir Herdt² and Rolf Drechsler³
¹University of Bremen, DE; ²DFKI, DE; ³University of Bremen/DFKI, DE
Abstract
In this paper we propose an effective methodology for integrating Concolic Testing (CT) with SystemC-based Virtual Prototypes (VPs) for verification of embedded SW binaries. Our methodology involves three steps: 1) integrating CT support with the Instruction Set Simulator (ISS) of the VP, 2) utilizing the standard TLM-2.0 extension mechanism for transporting concolic values alongside generic TLM transactions, and 3) providing lightweight concolic overlays for SystemC-based peripherals that enable non-intrusive CT support for peripherals and thus significantly reduce the CT integration effort. Our RISC-V experiments using the RIOT operating system demonstrate the effectiveness of our approach.

IP2_1.2

A CONTAINERIZED ROS-COMPLIANT VERIFICATION ENVIRONMENT FOR ROBOTIC SYSTEMS
Speaker:
Samuele Germiniani, University of Verona, IT
Authors:
Stefano Aldegheri, Nicola Bombieri, Samuele Germiniani, Federico Moschin and Graziano Pravadelli, University of Verona, IT
Abstract
This paper proposes an architecture and a related automatic flow to generate, orchestrate and deploy a ROS-compliant verification environment for robotic systems. The architecture enables assertion-based verification by exploiting monitors automatically synthesized from LTL assertions. The monitors are encapsulated in plug-and-play ROS nodes that do not require any modification to the system under verification (SUV). To guarantee both verification accuracy and real-time constraints of the system in a resource-constrained environment even after the monitor integration, we define a novel approach to move the monitor evaluation across the different layers of an edge-to-cloud computing platform. The verification environment is containerized for both cloud and edge computing using Docker to enable system portability and to handle, at run-time, the resources allocated for verification. The effectiveness and efficiency of the proposed architecture have been evaluated on a complex distributed system implementing a mobile robot path planner based on 3D simultaneous localization and mapping.