db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
@InProceedings{OHalloran08,
title = "{H}ow to {S}oar with {CSP}",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
author= "O'Halloran, Colin",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
editor= "Welch, Peter H. and Stepney, S. and Polack, F.A.C and Barnes, Frederick R. M. and McEwan, Alistair A. and Stiles, G. S. and Broenink, Jan F. and Sampson, Adam T.",
db_connect: Could not connect to paper db at "wotug@dragon.kent.ac.uk"
pages = "15--15",
booktitle= "{C}ommunicating {P}rocess {A}rchitectures 2008",
isbn= "978-1-58603-907-3",
year= "2008",
month= "sep",
abstract= "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:
\textlessul\textgreater
\textlessli\textgreatera
language subset for Soar, designed for formal
analysis;
\textlessli\textgreatera formal model of the Soar
subset written in CSP;
\textlessli\textgreatera prototype
translator \textquotedblSoar2Csp\textquotedbl from Soar to
the CSP model;
\textlessli\textgreatera framework for static
analysis of Soar agents through model
checking using
FDR2;
\textlessli\textgreaterthe identification of
\textquotedblhealthiness conditions\textquotedbl required of
any
Soar Agent;
\textlessli\textgreatera verifiable
implementation of the CSP based Soar agents on
an
FPGA.
\textless/ul\textgreater"
}