报告题目：Supporting Construction, Analysis, and Understanding of Software Models（软件模型的形式化构建、分析和理解）

报告人：Dr. Marsha Chechik  ( Department of Computer Science, University of Toronto)

报告时间：5月29日下午三点

报告地点：FIT大楼1-101

主办单位：软件学院

学科分类：计算机科学与技术

内容简介：

Supporting Construction, Analysis, and Understanding of Software Models

                            Marsha Chechik

                   Department of Computer Science

                        University of Toronto

Software systems of today are pervasive, increasingly complex, and

error prone.  Software bugs lead to a loss of productivity, denial of

service, and security breaches, cost millions of dollars to the

economy, and sometimes cause a loss of human life.  It is clear that

testing alone is not sufficient to improve our confidence in these

systems and must be supplemented by more sophisticated analysis

techniques.

In the talk, I will discuss several approaches aimed at automated

reasoning about software artifacts.  The first of these is YASM -- a

software model-checker that reasons about models automatically

extracted directly from C code.  Unlike similar approaches, it is well

suited for both verification and bug finding.  Furthermore, YASM can

check safety (i.e., assertion violations) and liveness (i.e.,

non-termination) properties.  The current research prototype can handle

programs which are a few thousand lines of code, and has been

successfully applied to analyzing device drivers, parts of Linux

filesystem, and parts of OpenSSH.

In the second part of the talk, I give a general overview of

our activities in techniques for creating and understanding software

models.  In particular, I will describe our work on TLQSolver --

a model-exploration tool that uses model-checking technology to

discover temporal logic properties of a design.

Biography:

Marsha Chechik received her Ph.D. from the University of Maryland in

1996 and joined the department of Computer Science at the University

of Toronto.  She is currently an associate professor, cross-appointed

to the Department of Electrical and Computer Engineeering.

Prof. Chechik's research interests are mainly in the use of automated

reasoning techniques to improve the quality of software.  She has

published over 50 papers in formal methods (specifically,

model-checking), software specification and verification, multi-valued

logics, computer security and requirements engineering.  In 2002-2003,

Prof. Chechik was a visiting scientist at Lucent Technologies in

Murray Hill, NY and at Imperial College, London UK.  She is an

associate editor of IEEE Transactions on Software Engineering and has

served on program committees of several major international

conferences.