CTL (Computation Tree Logic) model checking is a formal method for design verification that checks whether the behavior of the verified system is contained in that of the requirements specification. If this check doesn't pass, the CTL model checker generates a subset of fair states which belongs to the system but not to the specification. In this letter, we present an incremental method which successively modifies the latest verification result each time the design is modified. Our incremental algorithm allows the designer to make changes in terms of addition or subtraction of fair CTL formulas, or fairness constraints on acceptable behavior from the problem statement. Then, these changes are adopted to update the set of fair states computed earlier. Our incremental algorithm is shown to be better than the current non-incremental techniques for CTL model checking. Furthermore, a conclusion supported by the experimental results is presented herein.

In 1996, Chiu and Hsu proposed a multi-role-based access control (MRBAC) policy. Nevertheless, the Chiu-Hsu scheme can be further enforced by role list, union, and intersection (i. e. containment) to deal with the problems regarding the MRBAC and the object role with different security ranks. The author presents an improvement of the Chiu-Hsu scheme using more detailed list structure. This improvement offers some significant advantages.

As expert system technology gains wider acceptance in digital system design, the need to build and maintain a large scale knowledge base will assume greater importance. However, how to build a correct and efficient rule base is even a hard part in the knowledge-based system development. In this paper, we develop FARHDL (Frame-And-Rule-based Hardware Description Language) to form a knowledge base. The FARHDL is simple but powerful to specify the hardware requirements and can be directly simulated by PROLOG. Through the knowledge base transformed from FARHDL, a formal method can be developed to design, implement, and validate the digital hardware systems. Furthermore, behavioral properties, anomaly properties, structural properties, and timing properties are applied to analyze the requirements specification. The purposes of those properties are used to detect explicit/implicit incorrect specification clauses and to capture some desired requirements, such as completeness and consistency. Finally, the analysis results can be a useful tool for finding obscure problems in tricky digital system designs and can also aid in the development of formal specifications.

According to the grey data generating techniques in grey system theory, we propose a novel cryptosystem, whose applications can develop a new direction in the field of information security. In this paper, we present the concepts of sum-lock, difference-lock, sum-ladder, and difference-ladder. By using these concepts, we can obtain a cryptosystem with lock generation and sum-difference replacement ladder. In addition, we provide the encryption and decryption algorithms of our cryptosystem and adopt an illustrative example to verify it.