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 email@example.com http://lists.psas.pdx.edu/mailman/listinfo/psas-avionics