|
|
This page gives an overview of the research projects I have been
involved while in the graduate school. The projects are sorted according to the
institution where the projects took place. For details about my current
projects, please visit my current research
web page. If you need more information about my previous research
projects, feel free to contact me via e-mail.
|
|
Wayne State University,
Detroit, Michigan Since Fall 2000 I worked on my Ph.D.
degree in Computer Science under the supervision of Dr.
Frank Stomp. My research
focused on Formal Methods and verification of algorithms and their
correctness proofs. I was involved in several projects:
 | A Proof of an Atomic Register Construction (2002-2005)
An implementation of an atomic bit register was published recently.
The algorithm, although short in description, is complicated. This
project was aimed at investigation of correctness of that algorithm. We
developed a correctness proof of the algorithm and worked on mechanization
of
the proof using the PVS theorem prover.
|
| A Formal Proof of a Self-Stabilizing ℓ-Exclusion Algorithm
(2001-2004)
Distributed and parallel algorithms are usually complicated. An ℓ-exclusion algorithm implements a protocol that ensures
that not more that ℓ processes are in their critical sections at
the same time and every process interested in entering its
critical section eventually enters the critical section. A
self-stabilizing version of that algorithm ensures that the protocol
tolerates transient failures.
In this project, we developed a formal correctness proof of a self-stabilizing ℓ-exclusion
algorithm (SLEX). The analyzed algorithm is an
improvement of SLEX due to Abraham, Dolev, Herman, and Koll,
since our version satisfies a stronger liveness property. The
proof is formulated in Linear-Time Temporal Logic and consists
of a safety part and a liveness part. Our analysis provides some
new insight in the correctness of the algorithm: (1) We
characterize processes (and their minimum number) identified by
some process as attempting to enter their critical sections, and
(2) a novel proof rule for reasoning about programs in the
presence of disabled processes is presented to structure the
liveness proof. Our proof is constructive, in contrast to the
operational arguments of Abraham et al.
Related Publications:
 | Besta, M.: Self-Stabilizing ℓ-Exclusion: A Correctness Proof.
Dissertation, Wayne State University, Detroit, MI, June 2005. |
| Besta, M. and F. Stomp:
An Assertional Correctness Proof of a Self-Stabilizing ℓ-Exclusion Algorithm (Extended Abstract).
In Proceedings of the 11th IEEE International Conference on Engineering of Complex Computer Systems
(ICECCS '06), pp. 199-208, Stanford, CA, August 2006. |
| Besta, M:
Self-stabilizing ℓ-exclusion: A Correctness Proof.
Dissertation prospectus, Wayne State University, Detroit,
MI, 2002. |
| Abraham, U., S. Dolev, T. Herman, and I. Koll:
Self-stabilizing ℓ-exclusion. In Theoretical Computer
Science 266(1-2), 653-692, 2001.
|
|
| Boyer-Moore's String Preprocessing Algorithm (2000-2002)
The Boyer-Moore's pattern matching algorithm utilizes two
preprocessing algorithms: one based on single characters only and the
other based on a string. Correctness of the single-character
preprocessing algorithm has been established and mechanically verified
by Boyer and Moore in 1981. The string-preprocessing algorithm is more
complicated. There have been found several errors in that algorithm by
different authors. In 1999, a minor error was found in the
string-preprocessing algorithm and corrected. To make sure the
correction of that error does not introduce any new errors in the
algorithm a correctness proof of the corrected algorithm was
developed. In this research project we have mechanically verified the
hand-written correctness proof using the PVS theorem prover. The PVS
proof can be found
here.
Related Publications:
| Besta, M. and F. Stomp:
A complete mechanization of a
correctness proof of a string-preprocessing algorithm. In
Formal Methods in System Design 27(1-2), pp. 5-27, 2005. |
| Besta, M. and F. Stomp:
Mechanization of a proof of a string-preprocessing in Boyer-Moore's
pattern matching algorithm. In Proceedings of the 8th
International Conference on Engineering of Complex Computer Systems
(ICECCS '02), pp. 68-77, IEEE CS, December 2002, Greenbelt, MD. |
| Stomp, F.:
Correctness of substring-preprocessing in Boyer-Moore's pattern
matching algorithm. In Theoretical Computer Science
290(1), 59-78, 2003.
|
|
|
|
Charles University, Prague,
Czech Republic In Fall 1997 I started working on my Ph.D. degree under
the supervision of Dr. Frantisek Plasil. During my stay at the
Department of Software Engineering I worked on
| Behavior Protocols (1998-2000)
Nowadays most of software products are built from software components.
A component is described by a set of interfaces providing services to
clients and a set of interfaces requesting services from other
components. Larger components are assembled from smaller components.
Architectures of assembled components are described by means of an
architecture description language. It is desirable to describe not
only component architecture, but also component collaboration, i.e.,
component behavior. We conducted research to enhance an architecture
description language with a description of component behavior. You can
read more about behavior protocols
here.
Related Publications:
| Plasil, F., S. Visnovsky, and M. Besta:
Bounding component behavior via protocols. In Proceeding of
Technology of Object-Oriented Languages and Systems (TOOLS 30),
pp. 387-398, IEEE CS, August 1999, Santa Barbara, CA. |
| Plasil, F. and S. Visnovsky:
Behavior protocols for software components. In IEEE
Transactions on Software Engineering 28(11), 1056-1076, 2002.
|
|
|
| Palacky University,
Olomouc, Czech Republic I received my Bachelor and Master's degrees in
Computer Science from Palacky University in Olomouc. During my studies
in the
Department of Computer Science, I worked under the supervision of Dr.
Vladimir Sklenar and was involved in three research projects. Their
brief descriptions is below:
| Abstract Data Views (1994-1996)
My Master thesis research was on a new programming concept called
Abstract Data Views (ADV). This is a design and implementation
mechanism providing clean separation of the user interface from the
application at both the design and implementation level. This concept
can be used not only for graphical presentation of the application
state, but also as a means of communication among (distributed)
components.
Related Publications:
| Besta, M.:
Abstract Data Views. Master's thesis, Palacky University,
Olomouc, Czech Republic, May 1996.
|
|
| ALVIS - Algorithm Visualization (1993-1995)
In order students better understand design principles of new
algorithms it is convenient to employ a demonstration tool. In the
course of this project we implemented a sophisticated tool that
allowed one to design a visual demonstration of an arbitrary
algorithm. We implemented language interpreters of several programming
languages and many data and program view components to allow for
visualization and interaction between a user and the tool.
Related Publications:
| Sklenar, V., M. Kudelka, and V. Snasel: A Software Tool for
Visualization of Algorithms. In Proceedings of Computer Based
Learning in Science (CBLIS '95), Opava, Czech Republic, July
1995. (ISBN 80-901974-0-X)
|
|
| Normal Forms of Context-Free Grammars (1992-1993)
In this project we implemented a tool for transformation of
context-free grammars into Chomsky and Greibach Normal Forms. The tool
offers a user interface to allow for demonstration of transformation
steps that have to be taken during execution of the transformation
algorithms. You can download the project archive
here (in
Czech).
|
|
|
