Abstract
The process and results of using formal methods to specify the Lights Out Ground Operations System (LOGOS) are presented in this paper. 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. This paper gives a sample specification of two of the agents in the LOGOS system and examples of omissions and race conditions found.
Original language | English |
---|---|
Pages | 72-80 |
Number of pages | 9 |
Publication status | Published - 2000 |
Externally published | Yes |
Event | Proceedings of the 6th IEEE International Confernce on Engineering of Complex Computer Systems - Tokyo, Jpn Duration: 11 Sep 2000 → 14 Sep 2000 |
Conference
Conference | Proceedings of the 6th IEEE International Confernce on Engineering of Complex Computer Systems |
---|---|
City | Tokyo, Jpn |
Period | 11/09/00 → 14/09/00 |