Name
Abstract | ||
|---|---|---|
While autonomous systems offer great promise in terms of capability and flexibility their reliability is particularly hard to assess. This paper describes research to apply formal verification methods to languages used to develop autonomy software. In particular we describe tools that automatically convert autonomy software into formal models that are then verified using model checking. This approach has been applied to MPL code for the Livingstone fault diagnosis system and to TDL task descriptions for mobile robot systems. Our long-term objective is to create tools that enable engineers and roboticists to use formal verification as part of the normal software development cycle. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1109/IROS.2000.893218 | 2000 IEEE/RSJ INTERNATIONAL CONFERENCE ON INTELLIGENT ROBOTS AND SYSTEMS (IROS 2000), VOLS 1-3, PROCEEDINGS |
Keywords | Field | DocType |
mobile robots,autonomous systems,mobile robot,model checking,software systems,software development,application software,formal verification,testing | Model checking,Software engineering,Computer science,Software system,Control engineering,Software,Software development process,Formal methods,Software verification and validation,Embedded system,Software verification,Formal verification | Conference |
Citations | PageRank | References |
12 | 1.62 | 12 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Reid G. Simmons | 1 | 4114 | 562.20 |
| Charles Pecheur | 2 | 284 | 28.50 |
| Grama Srinivasan | 3 | 12 | 1.62 |