Digital Library[ Search Result ]
Memory Model Design for Integer-Pointer Casting Support in C-like languages Via Dual Non-determinism
http://doi.org/10.5626/JOK.2024.51.7.643
In system programming, pointers are essential elements. However, applying formal verification methods to programs involving integer-pointer casting poses an important challenge. To address this challenge, a mathematically defined memory model that supports integer-pointer casting, along with proof techniques for verification, is necessary. This study presents a memory model that supports integer-pointer casting within the Coq proof assistant. The model accommodates patterns associated with integer-pointer operations, including one-past-the-end pointers. Additionally, a simulation-based proof technique is introduced, which enables the utilization of the model for program verification. The adequacy of this technique is established through proof. To validate the effectiveness of the approach, the defined memory model is integrated into CompCert, a verified C compiler, replacing its original memory model. Subsequently, two proofs of CompCert's optimization verification are updated using the simulation technique. It is anticipated that the proposed memory model will find applications in program and compiler verification tasks involving integer-pointer operations.
Formal Model Design for Network and Operating System Behaviors in Real-time Distributed System Verification with Coq
http://doi.org/10.5626/JOK.2020.47.11.1071
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.
A Design of Effective Inference Methods and Their Application Guidelines for Supporting Various Medical Analytics Schemes
Moon Kwon Kim, Hyun Jung La, Soo Dong Kim
As a variety of personal medical devices appear, it is possible to acquire a large number of diverse medical contexts from the devices. There have been efforts to analyze the medical contexts via software applications. In this paper, we propose a generic model of medical analytics schemes that are used by medical experts, identify inference methods for realizing each medical analytics scheme, and present guidelines for applying the inference methods to the medical analytics schemes. Additionally, we develop a PoC inference system and analyze real medical contexts to diagnose relevant diseases so that we can validate the feasibility and effectiveness of the proposed medical analytics schemes and guidelines of applying inference methods.
Search
Journal of KIISE
- ISSN : 2383-630X(Print)
- ISSN : 2383-6296(Electronic)
- KCI Accredited Journal
Editorial Office
- Tel. +82-2-588-9240
- Fax. +82-2-521-1352
- E-mail. chwoo@kiise.or.kr