Jeffrey J.P. Tsai
Department of Electrical Engineering and Computer Science
- University of Illinois
Chicago, IL 60607, USA
tsai@eecs.uic.edu
Abstract
With the rapid growth of networking and high-computing power, the demand of larger and more complex software systems has increased dramatically. Examples include web-based systems, multimedia systems, telecommunication systems, intelligent agents systems, flight control systems, patience monitoring systems, robotics, virtual reality systems, and so on. However, the development of large-scale and complex software systems is much more difficult and error prone. This is due to the fact that techniques and tools for assuring the correctness and reliability of software systems lag far behind the increasing growth of size and complexity of software systems. The results are unreliable and poorly performing applications, delayed projects, and considerable cost overruns. In order to improve the usability and reliability of large-scale systems, the supporting techniques and development tools need to be greatly enhanced.
Formal verification is rapidly becoming accepted as a promising and automated method to verify the correctness of software systems. Despite many works in the area of formal verification, one of main bottlenecks so far is the state explosion problem. When the size of a software system increases linearly, the analysis complexity of the system could grow exponentially. The capability and performance of current techniques still can not efficiently verify typical large-scale software systems in practice. In this talk, we will introduce a set of new condensation theories: IOT-failure equivalence, IOT-state equivalence, and firing-dependence theory to cope with this problem. Our condensation theories are much weaker than current theories useful for the compositional verification of Petri nets and Labeled Transition Systems. Our technique can efficiently analyze several properties: boundedness, reachable markings, reachable sub-markings, and deadlock states. Based on the notion of our new theories, we develop a set of condensation rules for efficient verification of component-based software systems. The experimental results show a significant improvement in the analysis of several systems such as, communication models, task scheduling, and resource competition problems.
Last Updated: May, 9, 2000 by Elisabetta Ferrando