Date: Thursday 28 March 2019
Time: 14:00 - 15:30
Location / Room: Room 1
Chair:
Eugenio Villar, Universidad de Cantabria, ES
Co-Chair:
Marc Geilen, Eindhoven University of Technology, NL
MBD of Cyber-Physical Systems
| Time | Label | Presentation Title Authors |
|---|---|---|
| 14:00 | 11.1.1 | SPECIFYING AND EVALUATING QUALITY METRICS FOR VISION-BASED PERCEPTION SYSTEMS Speaker: Jyotirmoy Deshmukh, Arizona State University, US Authors: Adel Dokhanchi, Aniruddh Puranic, Xin Qin, Anand Balakrishnan, Heni Ben Amor, Georgios Fainekos and Jyotirmoy V. Deshmukh, Univ. of Southern California, US Abstract Robust perception algorithms are a vital ingredient for autonomous systems such as self-driving vehicles. Checking the correctness of perception algorithms such as those based on deep convolutional neural networks (CNN) is a formidable challenge problem. In this paper, we suggest the use of Timed Quality Temporal Logic (TQTL) as a formal language to express desirable spatio-temporal properties of a perception algorithm processing a video. While perception algorithms are traditionally tested by comparing their performance to ground truth labels, we show how TQTL can be a useful tool to determine quality of perception, and offers an alternative metric that can give useful information, even in the absence of ground truth labels. We demonstrate TQTL monitoring on two popular CNNs: YOLO and SqueezeDet, and give a comparative study of the results obtained for each architecture. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 14:30 | 11.1.2 | MODELING CROSS-LAYER INTERACTIONS FOR DESIGNING CERTIFIABLE CYBER-PHYSICAL SYSTEMS Speaker: Samarjit Chakraborty, TU Munich, DE Authors: Samarjit Chakraborty, James H. Anderson, Martin Becker, Helmut Graeb, Samiran Halder, Ravindra Metta, Lothar Thiele, Stavros Tripakis and Anand Yeolekar, TU Munich, DE Abstract A central challenge in designing embedded control systems or cyber-physical systems (CPS) is that of translating high-level models of control algorithms into efficient implemen- tations, while ensuring that model-level semantics are preserved. While a large body of techniques for designing provably correct control strategies exist in the control theory literature, when it comes to transforming mathematical descriptions of these strategies to an efficient implementation, the available means are surprisingly ad hoc in nature. Among other reasons, this is be- cause of (i) implementation platform details not sufficiently being accounted for in controller models, (ii) side effects introduced in the code generation process, (iii) various compiler optimizations whose impact on the dynamics of the plant being controlled not being properly understood, (iv) the presence of analog components on the implementation platform whose behavior is difficult to model, (v) computation and communication delays that exist in an implementation but were not accounted for in the model, and (vi) also the effects of image/video processing whose accuracy and timing behavior are difficult to model. As we move towards designing autonomous systems, these issues become biting problems on the path to certification, and striking a balance between performance and certification. In this position paper, we discuss some of these challenges - that we formulate as the need for modeling the interactions between various imple- mentation layers in a CPS - and potential research directions to address them. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 15:00 | 11.1.3 | STEPS TOWARD VERIFIED PROGRAMMING OF EMBEDDED COMPUTING DEVICES Speaker: Jean-Pierre Talpin, INRIA, FR Authors: Jean-Pierre Talpin1, Jean-Joseph Marty1, Shravan Narayan2, Deian Stefan2 and Rajesh Gupta2 1INRIA, FR; 2University of California at San Diego, US Abstract We propose a type-driven approach to building ver- ified safe and correct IoT applications. Today's IoT applications are plagued with bugs that can cause physical damage. This is largely because developers account for physical constraints using ad-hoc techniques. Accounting for such constrains in a more principled fashion demands reasoning about the composition of all the software and hardware components of the application. Our proposed framework takes a step in this direction by (1) using refinement types to make make physical constraints explicit and (2) imposing an event-driven programing discipline to simplify the reasoning of system-wide properties to that of an event queue. In taking this approach, our framework makes it possible for developers to build verified IoT application by making it a type error for code to violate physical constraints. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 15:30 | End of session 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 Breaks (Lunch Area)On all conference days (Tuesday to Thursday), a seated lunch (lunch buffet) will be offered in the Lunch Area to fully registered conference delegates only. There will be badge control at the entrance to the lunch break area. Tuesday, March 26, 2019
Wednesday, March 27, 2019
Thursday, March 28, 2019
|