A formal specification language for modeling agent systems

Formal methods in software specification enable the development of reliable software with a reduction in magnitude of unidentified errors that might occur while developing software systems. The state of the practice with regards to formal methods in software specification, as well as in other phases of the software life cycle, is not clear and well defined since the field is still immature. This paper defines the need for applying formal methods while specifying and developing software systems. The Descartes specification language, a formal executable specification language, was taken into study to specify software systems. A description of agent oriented systems along with the extended constructs of the Descartes specification language for specifying agent systems was defined in this research. A concrete agent architecture with a generalized notation for formally specifying agent oriented systems was defined in this paper. The integration of formally specifying complex systems using agent oriented technology with the extended Descartes language constructs will impact the current ways of specifying software systems. Also, the paper can help bridge the gap between the specification, design, and the implementation phases of software development.