Task analysis and design plans in formal specification design

This paper presents BENTON, a prototype system demonstrating task analysis and multi-agent reasoning applied to formal specification synthesis. BENTON transforms specifications written as attribute-value pairs into Larch Modula-3 interface language and Larch Shared Language specifications. BENTON decomposes the software specification design task into synthesis, analysis and evaluation subtasks. Each subtask is assigned a specific design method based on problem and domain characteristics. This task analysis is achieved using blackboard knowledge sources and multi-agent reasoning employing design plans to implement different problem solving methods. Knowledge sources representing different problem solving methodologies monitor blackboard spaces and activate when they are applicable. When executed, Design plans send subtasks to agents that select from available problem solving methodologies. BENTON agents and knowledge sources use case-based reasoning, schemata-based reasoning and procedure execution as their fundamental reasoning methods. This paper presents an overview of the BENTON design model, its agent architecture and plan execution capabilities, and two annotated examples of BENTON problem solving activities.