Hello Rafael!

On Mon, Mar 30, 2009 at 12:29 AM, Rafael Medaglia
<rafael.medag...@gmail.com> wrote:
> ... my dissertation is about the use of model checking in an
> implementation of the communication protocol proposed by the CCSDS.

Cool! Good luck.

> I’d like to work with model checking and Barton C Massey mentioned
> that the core avionics SW and SW in the microcontrollers nodes could
> use some verification in the safety properties.
>
> I’d really appreciate if you (1) could give me some directions about
> where you believe model checking better fits in the project (core
> avionics, microcontrollers nodes or somewhere else),

Bart knows more about model checking than most anyone I know, but since
I only have the general idea I may not have a very good answer here.
I'll try anyway...

I think it's most important to capture the knowledge different team
members have about what kinds of failures can occur, and make sure the
software can detect them and respond appropriately.

Would you be willing to help interview the folks on our team and produce
a report on the known failure modes as part of your project? We don't
currently have that written down as far as I know, though several of us
have in our heads partial lists of things to worry about.

We have ad-hoc models of how the control software should handle both
normal and failure cases. For example, see:
        http://psas.pdx.edu/FlightComputerStateFlowSep2003/
If we had the failure modes of concern, then you could use model
checking to verify whether the above state flow produces the response we
want in each failure case, right? That would be a useful result, and
might be a reasonable target for Summer of Code.

If you have more time after that--and I kind of hope you would--then
perhaps you could help us design a new model that fits better with our
new Bayesian Particle Filter control loop, while verifying that it meets
the safety goals. I'm not satisfied with the state-machine architecture
we've been using since it requires the flight computer to observe
measurements at the time of every state transition, and I'd like to be
able to handle a reboot in mid-flight.

> (2) some guidelines about where to get extra documentation,

We have a ton of material on our web site, at http://psas.pdx.edu/, and
our mailing list archives sometimes have answers we haven't captured on
the web site.

> I subscribed in the list (avionics) and started reading the
> lv2_avionics_design.pdf.

That's a good start. If you want to look over our current flight
computer and simulator code, it's in our event-driven-fc repo. You can
browse it on the web or pull down a copy; see
        http://psas.pdx.edu/git/

Jamey

_______________________________________________
psas-avionics mailing list
psas-avionics@lists.psas.pdx.edu
http://lists.psas.pdx.edu/mailman/listinfo/psas-avionics

Reply via email to