Towards Standardized Conformance Test Suite for ISO Transport Layer Protocol

In this paper, we develop a sound Conformance Test Suite for the Transport Layer Protocol Internationally standardized by both ISO and IEC. This is to test the implementations of the protocol, promote and facilitate standardized test suites, and promote the use of formal methods. We use formal methods for the generation of testing sequences to make the results sound. The protocol is formally specified in Lotos; the ISO/IEC Formal Description Technique for computer/communications protocols and distributed systems.

The Design and Implementation of a Editor that Supports Syntax Highlighting of E-Lotos

Formal methods (FM) are mathematically based techniques that provide a rigorous basis for software development: the application of FMs makes it possible to achieve provable correctness and reliability in the various steps of system design and implementation. Generally, Formal methods need the support of formal description technique (FDT). Because the FDL has strict syntax and semantics. It is the realization of the abstract to the concrete, strictly, can be symbolic execution, unambiguous. E-LOTOS formal description is an important technology. This paper describes the design and the implement of the editor that support syntax highlighting of E-LOTOS. The editor is implemented using java Swing and JFlex.

Precise Descriptions of VLC Synchronization with CSP Semantic Models

Variable length codes (VLC) have found widespread applications due to their inherent coding efficiency. However, encoder-decoder synchronization becomes critically important for VLC to operate properly. Traditional treebased techniques lack the scalability to analyse the synchronization behaviours of VLC, and simulation techniques are typically used instead for large code sets. Building on an initial paper in which we first described an application of CSP to this domain, we present further advances in this paper. The contributions of this paper are twofold. First, we describe a novel application of the CSP stable failure model to completely describe the VLC synchronization mechanisms. Consequently, we concisely characterize bit patterns that can bring about rapid synchronization. The overall goal is to advance our understanding in this important area of research through an established formal description technique originally developed and used within the computing research community.