View source for SURF 2020: Hardware Implementation of Contract-Based Design for Automated Valet Parking System

'''[[SURF 2020|2020 SURF]]: project description'''
* Mentor: Richard M. Murray
* Co-mentor: Josefine Graebener

==Project Description==
Due to the increasing complexity of cyber-physical systems, a modular approach to the design of these systems is necessary, while also guaranteeing correct and reliable behavior. Hybrid systems with multiple layers of abstraction need to ensure the correct implementation and composition of the components. For example a system can consist of a high level decision making process, which is then refined to lower layers of abstraction, which implement the desired behavior by composing components on each layer. For this layered design to satisfy the specification, rules for the composition of the components and refinement of the layers are necessary. This is guaranteed by contracts between the layers and the components in each layer of the system, which define the accepted behavior of the overall system [5].
A system specification can be defined in terms of contracts using temporal logic as specification language, which can be formally verified [3]. Systems can be designed according to a contract-based methodology as proposed in [1]. This defines the system under normal operations, but for safety-critical systems such as self driving cars it is necessary to guarantee a specific behavior in the presence of failures as well. To achieve this we introduce reactivity into our contract design, which defines how the system will react to failure scenarios [2][4].

The example under consideration is an automatic valet parking, which shall be verified in an experimental setup. The focus of this project is the vertical contract architecture (contracts between the layers) which define the refinement of the specification including pre-defined failure scenarios. 

The study objective is to set up the parking lot infrastructure in a small scale model using multiple R/C cars and verify the control strategy, which means executing the parking and retrieving process with multiple cars in the parking lot during normal operations and including failure scenarios, such as cars stopping during the process or unexpected obstacles. 

The project requires some familiarity with Python or enough programming experience to learn it in a short time. Experience in experimental robotics and ROS is an advantage.

[[File:AVP.png|thumb|500px|right|Parking lot layout.]]

==References==

[1] Albert Benveniste, Benoit Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, et al.. Contracts for System Design. [Research Report] RR-8147, INRIA. 2012, pp.65. 〈hal-00757488〉

[2] Burdick J. W. et al., Sensing, Navigation and Reasoning Technologies for the DARPA Urban Challenge, DARPA Urban Challenge Final Report, 2007 

[3] P. Nuzzo, H. Xu, N. Ozay, J. B. Finn, A. L. Sangiovanni-Vincentelli, R. M. Murray, A. Donze, S. A. Seshia. A Contract-Based Methodology for Aircraft Electric Power System Design. IEEE Access, 2014. DOI 10.1109/ACCESS.2013.2295764

[4] T. Phan-Minh, R. M. Murray, Contracts of Rectivity, Submitted, Int'l Conf on Formal Modeling and Analysis of Timed Systems (FORMATS) 2019

[5] Alberto Sangiovanni-Vincentelli, Werner Damm, Roberto Passerone, Taming Dr. Frankenstein: Contract-Based Design for Cyber-Physical Systems, European Journal of Control (2012)3:217–238