CPA: Conference Support Proposal: 2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design

NSF CPA集群支持学生旅行参加第二届ACM/IEEE国际协同设计方法和模型会议(MEMOCODE.04)随着计算系统变得越来越复杂，集成到日常使用的文物，如手机，汽车，手持设备，医疗假肢和其他广泛的应用，对设计方法的需求能够保证硬件和软件的成功集成，功能的正确性和可靠性变得越来越重要。今天的计算不再局限于服务器、工作站和桌面计算，而是无处不在，最重要的是在医疗领域，以及在航空电子控制、汽车控制等安全关键系统中。然而，历史上硬件和软件都是分开构建的，两者都非常复杂，确保正确构建硬件或软件的方法学本身就是研究课题。然而，由于人类社会对无处不在和普适计算的日益依赖，我们面临着对形式化和数学技术来对集成了硬件和软件的系统进行建模和分析的需求。2003年，第一届国际ACM/IEEE协同设计形式化方法和模型(MEMOCODE)会议首次将在软件工程领域应用形式化方法的研究人员和应用形式化方法设计和验证硬件系统的研究人员聚集在一起。从小组讨论、重点讨论和非正式讨论中可以感受到，双方的正式方法从业者在知识、经验和技术方面都有很大的共同之处。此外，软硬件协同设计问题对这种共生提出了前所未有的需求，这也是创建这一系列会议的最初目的。更重要的是，去年(在法国)出席会议的美国研究人员认为，与欧洲的倡议和研究活动相比，美国在这一重要的正式方法领域缺乏研究活动。因此，今年的会议将在加利福尼亚州的圣地亚哥举行，以吸引更多的美国参与者，并为美国研究人员创造一个交流正式方法想法、技术和创造性倡议的论坛。这项建议寻求美国国家科学基金会的资金支持，以支持首次参加会议的美国研究生或高级本科生，使他们接触到正式方法的各个方面，并认识到正式方法在系统设计中的重要性，特别是硬件/软件安全关键系统。来自NSF的这种支持的智力影响将是，聪明年轻学生的出勤率的增加将推动这一非常重要领域的更多研究工作。由于研究人员对寻求正式方法的兴趣要小得多，欧洲共同体比美国同行取得了更大的进步。国家科学基金会可以为丰富MEMOCODE的教育和研究目标做出重大贡献。研讨会从NSF以外的其他来源获得了一些资金，用于邀请演讲者和其他费用。NSF申请的资金的更广泛影响是，它将为美国研究人员的学生提供旅行支持，以鼓励研讨会主题的教育和研究。重点将是资助那些没有其他资金来源的学生参加会议，并将努力资助代表性不足的团体的成员。

Proposal to NSF CPA Cluster for Supporting Student Travel to the 2nd ACM/IEEE International Conference on Methods & Models for Co-Design (MEMOCODE.04) As computing systems are becoming increasingly complex, integrated to daily usable artifacts such as cell phones, cars, hand-held devices, medical prosthetics and other wide range of applications, the need for design methodologies which can guarantee successful integration of hardware and software, functional correctness and reliability is gaining importance. Today.s computing is no longer limited to servers, work stations and desktop computing, but they are embedded everywhere, most importantly in the medical space, as well as in the safety critical systems such as avionics control, automotive control etc. However, historically hardware and software have been built separately, and both being extremely complex, the methodologies that ensure correct construction of hardware or software are themselves research topics. Yet, we are faced with the need for formal and mathematical techniques to model and analyze systems which integrate both hardware and software, because of the increasing reliance of human society on ubiquitous and pervasive computing. In 2003 the First International ACM/IEEE Formal Methods and Models for Co-Design (MEMOCODE) conference, for the first time, brought together researchers who apply formal methods in software engineering fields, and those who apply formal methods to design and validate hardware systems. It was felt from the panel discussions, key note talks, and informal discussions that formal method practitioners from both sides have a lot of share in terms of knowledge, experience and techniques. Also, the hardware-software co-design problem imposes an ever than before need for this symbiosis, which was the original aims of creating this series of conferences. More importantly, the US researchers present at the conference last year (in France), felt that there is a lack of research activity in this important area of formal methods in the US, compared to the initiatives and research activities in Europe. As a result, this year the conference is being held in San Diego, California, to bring more US participants, and create a forum for US researchers to exchange formal method ideas, techniques and creative initiatives. This proposal seeks financial support from NSF to support US graduate or advanced undergraduate students attending the conference for the first time, so that they get exposure to various aspects of formal methods, and recognize the importance of formal methods in system design, especially hardware/software safety critical systems. The intellectual impact of this support from NSF would be that the increased attendance of bright young students will fuel more research work in this very important area. The European community has made much more progress than their counter parts in the US due to a much less degree of interest by researchers to pursue formal methods. NSF can make substantial contribution to the enrichment of educational and research objectives of MEMOCODE. The workshop has some funding from sources other than NSF for invited speakers and other expenses. Broader Impact of the requested NSF funding is that it will provide travel support for students of US researchers, to encourage education and research in the workshop topic. The emphasis will be on funding students who do not otherwise have funding sources to attend the conference, and an attempt will be made to fund members of underrepresented groups.