Layering assume-guarantee contracts for hierarchical system design - Revision history

Murray at 20:15, 8 June 2019

2019-06-08T20:15:24Z

← Older revision		Revision as of 20:15, 8 June 2019
Line 2:		Line 2:
	\|Title=Layering assume-guarantee contracts for hierarchical system design		\|Title=Layering assume-guarantee contracts for hierarchical system design
	\|Authors=Ioannis Filippidis and Richard M. Murray		\|Authors=Ioannis Filippidis and Richard M. Murray
	\|Source=~~To appear,~~ <i>Proceedings of the IEEE</i>, 2018		\|Source=<i>Proceedings of the IEEE</i>, 2018
	\|Abstract=Specifications for complex engineering systems are typically decomposed into specifications for individual subsystems in a manner that ensures they are implementable and simpler to develop further. We describe a method to algorithmically construct component specifications that implement a given specification when assembled. By eliminating variables that are irrelevant to realizability of each component, we simplify the specifications and reduce the amount of information necessary for operation. We parametrize the information flow between components by introducing parameters that select whether each variable is visible to a component or not. The decomposition algorithm identifies which variables can be hidden while pre- serving realizability and ensuring correct composition, and these are eliminated from component specifications by quantification and conversion of binary decision diagrams to formulas. The resulting specifications describe component viewpoints with full information with respect to the remaining variables, which is essential for tractable algorithmic synthesis of implementations. The specifications are written in TLA+, with liveness properties restricted to an implication of conjoined recurrence properties, known as GR(1). We define an operator for forming open systems from closed systems, based on a variant of the “while-plus” operator. This operator simplifies the writing of specifications that are realizable without being vacuous. To convert the generated specifications from binary decision diagrams to readable formulas over integer variables, we symbolically solve a minimal covering problem. We show with examples how the method can be applied to obtain contracts that formalize the hierarchical structure of system design.		\|Abstract=Specifications for complex engineering systems are typically decomposed into specifications for individual subsystems in a manner that ensures they are implementable and simpler to develop further. We describe a method to algorithmically construct component specifications that implement a given specification when assembled. By eliminating variables that are irrelevant to realizability of each component, we simplify the specifications and reduce the amount of information necessary for operation. We parametrize the information flow between components by introducing parameters that select whether each variable is visible to a component or not. The decomposition algorithm identifies which variables can be hidden while pre- serving realizability and ensuring correct composition, and these are eliminated from component specifications by quantification and conversion of binary decision diagrams to formulas. The resulting specifications describe component viewpoints with full information with respect to the remaining variables, which is essential for tractable algorithmic synthesis of implementations. The specifications are written in TLA+, with liveness properties restricted to an implication of conjoined recurrence properties, known as GR(1). We define an operator for forming open systems from closed systems, based on a variant of the “while-plus” operator. This operator simplifies the writing of specifications that are realizable without being vacuous. To convert the generated specifications from binary decision diagrams to readable formulas over integer variables, we symbolically solve a minimal covering problem. We show with examples how the method can be applied to obtain contracts that formalize the hierarchical structure of system design.
	\|URL=http://www.cds.caltech.edu/~murray/preprints/fm18-pieee.pdf		\|URL=http://www.cds.caltech.edu/~murray/preprints/fm18-pieee.pdf
Line 9:		Line 9:
	\|Tag=fm18-pieee		\|Tag=fm18-pieee
	\|Funding=SRC TerraSwarm		\|Funding=SRC TerraSwarm
			\|Flags=NCS
	}}		}}

Murray at 06:04, 15 July 2018

2018-07-15T06:04:16Z

← Older revision		Revision as of 06:04, 15 July 2018
Line 2:		Line 2:
	\|Title=Layering assume-guarantee contracts for hierarchical system design		\|Title=Layering assume-guarantee contracts for hierarchical system design
	\|Authors=Ioannis Filippidis and Richard M. Murray		\|Authors=Ioannis Filippidis and Richard M. Murray
	\|Source=~~Submitted~~, <i>Proceedings of the IEEE</i>, ~~Jul 2017~~		\|Source=To appear, <i>Proceedings of the IEEE</i>, 2018
	\|Abstract=Specifications for complex engineering systems are typically decomposed into specifications for individual subsystems in a manner that ensures they are implementable and simpler to develop further. We describe a method to algorithmically construct component specifications that implement a given ~~spec- ification~~ when assembled. By eliminating variables that are irrelevant to realizability of each component, we simplify the specifications and reduce the amount of information necessary for operation. ~~To identify~~ which variables can be hidden while ~~preserving~~ realizability~~, we parametrize the information flow between components~~, and ~~eliminate the selected variables~~ from component specifications. The resulting specifications describe component viewpoints with full information with respect to the remaining variables, which is essential for tractable algorithmic synthesis of implementations. The specifications are written in TLA+, with liveness properties restricted to an implication of conjoined recurrence properties, known as GR(1). We define an operator for forming open-systems from closed-systems, based on a variant of the “while-plus” operator. ~~The resulting open-system properties~~ are realizable ~~when expected to be,~~ without ~~need for separate side conditions~~. To convert the generated specifications from binary decision diagrams to readable formulas over integer variables, we symbolically solve a minimal covering problem. We show with examples how the method can be applied to obtain contracts that formalize the hierarchical structure of system design.		\|Abstract=Specifications for complex engineering systems are typically decomposed into specifications for individual subsystems in a manner that ensures they are implementable and simpler to develop further. We describe a method to algorithmically construct component specifications that implement a given specification when assembled. By eliminating variables that are irrelevant to realizability of each component, we simplify the specifications and reduce the amount of information necessary for operation. We parametrize the information flow between components by introducing parameters that select whether each variable is visible to a component or not. The decomposition algorithm identifies which variables can be hidden while pre- serving realizability and ensuring correct composition, and these are eliminated from component specifications by quantification and conversion of binary decision diagrams to formulas. The resulting specifications describe component viewpoints with full information with respect to the remaining variables, which is essential for tractable algorithmic synthesis of implementations. The specifications are written in TLA+, with liveness properties restricted to an implication of conjoined recurrence properties, known as GR(1). We define an operator for forming open systems from closed systems, based on a variant of the “while-plus” operator. This operator simplifies the writing of specifications that are realizable without being vacuous. To convert the generated specifications from binary decision diagrams to readable formulas over integer variables, we symbolically solve a minimal covering problem. We show with examples how the method can be applied to obtain contracts that formalize the hierarchical structure of system design.
	\|URL=http://www.cds.caltech.edu/~murray/preprints/~~fm17~~-~~pieee_s~~.pdf		\|URL=http://www.cds.caltech.edu/~murray/preprints/fm18-pieee.pdf
	\|Type=Journal ~~submission~~		\|Type=Journal paper
	\|ID=2017h		\|ID=2017h
	\|Tag=~~fm17~~-pieee		\|Tag=fm18-pieee
	\|Funding=SRC TerraSwarm		\|Funding=SRC TerraSwarm
	}}		}}

Murray at 02:46, 8 August 2017

2017-08-08T02:46:35Z

← Older revision		Revision as of 02:46, 8 August 2017
Line 6:		Line 6:
	\|URL=http://www.cds.caltech.edu/~murray/preprints/fm17-pieee_s.pdf		\|URL=http://www.cds.caltech.edu/~murray/preprints/fm17-pieee_s.pdf
	\|Type=Journal submission		\|Type=Journal submission
	\|ID=~~2017g~~		\|ID=2017h
	\|Tag=fm17-pieee		\|Tag=fm17-pieee
	\|Funding=SRC TerraSwarm		\|Funding=SRC TerraSwarm
	}}		}}

Murray: Created page with "{{Paper |Title=Layering assume-guarantee contracts for hierarchical system design |Authors=Ioannis Filippidis and Richard M. Murray |Source=Submitted, Proceedings of the IE..."

2017-08-08T02:44:31Z

Created page with "{{Paper |Title=Layering assume-guarantee contracts for hierarchical system design |Authors=Ioannis Filippidis and Richard M. Murray |Source=Submitted, <i>Proceedings of the IE..."

New page
{{Paper
|Title=Layering assume-guarantee contracts for hierarchical system design
|Authors=Ioannis Filippidis and Richard M. Murray
|Source=Submitted, <i>Proceedings of the IEEE</i>, Jul 2017
|Abstract=Specifications for complex engineering systems are typically decomposed into specifications for individual subsystems in a manner that ensures they are implementable and simpler to develop further. We describe a method to algorithmically construct component specifications that implement a given spec- ification when assembled. By eliminating variables that are irrelevant to realizability of each component, we simplify the specifications and reduce the amount of information necessary for operation. To identify which variables can be hidden while preserving realizability, we parametrize the information flow between components, and eliminate the selected variables from component specifications. The resulting specifications describe component viewpoints with full information with respect to the remaining variables, which is essential for tractable algorithmic synthesis of implementations. The specifications are written in TLA+, with liveness properties restricted to an implication of conjoined recurrence properties, known as GR(1). We define an operator for forming open-systems from closed-systems, based on a variant of the “while-plus” operator. The resulting open-system properties are realizable when expected to be, without need for separate side conditions. To convert the generated specifications from binary decision diagrams to readable formulas over integer variables, we symbolically solve a minimal covering problem. We show with examples how the method can be applied to obtain contracts that formalize the hierarchical structure of system design.
|URL=http://www.cds.caltech.edu/~murray/preprints/fm17-pieee_s.pdf
|Type=Journal submission
|ID=2017g
|Tag=fm17-pieee
|Funding=SRC TerraSwarm
}}