TY  - JOUR
T1  - Formal Model Design for Network and Operating System Behaviors in Real-time Distributed System Verification with Coq
AU  - Kim, Yoonseung 
AU  - Hur, Chung-Kil 
JO  - Journal of KIISE, JOK
PY  - 2020
DA  - 2020/1/14
DO  - 10.5626/JOK.2020.47.11.1071
KW  - software formal verification
KW  - distributed systems
KW  - real-time systems
KW  - formal model
AB  - Improving the safety and reliability of distributed systems using formal verification methods is an urgent problem. As many of these distributed systems are safety-critical, such as medical or avionics systems, failures of these systems may cause catastrophic results. However, applying formal verification to distributed systems requires not only execution semantics in software, but also behavioral models of the environments, including the operating systems and network involved. We designed a formal abstract model of network and operating system behaviors with the Coq proof assistant. This model consists of local-site execution semantics that model a single computer, the composition of these local-site semantics along with a message exchange model constitutes the global system semantics. We applied and tested this model to verify its applicability when used in a simple server-client system. We expect this model to be used in the verification of practical systems.