Specification, Validation, and Synthesis of Email Agent Controllers: A Case Study in Function Rich Reactive System Design

With a few exceptions, previous formal methods for reactive system analysis have focused on finite state machines represented in terms of boolean states and boolean next-state functions. By contrast, in many reactive system domains requirements engineers and developers think in terms of complex data types and expressive next-state functions. Formal methods for reactive system design must be extended to meet their needs as well. I term a reactive system function rich if expressing its state, next-state function, or output function naturally requires this higher expressive power. ISAT, a prototype formal-methods based tool environment, is intended to assist in the creation and validation of function rich reactive systems. This paper describes a case study I have carried out using ISAT to design, validate, synthesize, and evolve controllers for the email agent components making up a novel spam-free email system that I deployed in a user trial in July 1999. The trial has been running since, with high availability, through several evolutionary specification changes and resulting software releases. The case study illustrates the use of a mix of validation techniques, from scenario simulation and coverage through static analysis and theorem proving, and discusses the value each technique adds. In addition to summarizing ISAT and the trial, this paper discusses tool requirements placed by the domain and task, the simple and powerful platform/controller/pure-functions software architecture of the components, and lessons learned.