Open AccessDescription of Command and Control Networks in Coq
Author(s) -
Guilherme G. F. da Silva,
Edward Hermann Hæusler,
Cláudia Nalon
Publication year - 2021
Language(s) - English
Resource type - Conference proceedings
DOI - 10.5753/weit.2021.18923
Subject(s) - computer science , correctness , usability , simple (philosophy) , proof assistant , representation (politics) , control (management) , programming language , ranking (information retrieval) , command and control , theoretical computer science , artificial intelligence , human–computer interaction , mathematics , mathematical proof , philosophy , geometry , epistemology , political science , telecommunications , politics , law
A command and control (C2) system can be defined as a group of individuals organised hierarchically in which higher-ranking individuals can issuedirections to their subordinates with a certain goal in mind. We present a model for representation of command and control networks in the Coq proof assistant based on a tree data structure. Our model utilises Coq’s implementation of data structures and includes examples of how to define functions and properties that may be relevant in a C2 system, as well as examples of some of the tests we have performed to verify the correctness and usability of our model. The examples given here are simple, but constitute basic blocks that can later be used in more realistic formalisations.