Re: Using model checking to do test generation for RTEMS

Dear Chris, > On 7 Sep 2020, at 04:21, Chris Johns wrote: > > ... stuff deleted ... >>> How is the log from the test output used to validate the model? >> >> The test output shows what the test did, so it can be used by someone >> familiar >> with the >> requirements to judge if the test ex

Re: Using model checking to do test generation for RTEMS

On 4/9/20 7:35 pm, Andrew Butterfield wrote: > Dear Chris, > >  thanks for your feedback - much appreciated! > > Responses to your queries inline below. > >> On 3 Sep 2020, at 00:38, Chris Johns > > wrote: >> >> On 1/9/20 2:30 am, Andrew Butterfield wrote: >>> Dear all,

Re: Using model checking to do test generation for RTEMS

Dear Chris, thanks for your feedback - much appreciated! Responses to your queries inline below. > On 3 Sep 2020, at 00:38, Chris Johns wrote: > > On 1/9/20 2:30 am, Andrew Butterfield wrote: >> Dear all, >> >> I am involved the in the ESA sponsored project RTEMS-SMP, to add >> tools and da

Re: Using model checking to do test generation for RTEMS

On 1/9/20 2:30 am, Andrew Butterfield wrote: > Dear all, > > I am involved the in the ESA sponsored project RTEMS-SMP, to add > tools and data for software qualification. Our focus is on the use > of formal techniques to assist in software verification. Excellent :) > We have a developed a pr