|
Published Articles >> Table of Contents >> Abstract
Sixth IEEE International Conference on Complex Computer Systems (ICECCS'00)
p. 0072
Experience Using Formal Methods for Specifying a Multi-Agent System
C. Rouff, NASA Goddard Space Flight Center, Greenbelt, MD, USA
J. Rash, NASA Goddard Space Flight Center, Greenbelt, MD, USA
M.G. Hinchey, NASA Goddard Space Flight Center, Greenbelt, MD, USA
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICECCS.2000.873929
Send link to a friend
| Abstract |
|
Abstract: The process and results of using formal methods to specify the Lights Out Ground Operations System (LOGOS) are presented. LOGOS is a prototype multi agent system developed to demonstrate the feasibility of providing autonomy to satellite ground operations functions at NASA Goddard Space Flight Center (GSFC). Following the initial implementation of LOGOS, the development team decided to use formal methods to check for race conditions, deadlocks and omissions. The specification exercise revealed several omissions as well as race conditions. After completing the specification, the team concluded that certain tools would have made the specification process easier. The paper gives a sample specification of two of the agents in the LOGOS system and examples of omissions and race conditions found.
|
 Additional Information
|
Index Terms- formal specification; formal methods; multi-agent system specification; Lights Out Ground Operations System; LOGOS; prototype multi agent system; satellite ground operations functions; NASA Goddard Space Flight Center; GSFC; development team; race conditions; deadlocks; omissions; specification exercise; specification process; sample specification
Citation:
C. Rouff, J. Rash, M.G. Hinchey,
"Experience Using Formal Methods for Specifying a Multi-Agent System,"
iceccs,
p. 0072,
Sixth IEEE International Conference on Complex Computer Systems (ICECCS'00),
2000
|
|
