Dilian
Gurov
last updated December
3, 1997
| |
Dilian
Gurov
last updated December
3, 1997
|
| formalWARE
project
formalWARE
formalWARE
|
Dilian Gurov is a Ph.D. student
in the Department of Computer Science at the University of Victoria supervised
by Dr. Bruce M. Kapron and Dr. Hausi A. Muller. He received his B.Sc. in
Computer Science in 1989 from the Technical University of Sofia, Bulgaria.
His thesis supervision committee includes his two supervisors as well as
Dr. Mantis Cheng (UVic) and Dr. Nikitas Dimopulos (UVic).
His primary research interest is the specification and verification of communicating systems where the content (or ``values'') of interactions between entities i s essential detail that must be considered when verifying that the system satisfies desired properties, e.g., free of potential deadlocks. Alongside with computation and information processing, interaction is becoming a more crucial aspect of computer systems and, in many instances, is the main source of complexity in the specification, design and verification of the system. Communication protocols, telephone switching systems, and air traffic control systems are examples of systems which fulfill their primary goals by interacting with other systems at least as much as they do by processing information. During such interaction (or communication), data (or values) are transmitted which often influence the future interactions of the participating agents. Systems with this sort of behaviour are often referred to as "communicating systems with value passing". Gurov pursues a logical approach to the specification and verification of communicating systems: the expected interaction behaviour of the system is specified by a set of properties (like, for example, the properties of not having deadlocks or livelocks), which are formalized as logic formulae in a suitable logic language, namely a (first-order) extension of the propositional modal mu-calculus. Then, an abstract design (i.e. model) of the system is created in a suitable process language, namely in value-passing CCS. To verify the model means to check whether all formulae of the specification hold in this particular model (model checking). Gurov, together with Bruce Kapron (UVic) and Sergey Berezin (CMU), is developing a proof system in which such proofs can be conducted. This effort is intended to provide machine assistance for the verification process, as well as to study theoretical aspects of our proof system. Gurov is collaborating with other FormalWare
researchers as well as personnel at Hughes to model and validate aspects
of the an aeronautical telecommunications network. The application layer
protocols of this network are excellent examples of communicating systems,
and thus, are very suitable for testing the applicability of Gurov's approach.
Related Publications:Berezin S., Gurov D.: A Compositional Proof System for the Modal mu-Calculus and CCS, Report CMU-CS-97-105, School of Computer Science, Carnegie Mellon University, January 1997 (submitted to the International Conference on Computer Aided Verification CAV'97).Gurov D., Berezin S., Kapron B.M.: A Modal
mu-Calculus and a Proof System for Value Passing Processes, Proceedings
of INFINITY International Workshop on Verification of Infinite State Systems,
Pisa, Italy, August 30-31, 1996, pp. 149-163, published by University of
Passau as MIP-96, 14 July 1996 (also to appear in the Electronic Notes
in Theoretical Computer Science, Vol.6 1996).
Further Information:He can be reached by email at dgurov@csc.uvic.ca.
. |
