Executable specifications for agent systems using the extended Descartes specification language with tool support
Vinitha Hannah Subburaj · ThinkTech (Texas Tech University) · 2013
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 research effort defines the need of applying formal methods while specifying and developing software systems and the benefits over traditional methods of software development. 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. Discrete and concrete functions of agents with a high-level of abstraction details were specified using the extended Descartes specification language. Tool support for executing the specifications written using the extended Descartes specification language in order to verify the correctness of the specification was developed in Java. Concepts of agent oriented system design were adopted from the Gaia methodology for agent oriented analysis and design. A concrete agent architecture with a generalized notation for formally specifying agent oriented systems was defined in this research effort. The tool support for executing the extended Descartes specification language incorporated the latest technologies to efficiently facilitate the execution of specifications. Effective design, implementation, and evaluation of the agent oriented extensions to the Descartes language processor have been achieved by this research effort. The integration of formally specifying complex systems using agent oriented technology with the extended Descartes language constructs and executing the specifications using the tool support will impact the current traditional ways of specifying software systems. Also, the research effort will bridge the gap between the specification, design, and the implementation phases of software development.