Here are my publications organized in
CiteULike free service.
Here is my personal bibliography
generated with COBISS (used by Slovenian libraries).
Here is BiBTeX file.
Here are publications cited in my Ph.D.
Journals:
Where not indicated, papers use english language.
Abstract:
This paper presents a systematic approach for
designing a C++ app for demonstrating sorting algorithms
on smartphones and tablets. It is part of an on-going project
on the usages of new technologies in education. The general
properties of mobile platforms are discussed together with
details specific to demonstrating sorting algorithms. The
implementation of Insertion Sort is given as an example.
The obtained results (e.g. design rules and algorithms) have
been tested within a prototype application.
Keywords:
Usability, Qt, Engineering Education, Mobile learning
Abstract:
Biddy is a BDD package under GPL, developed at the University of Maribor.
It uses ROBDDs with compleÂment edges, as described in the paper K. S. Brace, R. L. Rudell, R. E. Bryant,
Efficient Implementation of a BDD Package, 1990. Compared to other available BDD packages,
Biddy's most distinguishing features are its specially deÂsigned C interface and an original
implementation of autoÂmatic garbage collection. More generally, the Biddy project is not only
concerned with the computer library, but also ofÂfers a demo application for the visualization
of BDDs, called BDD Scout. The whole project is oriented towards a readÂable and comprehensible
source code in C, which can be compiled unchanged on different platforms, including GNU/Linux
and MS Windows.
Keywords:
Boolean algebra, binary decision diagram, symbolic manipulation of Boolean functions, formal methÂods, free software
Abstract:
Model checkers for systems represented by labelled transition systems are not as extensively
used as those for systems represented by Kripke structures. This is partially due to the lack
of an elegant formal language for property specification which would not be as raw as,
for example, HML yet also not as complex as, for example, $\mu$-calculus. This paper proposes
a new action-based propositional branching-time temporal logic ACTLW, which enhances popular
computation tree logic (CTL) with the notion of actions in a similar but more comprehensive
way than action-based CTL introduced by R. De Nicola and F. Vaandrager in 1990. ACTLW is
defined by using temporal operators until and unless only, whereas all other
temporal operators are derived from them. Fixed-point characterisation of the operators
together with symbolic algorithms for global model checking are shown. Usage of this new
logic is illustrated by an example of verification of mutual-exclusion algorithms.
Keywords:
formal verification, model checking, action-based temporal logic, fixed point, mutual-exclusion algorithm
Abstract:
Distributed mutual-exclusion (DME) circuits are an interesting example of asynchronous
circuits. They are composed of identical DME cells connected in a ring of arbitrary size.
Each DME cell provides a connection point for one user, and all users compete for exclusive
access to a shared resource. This paper reports about formal verification of two well-known
DME circuit implementations. External behaviour of the circuits is described with a simple
process, whereas the required properties are expressed with temporal logic ACTL. We were able
to detect hazards and verify correctness of external behaviour of the circuits under the
fundamental mode of operation.
Keywords:
asynchronous circuit, fundamental mode, process algebra, model checking, ACTL
Some results in this paper needs revision. They have been partialy revised in Ph.D.
Abstract:
It is of great interest for users of communication protocols
to have a proof that they are correct and reliable to
use. In order to prove a protocol correct formally, the
protocol and the required properties must be formally
described. This paper reports on verifying properties of
a bounded retransmission protocol for large data packets.
It is used to transfer les via a lossy communication
channel. We emphasize timing properties of the protocol.
We specied the protocol in Verilog and stated properties
in a computation tree logic. The verication was
carried out automatically by model checking. We used
the non-commercial tool VIS which made it possible to
introduce nondeterministic choice of data packets length
and a realistic notion of time.
Keywords:
formal verication, bounded retransmission protocol, model checking, CTL, Verilog, VIS
Abstract:
This paper describes data structures and algorithms for the representation of Boolean
functions with reduced ordered binary decision diagrams (ROBDDs). A hash table is used for
quick search. Additional information about variables and functions is stored in binary trees.
Manipulations on functions are based on a recursive algorithm of ITE operation.
The primary goal of this article is to describe programming technics needed to realize
the idea. For the first time here recursive algorithms for composing functions and garbage
collection with a formulae counter are presented. This is better than garbage collection
in other known implementations. The results of the tests show that the described
representation is very eficient in applications which operate with Boolean functions.
Keywords:
boolean algebra, reduced ordered binary decision diagrams
The main results of this paper are also covered in paper "Representation of Boolean functions with ROBDDs" which has been presented at IEEE Region 8 Student Paper Contest, Paris-Evry, 1993.
Conference papers:
Where not indicated, papers use english language.
Firefox OS: a new challenge for student projects
Abstract:
Telecommunications students must carry out a number of projects while studying,
and many of them involve mobile devices.
This paper suggests that Firefox OS, a new mobile operating system, is a good
platform for such projects.
One of its interesting benefits is a fast learning curve
because it builds on standardised web technologies, which are
already familiar to many students.
Moreover, using an open platform is an ideal choice
for academic environments.
This paper shows that one can make an interesting project in a few
relatively easy steps without installing and learning complex environments.
Some important aspects of project planning are also discussed and an example
of a student project is given.
Abstract: This paper presents a systematic approach to the implementation of a mobile framework for demonstrating of sorting algorithms. Well-known corresponding projects are listed. The pseudo-code form is discussed, together with the graphical presentation of actions. A set of atomic operations that reveal the concept of sorting algorithms has been identified. Implementations of Gnome Sort, Insertion Sort, and Quicksort are given as a portable C-style code. The presented code has been tested within a prototype application on a modern smartphone. The project was oriented towards the usage in mobile learning systems.
Using FLTK in the course about C++ programming
Abstract:
This paper gives three relatively short C++ programs. They demonstrate the building of a graphical user
interface by using free cross-platform library FLTK. All three programs are described and can be useful for
demonstration of the basic concepts of object-oriented programming. Indeed, when students master them, their
knowledge and programming skills are good enough to understand and create complex object-oriented
programs - and this is our main goal of teaching programming in the first year.
Abstract: EST is a tool for formal verication of systems. A system to be verified should be specified in a CCS-like syntax. CCS has been chosen because it is widely used in theoretical approaches due to a relatively small set of operators and nice laws valid for them. In this paper we make an overview of operators supported by EST. They can be classified into two groups: standard CCS operators and additional operators which we introduced to shorten specifications and to facilitate traslations from other formalisms.
Abstract: Witnesses and counterexamples produced by model checkers provide a very useful source of diagnostic information. They are usually returned in the form of a single computation path along the model of the system. However, a single computation path is not enough to explain all reasons of a validity or a failure. Our work in this area is motivated by the application of action-based model checking algorithms to the test case generation for models formally specied with a CCS-like process algebra. There, only linear and nite witnesses and counterexamples are useful and for the given formula and model an ecient representation of the set of witnesses (counterexamples) explaining all reasons of validity (failure) is needed. This paper identies a fragment of an action-based computation tree logic (ACTL), that guarantee linear witnesses and counterexamples. For it, witness and counterexample automata are introduced, which are nite automata recognizing linear witnesses and counterexamples, respectively. An algorithm for generating such automata is given.
Some results in this paper needs revision. They has been already revised in Ph.D.
A framework for automatic solving of logic riddles
Abstract:
We study a sort of logic riddles given as a set of facts
from which other facts must be derived. These problems,
usually stated for entertainment, can be easily solved if
there is only a small number of possible solutions. However,
they become much more complex when the number
of facts and possible solutions grows. The problem motivated
us to think about a framework for automatic solving
using computer. It is based on a propositional calculus.
The most complex part of the system is parsing and understanding
of the facts stated in a natural language as
well as their transformation into mathematical formulae.
Abstract: Model checking has become a widely used technique for verification of concurrent systems. However, its use is still much restricted to scientists with high mathematical education because temporal logic formulae are difficult to understand and even more difficult to create. Therefore, many projects have been started to find out how computers can help engineers in specifying system properties. This paper reports on using patterns of temporal logic formulae, which facilitate the usage of model checking.
Some results in this paper needs revision. They has been already revised in Ph.D.
Abstract: This paper is about technical reports, a special type of research papers, that are getting more and more popular source of scientific knowledge. Five most important search engines for locating technical reports are described. Some other sources of research papers on the Internet are mentioned, too. Reading the paper you can improve your skills to search for scientific knowledge significantly. This is also the main purpose of the paper.
This paper is a little bit outdated.
Abstract: Efficient Symbolic Tools (EST) is a software package for formal verification of concurrent systems. It appears as an educational project and has been entirely written in the Laboratory of Microcomputer Systems at the Faculty of Electrical Engineering and Computer Science in Maribor. The main purpose of our work was a study of algorithms that could serve for formal verification of complex protocols, which are used in computer and telecommunication networks.
This paper is a little bit outdated.
Abstract: Model checking is a formal method widely used in computer science for verification of concurrent systems, e.g. communication protocols. The method requires that a system is given with a graph and properties of the system are given as a set of logic formulas. Model checking is an algorithmic method and it can be carried out fully automatically by fixpoint calculation. This paper describes how to use model checking for safety assurance of logistic systems.
Abstract: Various process algebras have been introduced for reasoning about concurrent systems. Some of them include explicit data-passing mechanisms, while others do not. This paper presents a non-trivial problem involving data, which can also be comprehensively solved with a simple process algebra without explicit data-passing. The presented problem is very suitable for comparing the strength of different process algebra software tools.
Some results in this paper needs revision.
Abstract: Process algebras are a convenient tool for describing and reasoning about the behaviour of concurrent systems. A variety of equivalence relations are used to study the relationship between different systems or between different levels of abstractions of the system. This paper reports on an implementation of a testing equivalence with binary decision diagrams (BDDs). It is defined in terms of observations that process may or must satisfy. As the testing equivalence is shown to be an instance of a bisimulation equivalence, efficient algorithms for computing bisimulations using BDDs could be employed for its implementation.
Universal decomposition rule for OBDD, OFDD, and 0-sup-BDD
Abstract:
Binary decision diagrams (BDD) are very successful data structure for
representation and manipulation of Boolean functions. Various types of
BDDs have been proposed. In this paper relations between OBDD, OFDD,
and 0-sup-BDD are shown in a new way. A generic decomposition rule for
them is introduced. Using this rule a set of 288 types of BDDs is
defined together with their reduction rules.
Representing Images with Binary Decision Diagrams
Abstract:
This paper suggests binary decision diagram
(BDD) as a useful data structure for representing
images and image sequences. First, we give a short
description of BDDs. Next, we show how they can
be used to represent images. We perform some tests
with bintrees and two common types of binary decision diagrams,
ROBDDs and 0-sup-BDDs. Results show that BDDs are very efficient.
This paper has been superseded. Its main results are covered in paper "ACTLW - An Action-based Computation Tree Logic With Unless Operator", Information Sciences, 2008.
This paper has been superseded. Its main results are covered in paper "ACTLW - An Action-based Computation Tree Logic With Unless Operator", Information Sciences, 2008.
This paper has been superseded. Its main results are covered in paper "ACTLW - An Action-based Computation Tree Logic With Unless Operator", Information Sciences, 2008.
This paper has been superseded. Its main results are covered in paper "ACTLW - An Action-based Computation Tree Logic With Unless Operator", Information Sciences, 2008.
This paper has been superseded. Its main results are covered in paper "ACTLW - An Action-based Computation Tree Logic With Unless Operator", Information Sciences, 2008.
This paper has been superseded. Its main results are covered in paper "Exploring properties of a bounded retransmission protocol with VIS", CIT --- Journal of Computing and Information Technology, 1999.
Other
Where not indicated, papers use english language.
Abstract: This paper describes data structures and algorithms for the representation of Boolean functions with reduced ordered binary decision diagrams (ROBDDs). A hash table is used for quick search. Additional information about variables and functions is stored in binary trees. Manipulations on functions are based on a recursive algorithm of ITE operation. The primary goal of this article is to describe programming technics needed to realize the idea. For the first time here recursive algorithms for composing functions and garbage collection with a formulae counter are presented. This is better than garbage collection in other known implementations. The results of the tests show that the described representation is very eficient in applications which operate with Boolean functions. Keywords: boolean algebra, reduced ordered binary decision diagrams
Ph.D. thesis
An action-based computation tree logic with unless operator
Abstract:
This thesis defines and studies action-based computation tree logic with
{\em unless} operator (ACTLW). ACTLW is a propositional branching-time temporal logic.
It is derived from logic ACTL, which was introduced in 1990 and which is one of
established temporal logics for expressing properties of action-based models.
ACTLW is more flexible than ACTL, because it does not impose the usage of silent action
$\tau$ in expressing of the properties. ACTLW has also a slightly greater expressive
power than ACTL, because it contains temporal operator {\em unless} ($\W$), whose meaning
cannot be fully covered in ACTL. As opposite, all ACTL formulae can be expressed using
ACTLW operators. ACTLW enables efficient implementation of model checking by using
similar algorithms to those used for CTL model checking, which is a significant advantage
in comparison to logic ACTL. The thesis gives a definition of logic ACTLW, derivations of
all standard temporal operators, and algorithms for global ACTLW model checking using
symbolic methods. Moreover, algorithms for generation of diagnostics for ACTLW, for
generation of linear witnesses and counterexamples for ACTLW, and for generation of
witness and counterexample automata for ACTLW are presented. The thesis is accomplished
with patterns of ACTLW formulae and two larger practical examples: a verification of
several different mutual-exclusion algorithms and a verification of two asynchronous
distributed mutual-exclusion circuits.
Keywords:
formal methods of system verification, model checking, temporal logic,
CTL, ACTL, ACTLW, diagnostics, witness, counterexample,
witness and counterexample automaton, mutual-exclusion problem
Master thesis
Checking correctness of concurrent systems behaviour
Abstract:
This master thesis is about methods for checking correctness of
concurrent systems behaviour based on the system specification with
a process algebra. A definition of the process algebra and some examples
of system specifications in terms of processes are given.
The master thesis presents the checking of trace equivalence,
strong, branching, and weak observational equivalence, testing equivalence,
and symbolic model checking with propositional branching-time temporal
logic ACTL. All discussed methods together
form an efficient tool for formal verification of systems.
An implementation of such a tool with BDDs is described.
The usage of the tool is demonstrated on the verification
of communication protocol BRP.
Keywords:
formal methods of system verification, concurrent systems,
process algebras, observational equivalences, testing equivalences,
symbolic model checking, ACTL, BDD
Diploma work
Using Ordered Decision Diagrams for Computer-Aided Manipulation of Boolean Functions
Abstract:
Decision Diagrams are successful data structure for representation
of Boolean functions. Mathematical background
needed for their understanding and computer algorithms for their
efficient implementation are given in this diploma work.
Ordered Binary Decision Diagrams (OBDDs), Ordered Functional Decision
Diagrams (OFDDs) and Zero-Suppresed Binary Decision Diagrams (0-sup-BDDs)
are described in details. Also, a short overview of Free Binary Decision
Diagrams (FBDDs), Extended Binary Decision Diagrams (XBDDs), Ordered
Kronecker Functional Decision Diagrams (OKFDDs) and Differential
Binary Decision Diagrams ($\triangle$BDDs) is included.
For ROBDD, ROFDD, and 0-sup-BDD the decomposition rule
and reduction rule are shown and algorithms for logical operations
are derived. Algorithms were realized in programming language C.
Efficiency of various types of decision diagrams is compared.
Results of tests in the domains of Boolean function equality testing,
representing combination sets, and representing images are given.
Keywords:
Boolean algebra, Boolean functions, Binary Decision
Diagrams, Functional Decision Diagrams, data structures