Vol. 25 · No. 5

In this paper, formal verification methodologies and the SPR (Safety Problem Resolver) model checking tool are used for verifying a security model's safety. The SPR tool makes it possible to analyze security issues on security systems based on the access control model. To illustrate this approach, a case study of the Simple Access Control Model (SACM) is used and specific safety problems of the security model are analyzed using the SPR tool.

At present, the importance of the biometric security increases a lot in cotext of the events in the world. Development of the individual biometric technologies such as the fingerprint recognition, iris or retina recognition or speaker recognition has been considered very important. However, it comes to be true that only one biometric technology is not sufficient enough. One of the most prosperous solutions might be a combination of more such technologies. This article aims at the technology of the speaker recognition and proposes a solution of its integration into a more complex biometric security system. Herein a design of the complex biometric security system is introduced based on the speaker recognition and the fingerprint authentication. A method of acquisition of a unique vector from speaker specific features is introduced as well.

We study randomly induced subgraphs G of a hypercube. Specifically, we investigate vertex covering of G by cubes. We instantiate a greedy algorithm for this problem from general hypergraph covering algorithm citeS72, and estimate the length of vertex covering of G. In order to obtain this result, a number of theoretical parameters of randomly induced subgraph G were estimated.

This paper deals with scheduling for single machine batch processing, specifically the transporting problem with one vehicle. Capacity restrictions of the machine are considered and the main objective is to find an assignment of jobs to achieve the minimal processing time of all batches, given these capacities. A polynomial algorithm is proposed for solving the case in which the jobs are non-preemptive, non-identical, and are known before the realization of the schedule. The proposed algorithm is implemented and shown to yield better results than alternatives from the literature.

MAS is a powerful paradigm in nowadays distributed systems, however its disadvantage is that it lacks the interconnection with semantic web standards such as OWL. The aim of this article is to present a semantic knowledge model of an agent suitable for discrete environments as well as implementation and a use of such model using the Jena semantic web library and the JADE agent system. The developed library allows interconnection of Agent and Semantic Web technologies can be used in an agent based application where such interconnection is needed. The defined model and methodology show the use of the library in knowledge management applications where the proposed model has been used and evaluated in the scope of the Pellucid and K-Wf Grid IST projects.

The paper presents novel testability analysis method applicable to regis-ter-transfer level digital circuits. It is shown if each module stored in a design library is equipped both with information related to design and information related to testing, then more accurate testability results can be acieved. A mathematical model based on virtual port conception is utilized to describe the information and proposed testability analysis method. In order to be effective, the method is based on the idea of searching two special digraphs developed for the purpose. Experimental results gained by the method are presented and compared with results of existing methods.