Description of Command and Control Networks in Coq

• Guilherme G. F. da Silva Pontifícia Universidade Católica do Rio de Janeiro (PUC-RIO)
• Edward Hermann Haeusler Pontifícia Universidade Católica do Rio de Janeiro (PUC-RIO) http://orcid.org/0000-0002-4999-7476
• Cláudia Nalon Universidade de Brasília (UnB) http://orcid.org/0000-0002-9792-5346

DOI: https://doi.org/10.5753/weit.2021.18923

Resumo

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.

Palavras-chave: Formal especification, Formal verification, Coq

Referências

Development, Concepts and Doctrine Centre (2017). Future of command and control. Joint Concept Notes, 17(2).

Nato Terminology Office (2021). Natoterm. https://nso.nato.int/natoterm/content/nato/pages/home.html?lg=en. Last visited: 17-Sep-2021.

Owre, S. (2020). PVS 7.1, The Prototype Verification System. https://pvs.csl.sri.com/.

van de Pol, J., Hooman, J., and Jong, E. (1998). Formal requirements specification for command and control systems. In In Proceedings of the Conference on Engineering of Computer Based Systems, pages 37–44. IEEE.

Silva, Guilherme (2021). Source code. http://github.com/GGFSilva/CommandAndControl/.

The Coq Team (2021). Coq 8.13. https://coq.inria.fr/.

Wang, J. (2012). Timed Petri Nets: Theory and Application. The International Series on Discrete Event Dynamic Systems. Springer US.