{"id":634,"date":"2018-02-07T10:46:20","date_gmt":"2018-02-07T10:46:20","guid":{"rendered":"https:\/\/blogs.ncl.ac.uk\/andreymokhov\/?p=634"},"modified":"2018-02-07T17:41:31","modified_gmt":"2018-02-07T17:41:31","slug":"spacecraft-control","status":"publish","type":"post","link":"https:\/\/blogs.ncl.ac.uk\/andreymokhov\/spacecraft-control\/","title":{"rendered":"Formal verification of spacecraft control programs"},"content":{"rendered":"

Last February I spent two weeks in Vienna, visiting Jakob Lechner and RUAG Space Austria, a company developing components for space missions. Jakob and his colleagues designed a specialised processing core called REDFIN (REDuced instruction set for Fixed-point & INteger arithmetic) for executing simple spacecraft control tasks, such as satellite antenna pointing. During the visit I implemented a prototype of a formal verification framework to support the development of REDFIN programs. Afterwards I was quite busy with my<\/a> other<\/a> projects<\/a>, but my PhD student Georgy Lukyanov helped to further improve the prototype.<\/p>\n

Jakob, Georgy and I have just submitted a conference paper<\/a> describing the REDFIN core and the verification framework.\u00a0Please have a look and let us know what you think. This will be a timely read after yesterday’s exciting SpaceX launch.<\/p>\n

<\/p>\n

As we all know, writing programs is easy. Writing correct programs on the other hand is very hard. And if you are writing a program for a space mission you better be sure it is correct. So, what can you realistically do? Of course you should write and\/or generate a lot of tests, but tests do not provide the full correctness guarantee. You can also use a strongly typed programming language and prove some properties at compile time, but your space-grade processor is highly unlikely to be a well-supported compilation target (and you might not be able to take your favourite garbage collector to space — it’s way too heavy!). You could also use formal methods and develop programs with the help of a theorem prover, eventually refining an abstract specification down to the level of bare metal. That might take you years though, especially if you have no previous experience in formal methods.<\/p>\n

When I was working on my PhD I did some work on formal specification of processors and instruction sets, so this is a long-time interest of mine. Hence, when I heard about the REDFIN project I immediately self-invited myself to RUAG Space Austria and tried to figure out a way to engineer a simple solution that can be integrated into the existing development and verification workflow without a big disruption and a steep learning curve. Eventually I used Haskell to implement a small DSL for capturing the semantics of REDFIN programs and connected it to an SMT solver using\u00a0SBV<\/a>, a wonderful symbolic verification library developed by Levent Erkok (huge thanks!). This idea is not new and we reference a few early papers that developed and applied it to\u00a0Arm<\/a>\u00a0and\u00a0Intel<\/a>\u00a0processors. I also got a lot of inspiration from this blog post<\/a> by Stephen Diehl and this talk<\/a> by Tikhon Jelvis. Thank you Stephen and Tikhon!<\/p>\n

P.S.: The code is not yet available, but I hope we’ll release it soon.<\/p>\n","protected":false},"excerpt":{"rendered":"

Last February I spent two weeks in Vienna, visiting Jakob Lechner and RUAG Space Austria, a company developing components for space missions. Jakob and his colleagues designed a specialised processing core called REDFIN (REDuced instruction set for Fixed-point & INteger arithmetic) for executing simple spacecraft control tasks, such as satellite antenna pointing. During the visit … Continue reading Formal verification of spacecraft control programs<\/span> →<\/span><\/a><\/p>\n","protected":false},"author":1174,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[6,12],"tags":[4],"class_list":["post-634","post","type-post","status-publish","format-standard","hentry","category-coding","category-research","tag-haskell"],"_links":{"self":[{"href":"https:\/\/blogs.ncl.ac.uk\/andreymokhov\/wp-json\/wp\/v2\/posts\/634","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/blogs.ncl.ac.uk\/andreymokhov\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/blogs.ncl.ac.uk\/andreymokhov\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/blogs.ncl.ac.uk\/andreymokhov\/wp-json\/wp\/v2\/users\/1174"}],"replies":[{"embeddable":true,"href":"https:\/\/blogs.ncl.ac.uk\/andreymokhov\/wp-json\/wp\/v2\/comments?post=634"}],"version-history":[{"count":32,"href":"https:\/\/blogs.ncl.ac.uk\/andreymokhov\/wp-json\/wp\/v2\/posts\/634\/revisions"}],"predecessor-version":[{"id":666,"href":"https:\/\/blogs.ncl.ac.uk\/andreymokhov\/wp-json\/wp\/v2\/posts\/634\/revisions\/666"}],"wp:attachment":[{"href":"https:\/\/blogs.ncl.ac.uk\/andreymokhov\/wp-json\/wp\/v2\/media?parent=634"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.ncl.ac.uk\/andreymokhov\/wp-json\/wp\/v2\/categories?post=634"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.ncl.ac.uk\/andreymokhov\/wp-json\/wp\/v2\/tags?post=634"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}