A.B. Can, Design for Verification for Concurrent& Distributed Programs

Faculty of Engineering and Natural Sciences
FENS SEMINARS

Design for Verification for Concurrent and Distributed Programs

Aysu Betin Can

Assuring reliability and correctness of complex software systems is a challenging problem. Most automated verification techniques and tools do not scale very well due to difficulty of extracting compact models from software systems. Typically, model extraction requires human guidance and reverse engineering in order to rediscover some information about the software that may be known to its developers at design time.

In this talk, I will present a design for verification (DFV) approach that embeds intentions of developers into software and makes software systems amenable to automated verification; hence, making the automated verification techniques scalable to large systems. The proposed DFV approach is applied to concurrent programming by introducing the concurrency controller pattern with the goal of eliminating synchronization errors in concurrent Java programs. The effectiveness  of this framework is investigated on two software systems: a concurrent text editor and a safety critical air traffic control software. The presented DFV approach is also applied to asynchronously communicating web services by introducing the peer controller pattern with the goal of both analyzing properties of interactions among the services in the composition and validating the conformance of the implementations to their interface specifications. The synchronizability analysis is adapted to this framework to enable behavior verification with respect to unbounded asynchronous communication queues. The presented framework is extended with an hierarchical interface model for compact representation of peer interfaces. The effectiveness of this framework is investigated with several composite web service implementations based on the peer controller pattern.

Biography:
Dr. Aysu Betin-Can received his Bachelor's degree in Computer Engineering from Middle East Technical University (METU), Ankara, Turkey in 1999 and Ph.D. (2005) degrees in Computer Science from University of California at Santa Barbara. Her research interests are software engineering, reliable software development, modular verification and specification, web services, concurrency, and model checking.

November 23, 2005, 15:40, G029