Name
Abstract | ||
|---|---|---|
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 cisst software package. This strategy is not specific to cisst and can be applied to other packages. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1109/ICRA.2012.6225285 | Robotics and Automation |
Keywords | Field | DocType |
control engineering computing,formal logic,formal verification,multi-threading,object-oriented programming,public domain software,robots,software packages,software reusability,HLRG,History for Local Rely/Guarantee,component-based software,concurrent robot software,formal methods,lock-free mechanisms,multithreaded software,mutexes,mutual exclusion primitives,open source cisst software package,performance gains,program logic,real-time performance requirements,robot software developers,semaphores,software reusability | Programming language,Software engineering,Computer science,Package development process,Correctness,Software,Robot software,Formal methods,Software verification and validation,Software construction,Formal verification | Conference |
Volume | Issue | ISSN |
2012 | 1 | 1050-4729 E-ISBN : 978-1-4673-1404-6 |
ISBN | Citations | PageRank |
978-1-4673-1404-6 | 1 | 0.44 |
References | Authors | |
13 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Peter Kazanzides | 1 | 584 | 96.63 |
| Yanni Kouskoulas | 2 | 24 | 3.83 |
| Anton Deguet | 3 | 124 | 18.83 |
| Zhong Shao | 4 | 897 | 68.80 |