SURF 2018: Contract-based Design of Control Systems - Revision history

Tmphan at 07:00, 19 December 2017

2017-12-19T07:00:13Z

← Older revision		Revision as of 07:00, 19 December 2017
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 ([4] ~~might be useful~~).		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.

Tmphan: /* Description */

2017-12-19T06:55:51Z

Description

← Older revision		Revision as of 06:55, 19 December 2017
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 ([4] might be useful).

	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.

Tmphan: /* References */

2017-12-19T06:54:44Z

References

← Older revision		Revision as of 06:54, 19 December 2017
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.

Tmphan at 20:31, 8 December 2017

2017-12-08T20:31:24Z

← Older revision		Revision as of 20:31, 8 December 2017
Line 1:		Line 1:

	'''[[SURF 2018\|2018 SURF]]: project description'''		'''[[SURF 2018\|2018 SURF]]: project description'''
	* Mentor: Richard M. Murray		* Mentor: Richard M. Murray
Line 16:		Line 17:

	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.		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.
			[[File:AVP_contracts.png\|500px\|left]]
	[[File:AVP_contracts.png\|~~400px~~\|left]]

	==References==		==References==

Tmphan at 20:27, 8 December 2017

2017-12-08T20:27:47Z

← Older revision		Revision as of 20:27, 8 December 2017
Line 2:		Line 2:
	* Mentor: Richard M. Murray		* Mentor: Richard M. Murray
	* Co-mentor: Tung Phan		* 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.		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		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

			[[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.
Line 13:		Line 17:
	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.		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		[[File:AVP_contracts.png\|400px\|left]]

			==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〉		[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〉

Tmphan: Created page with "'''2018 SURF: project description''' * Mentor: Richard M. Murray * Co-mentor: Tung Phan As systems grow in scale and complexity, a modular approach to design be..."

2017-12-08T20:11:10Z

Created page with "'''2018 SURF: project description''' * Mentor: Richard M. Murray * Co-mentor: Tung Phan As systems grow in scale and complexity, a modular approach to design be..."

New page

'''[[SURF 2018|2018 SURF]]: project description'''
* Mentor: Richard M. Murray
* Co-mentor: Tung Phan

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.

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/