Please help transcribe this video using our simple transcription tool. You need to be logged in to do so.
Component-based software has been proposed as a methodology for improving software reuse and has increasingly been adopted by robot software developers. At the same time, robot systems typically have real-time performance requirements and performance gains can often be obtained by multi-threading. It is challenging, however, to create correct multi-threaded software, especially when standard mutual exclusion primitives, such as mutexes and semaphores, are eschewed in favor of more efficient, lock-free mechanisms. It is even more difficult to find these errors, as they can remain dormant for years until triggered by just the "right" conditions. Our approach, therefore, is to apply Formal Methods to reason about the correctness of these mechanisms. As a first step, we adopted a recently-developed program logic called History for Local Rely/Guarantee (HLRG) and applied it to prove the correctness (after first finding and fixing an error) of one such mechanism in the open source <i>cisst</i> software package. This strategy is not specific to <i>cisst</i> and can be applied to other packages.
Questions and AnswersYou need to be logged in to be able to post here.