%T How to Soar with CSP
%A  Colin O\[rs]Halloran
%E Peter H. Welch,  S. Stepney,  F.A.C Polack,  Frederick R. M. Barnes,  Alistair A. McEwan,  G. S. Stiles,  Jan F. Broenink,  Adam T. Sampson
%B Communicating Process Architectures 2008
%X In this talk, I shall discuss work on the necessary
   technology
required for flight clearance of Autonomous
   Aircraft employing
Agents by reducing the certification
   problem to small verifiable
steps that can be carried out by
   a machine. The certification of
such Agents falls into two
   parts: the validation of the safety of
the Agent; and the
   verification of the implementation of the agent.
The work
   focuses on the Soar agent language and the main results
   are:
<ul>
<li>a language subset for Soar, designed for
   formal analysis;
<li>a formal model of the Soar subset
   written in CSP;
<li>a prototype translator
   \[dq]Soar2Csp\[dq] from Soar to the CSP model;
<li>a
   framework for static analysis of Soar agents through
   model
checking using FDR2;
<li>the identification of
   \[dq]healthiness conditions\[dq] required of any
Soar
   Agent;
<li>a verifiable implementation of the CSP based Soar
   agents on an
FPGA.
</ul>