# Difference between revisions of "SURF 2018: Contract-based Design of Control Systems"

(2 intermediate revisions by the same user not shown) | |||

Line 12: | Line 12: | ||

[[File:AVP.png|500px|right]] | [[File:AVP.png|500px|right]] | ||

− | 1. Study how to write formal specifications for contracts and implement algorithms that perform mathematical operations on contracts with the goal of automated contract synthesis, contract refinement and error recovery in mind. It is recommended that students willing to contribute to this version of the project have a basic knowledge of formal methods (see [3] for a quick introduction to the specification language TLA+) and automata theory. | + | 1. Study how to write formal specifications for contracts and implement algorithms that perform mathematical operations on contracts with the goal of automated contract synthesis, contract refinement and error recovery in mind. It is recommended that students willing to contribute to this version of the project have a basic knowledge of formal methods (see [3] for a quick introduction to the specification language TLA+) and automata theory (it might be helpful to have a look at [4]). |

2. Find a design scenario of interest to which our contract framework applies and demonstrate how they can be implemented. Some examples are autonomous valet parking service with non-cooperative human drivers, supervisory controller to vehicle communication subsystems. For a more concrete example, see [2]. Students interested in this version of the project should have a good knowledge of control theory. Experience with implementing controllers and generating simulations is highly valued. | 2. Find a design scenario of interest to which our contract framework applies and demonstrate how they can be implemented. Some examples are autonomous valet parking service with non-cooperative human drivers, supervisory controller to vehicle communication subsystems. For a more concrete example, see [2]. Students interested in this version of the project should have a good knowledge of control theory. Experience with implementing controllers and generating simulations is highly valued. | ||

Line 26: | Line 26: | ||

[3] https://www.learntla.com/introduction/ | [3] https://www.learntla.com/introduction/ | ||

+ | |||

+ | [4] Raclet, Jean-Baptiste, et al. "A modal interface theory for component-based design." Fundamenta Informaticae 108.1-2 (2011): 119-149. |

## Latest revision as of 07:00, 19 December 2017

**2018 SURF: project description**

- Mentor: Richard M. Murray
- Co-mentor: Tung Phan

## Description

As systems grow in scale and complexity, a modular approach to design becomes mandatory. With this comes the question of generating specifications for implementing submodules such that when these are reassembled at the end of the design process, a complete system that designers originally had in mind will emerge. Despite the existence of various theories and tools that support "local" design of submodules from many subfields of computer science and engineering, studies into interactions between these are still lacking. A contract-based methodology for system design like the one proposed in [1] is an attractive step in the direction of developing a mathematical design and specification framework.

In this project, we will investigate methods for integrating design implementations from different domains into a unified platform in a correct-by-construction manner. In particular, we allow the student to either choose to

1. Study how to write formal specifications for contracts and implement algorithms that perform mathematical operations on contracts with the goal of automated contract synthesis, contract refinement and error recovery in mind. It is recommended that students willing to contribute to this version of the project have a basic knowledge of formal methods (see [3] for a quick introduction to the specification language TLA+) and automata theory (it might be helpful to have a look at [4]).

2. Find a design scenario of interest to which our contract framework applies and demonstrate how they can be implemented. Some examples are autonomous valet parking service with non-cooperative human drivers, supervisory controller to vehicle communication subsystems. For a more concrete example, see [2]. Students interested in this version of the project should have a good knowledge of control theory. Experience with implementing controllers and generating simulations is highly valued.

Both versions require programming experience. The student is expected to know Python or to have enough programming experience to learn it in a short time.

## 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] 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

[3] https://www.learntla.com/introduction/

[4] Raclet, Jean-Baptiste, et al. "A modal interface theory for component-based design." Fundamenta Informaticae 108.1-2 (2011): 119-149.