Lempel-Ziv-Markov Chain Algorithm Modeling using Models of Computation and ForSyDe

Abstract

The data link is considered a critical function of modern aircraft, responsible for exchanging information to the ground and communicating to other aircraft. Nowadays, the increasing amount of exchanged data and information brings the need for network usage optimization. In this sense, data compression is considered a key approach to make data packages size smaller. Regarding the fact that avionics systems are safety-critical, it is fundamental not losing data nor performance during the compression procedures. In this context, manufacturers and regulatory agencies usually follow DO-178C guidance. Targeting model-based embedded design guidelines, DO-178C includes a supplement document, named DO-331. In this paper , we describe a widely used data compression algorithm, the Lempel-Ziv-Markov Chain algorithm (LZMA). Regarding formal model-based design, we argue that the synchronous dataflow model of computation captures the algorithm behavior more directly. The Formal System Design (ForSyDe) methodology is used to model the LZMA.