Digital Library[ Search Result ]
ILP-based Schedule Synthesis of Time-Sensitive Networking
Jin Hyun Kim, Hyonyoung Choi, Kyong Hoon Kim, Insup Lee, Se-Hoon Kim
http://doi.org/10.5626/JOK.2021.48.6.595
IEEE 802.1Qbv Time Sensitive Network (TSN), the latest real-time Ethernet standard, is a network designed to guarantee the temporal accuracy of streams. TSN is an Ethernet-based network system that is actively being developed for the factory automation and automobile network systems. TSN controls the flow of data streams based on schedules generated statically off-line to satisfy end-to-end delay or jitter requirements. However, the generation of TSN schedules is an NP-hard problem; because of this, constraint solving techniques, such as SMT (Satisfiability Modulo Theory) and ILP (Integer Linear Programming), have mainly been proposed as solutions to this problem. This paper presents a new approach using a heuristic greedy and incremental algorithm working with ILP to decrease the complexity of computing schedules and improve the schedule generation performance in computing TSN schedules. Finally, we compare our proposed method with the existing SMT solver approach to show the performance of our approach.
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.
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