A Formal Framework for Software System Modeling, Analysis and Realization 报告人: Xudong He, Florida International University 时间: 6月25日,上午10:00 - 11:30 地点: 蒙民伟楼 506室 摘要 Software is playing an essential role in the functioning of our society. Many software systems are often mission and safety critical and thus need to be highly dependable. How to develop and ensure the dependability of these complex software systems is a grand challenge. In this talk, a formal framework called SAM for software system modeling, analysis, and realization is presented. This formal framework has being developed at Florida International University for almost ten years. This formal framework is founded on two complementary formal methods Petri nets and temporal logic. Petri nets are used to define the behavior models of software components while temporal logic is used to specify desirable properties. Various approaches have been developed for modeling object-oriented, aspect-oriented, and agent-oriented systems. Formal analysis techniques based on existing model checking methods as well as testing techniques to assure design correctness have been explored. Furthermore a translation technique is implemented to generate prototypical Java implementation from a given SAM software architecture description. We believe that this formal framework forms the basis of a sound engineering approach for developing highly dependable software systems. 简介 Xudong He received the BS and MS degrees in computer science from Nanjing University, China, in 1982 and 1984, respectively. He received the Ph.D. degree in computer science from Virginia Polytechnic Institute & State University (Virginia Tech) in 1989. He joined the faculty in the School of Computing and Information Science (SCIS) at Florida International University (FIU) in 2000, and is professor of SCIS and the Director of the Center for Advanced Distributed System Engineering. His research interests include formal methods, especially Petri nets, and software testing techniques. |