Grant: Discovery Grants Program - Individual

Formal methods in system verification is an important field of theoretical computer science. In my research project I am particularly interested in formal methods involvement in the context of the safety critical systems. Such systems are often described as a collection of communicating asynchronous sequential processes. The objective of this proposal is to study methods based on automata and language theory for formal verification of such systems. The objectives of the proposed research program are the following: 1. Define and study mathematical models for representing asynchronous communicating systems in terms of collections of tape sharing multi-tape transducers. In such models, sequential processes are seen as relations on words expressible by finite automata. We will study their fundamental properties such as: decidability and complexity of membership problem, equality problem, inclusion problem, various closure properties, etc. 2. Develop an assertion language supporting a hierarchy of abstraction layers. The assertion language will be based on ""simple-functions"" for which there exists a unique representation in terms of canonical ""Concatenation State Machine"". The language will allow the specification (at different levels of abstraction) of local state transformations of sequential processes and represent them by finite automata. Such representation would permit the use of model checking methods in the process of formal verification of the system. 3. Develop a process algebra in order to establish a concise syntax, together with formal mathematical semantics for asynchronous communicating systems. Such a process algebra would constitute the foundation for the development of various proof methods in order, for example, to perform hand-crafted proofs over complex (e.g., infinite state space) systems, for which model checking methods do not apply.