Reasoning over Test Specifications using Assume-Guarantee Contracts - Revision history

Murray at 17:10, 7 January 2023

2023-01-07T17:10:59Z

← Older revision		Revision as of 17:10, 7 January 2023
Line 4:		Line 4:
	\|Source=Submitted, NASA Formal Methods (NFM), 2023		\|Source=Submitted, NASA Formal Methods (NFM), 2023
	\|Abstract=We establish a framework to reason about test campaigns described formally. First, we introduce the notion of a test structure — an object that carries i) the formal specifications of the system under test, and ii) the test objective, which is specified by a test engineer. We build on test structures to define test campaigns and specifications for the tester. Secondly, we use the algebra of assume-guarantee contracts to reason about constructing tester specifications, comparing test struc- tures and test campaigns, and combining and splitting test structures. Using the composition operator, we characterize the conditions on the constituent tester specifications and test objectives for feasibly combin- ing test structures. We illustrate the different applications of the quotient operator to split the test objective, the system into subsystems, or both. Finally, we illustrate test executions corresponding to the combined and split test structures in a discrete autonomous driving example and an aircraft formation-flying example. We anticipate that reasoning over test specifications would aid in generating optimal test campaigns.		\|Abstract=We establish a framework to reason about test campaigns described formally. First, we introduce the notion of a test structure — an object that carries i) the formal specifications of the system under test, and ii) the test objective, which is specified by a test engineer. We build on test structures to define test campaigns and specifications for the tester. Secondly, we use the algebra of assume-guarantee contracts to reason about constructing tester specifications, comparing test struc- tures and test campaigns, and combining and splitting test structures. Using the composition operator, we characterize the conditions on the constituent tester specifications and test objectives for feasibly combin- ing test structures. We illustrate the different applications of the quotient operator to split the test objective, the system into subsystems, or both. Finally, we illustrate test executions corresponding to the combined and split test structures in a discrete autonomous driving example and an aircraft formation-flying example. We anticipate that reasoning over test specifications would aid in generating optimal test campaigns.
	\|URL=~~http~~://www.cds.caltech.edu/~murray/preprints/bgim23-nfm_s.pdf		\|URL=https://www.cds.caltech.edu/~murray/preprints/bgim23-nfm_s.pdf
	\|Type=Conference paper		\|Type=Conference paper
	\|ID=2023a		\|ID=2023a

Murray at 17:10, 7 January 2023

2023-01-07T17:10:12Z

← Older revision		Revision as of 17:10, 7 January 2023
Line 4:		Line 4:
	\|Source=Submitted, NASA Formal Methods (NFM), 2023		\|Source=Submitted, NASA Formal Methods (NFM), 2023
	\|Abstract=We establish a framework to reason about test campaigns described formally. First, we introduce the notion of a test structure — an object that carries i) the formal specifications of the system under test, and ii) the test objective, which is specified by a test engineer. We build on test structures to define test campaigns and specifications for the tester. Secondly, we use the algebra of assume-guarantee contracts to reason about constructing tester specifications, comparing test struc- tures and test campaigns, and combining and splitting test structures. Using the composition operator, we characterize the conditions on the constituent tester specifications and test objectives for feasibly combin- ing test structures. We illustrate the different applications of the quotient operator to split the test objective, the system into subsystems, or both. Finally, we illustrate test executions corresponding to the combined and split test structures in a discrete autonomous driving example and an aircraft formation-flying example. We anticipate that reasoning over test specifications would aid in generating optimal test campaigns.		\|Abstract=We establish a framework to reason about test campaigns described formally. First, we introduce the notion of a test structure — an object that carries i) the formal specifications of the system under test, and ii) the test objective, which is specified by a test engineer. We build on test structures to define test campaigns and specifications for the tester. Secondly, we use the algebra of assume-guarantee contracts to reason about constructing tester specifications, comparing test struc- tures and test campaigns, and combining and splitting test structures. Using the composition operator, we characterize the conditions on the constituent tester specifications and test objectives for feasibly combin- ing test structures. We illustrate the different applications of the quotient operator to split the test objective, the system into subsystems, or both. Finally, we illustrate test executions corresponding to the combined and split test structures in a discrete autonomous driving example and an aircraft formation-flying example. We anticipate that reasoning over test specifications would aid in generating optimal test campaigns.
	\|URL=http://~~murray~~.cds.caltech.edu/preprints/bgim23-nfm_s.pdf		\|URL=http://www.cds.caltech.edu/~murray/preprints/bgim23-nfm_s.pdf
	\|Type=Conference paper		\|Type=Conference paper
	\|ID=2023a		\|ID=2023a

Murray: Created page with "{{Paper |Title=Reasoning over Test Specifications using Assume-Guarantee Contracts |Authors=Apurva Badithela, Josefine B. Graebener, Inigo Incer, and Richard M. Murray |Source=Submitted, NASA Formal Methods (NFM), 2023 |Abstract=We establish a framework to reason about test campaigns described formally. First, we introduce the notion of a test structure — an object that carries i) the formal specifications of the system under test, and ii) the test objective, which is..."

2023-01-07T17:07:44Z

Created page with "{{Paper |Title=Reasoning over Test Specifications using Assume-Guarantee Contracts |Authors=Apurva Badithela, Josefine B. Graebener, Inigo Incer, and Richard M. Murray |Source=Submitted, NASA Formal Methods (NFM), 2023 |Abstract=We establish a framework to reason about test campaigns described formally. First, we introduce the notion of a test structure — an object that carries i) the formal specifications of the system under test, and ii) the test objective, which is..."

New page

{{Paper
|Title=Reasoning over Test Specifications using Assume-Guarantee Contracts
|Authors=Apurva Badithela, Josefine B. Graebener, Inigo Incer, and Richard M. Murray
|Source=Submitted, NASA Formal Methods (NFM), 2023
|Abstract=We establish a framework to reason about test campaigns described formally. First, we introduce the notion of a test structure — an object that carries i) the formal specifications of the system under test, and ii) the test objective, which is specified by a test engineer. We build on test structures to define test campaigns and specifications for the tester. Secondly, we use the algebra of assume-guarantee contracts to reason about constructing tester specifications, comparing test struc- tures and test campaigns, and combining and splitting test structures. Using the composition operator, we characterize the conditions on the constituent tester specifications and test objectives for feasibly combin- ing test structures. We illustrate the different applications of the quotient operator to split the test objective, the system into subsystems, or both. Finally, we illustrate test executions corresponding to the combined and split test structures in a discrete autonomous driving example and an aircraft formation-flying example. We anticipate that reasoning over test specifications would aid in generating optimal test campaigns.
|URL=http://murray.cds.caltech.edu/preprints/bgim23-nfm_s.pdf
|Type=Conference paper
|ID=2023a
|Tag=bgim23-nfm
|Funding=AFOSR T&E
}}