On 29.11.23 09:13, Sebastian Huber wrote:
On 28.11.23 20:49, andrew.butterfi...@scss.tcd.ie wrote:
+ scenario
+ In a setting that involves many concurrent tasks that
interleave in arbitrary
+ ways, a scenario describes a single specific possible
interleaving. One
+ interpretation of the behaviour of a concurrent system is
the set of all its
+ scenarios.
+
This doesn't cover the common use case of a test scenario which is
usually
less about threading and more about values and using a set of methods in
a particular manner.
In the context in which Sebastian asked me for this entry, the term
`scenario` is used as described above.
But you are right that there are nuances here. In the Promela/SPIN
based test-generation work, each
counter example we get from SPIN describes a scenario as defined
above, and we generate C test code
that reproduces that scenario, including the precise interleaving of
the tasks as per that scenario.
The term scenario is used a lot in the formal verification chapter, so
it should have an entry. Joel, do you have a suggestion to improve the
wording?
I added an "In the context of formal verification, ..." to the term
definition and checked it in.
--
embedded brains GmbH & Co. KG
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@embedded-brains.de
phone: +49-89-18 94 741 - 16
fax: +49-89-18 94 741 - 08
Registergericht: Amtsgericht München
Registernummer: HRB 157899
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
Unsere Datenschutzerklärung finden Sie hier:
https://embedded-brains.de/datenschutzerklaerung/
_______________________________________________
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
