@article{MFAEFCC32,
title = "Formal Model Design for Network and Operating System Behaviors in Real-time Distributed System Verification with Coq",
journal = "Journal of KIISE, JOK",
year = "2020",
issn = "2383-630X",
doi = "10.5626/JOK.2020.47.11.1071",
author = "Yoonseung Kim,Chung-Kil Hur",
keywords = "software formal verification,distributed systems,real-time systems,formal model",
abstract = "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."
}