Experience using formal methods for specifying a multi-agent system

Christopher Rouff, James Rash, Michael G. Hinchey

Research output: Contribution to conferencePaperpeer-review

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 languageEnglish
Pages72-80
Number of pages9
Publication statusPublished - 2000
Externally publishedYes
EventProceedings of the 6th IEEE International Confernce on Engineering of Complex Computer Systems - Tokyo, Jpn
Duration: 11 Sep 200014 Sep 2000

Conference

ConferenceProceedings of the 6th IEEE International Confernce on Engineering of Complex Computer Systems
CityTokyo, Jpn
Period11/09/0014/09/00

Fingerprint

Dive into the research topics of 'Experience using formal methods for specifying a multi-agent system'. Together they form a unique fingerprint.

Cite this